prove substId/substAssoc for EvCtx

formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient/Linear/Properties.agda

+module Semantics.Abstract.TermModel.Convenient.Linear.Properties where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor
+open import Cubical.Categories.Monad.Strength.Cartesian
+open import Cubical.Categories.Monad.Kleisli
+open import Cubical.Categories.DistributiveLaw.ComonadOverMonad.BiKleisli.Base
+open import Cubical.Categories.DistributiveLaw.ComonadOverMonad.BiKleisli.Morphism
+open import Cubical.Categories.DistributiveLaw.ComonadOverMonad.BiKleisli.Morphism.Properties
+open import Cubical.Categories.Comonad.Instances.Environment
+
+open import Semantics.Abstract.TermModel.Convenient
+open import Semantics.Abstract.TermModel.Convenient.Linear
+private
+  variable
+    ℓ ℓ' : Level
+
+module StrengthLemmas (𝓜 : Model ℓ ℓ') where
+  open Model 𝓜
+  open Category cat
+  open Functor
+  open StrengthNotation 𝓜
+
+  private
+    variable
+      Γ Δ a b c : ob
+      γ δ : Hom[ Δ , Γ ]
+      E : Linear Γ [ a , b ]
+  id^* : (id ^*) ⟪ E ⟫ ≡ E
+  id^* {E = E} = cong₂ _∘_ refl (×pF .F-id) ∙ ⋆IdL _
+
+  comp^* : ((γ ∘ δ) ^*) ⟪ E ⟫ ≡ ((δ ^*) ⟪ ((γ ^*) ⟪ E ⟫) ⟫)
+  comp^* {E = E} =
+    cong₂ _∘_ refl (cong₂ _,p_ (sym (⋆Assoc _ _ _) ∙ cong₂ _∘_ refl (sym ×β₁) ∙ ⋆Assoc _ _ _)
+                               (sym ×β₂ ∙ cong₂ _∘_ (sym (⋆IdR _)) refl)
+                   ∙ sym ,p-natural)
+    ∙ (⋆Assoc _ _ _)

formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient/Semantics.agda

@@ -24,6 +24,7 @@ open import Syntax.Types
 open import Syntax.Terms
 open import Semantics.Abstract.TermModel.Convenient
 open import Semantics.Abstract.TermModel.Convenient.Linear
+open import Semantics.Abstract.TermModel.Convenient.Linear.Properties
 
 private
   variable
@@ -50,6 +51,7 @@ module _ (𝓜 : Model ℓ ℓ') where
   module T = IsMonad (𝓜.monad .snd)
   ⇒F = ExponentialF 𝓜.cat 𝓜.binProd 𝓜.exponentials
   open StrengthNotation 𝓜
+  open StrengthLemmas 𝓜
 
   ⟦_⟧ty : Ty → 𝓜.cat .ob
   ⟦ nat ⟧ty = 𝓜.nat
@@ -124,9 +126,8 @@ module _ (𝓜 : Model ℓ ℓ') where
   ⟦ ∘IdR {E = E} i ⟧E = Linear _ .⋆IdL ⟦ E ⟧E i
   ⟦ ∘Assoc {E = E}{F = F}{F' = F'} i ⟧E = Linear _ .⋆Assoc ⟦ F' ⟧E ⟦ F ⟧E ⟦ E ⟧E i
   ⟦ E [ γ ]e ⟧E = (⟦ γ ⟧S ^*) ⟪ ⟦ E ⟧E ⟫
-  -- TODO: upstream, show change-of-comonad is functorial in the morphism of distributive laws
-  ⟦ substId i ⟧E = {!!}
-  ⟦ substAssoc i ⟧E = {!!}
+  ⟦ substId {E = E} i ⟧E = id^* {E = ⟦ E ⟧E} i
+  ⟦ substAssoc {E = E}{γ = γ}{δ = δ} i ⟧E = comp^* {γ = ⟦ γ ⟧S} {δ = ⟦ δ ⟧S} {E = ⟦ E ⟧E} i
   ⟦ ∙substDist {γ = γ} i ⟧E = (⟦ γ ⟧S ^*) .F-id i
   ⟦ ∘substDist {E = E}{F = F}{γ = γ} i ⟧E = (⟦ γ ⟧S ^*) .F-seq ⟦ F ⟧E ⟦ E ⟧E i
   ⟦ bind M ⟧E = ⟦ M ⟧C