From ca6390da2bbd4e379cccad80e8b157ad8d3e51f6 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Thu, 1 Jun 2023 10:33:08 -0400
Subject: [PATCH] prove substId/substAssoc for EvCtx

---
 .../Convenient/Linear/Properties.agda         | 38 +++++++++++++++++++
 .../TermModel/Convenient/Semantics.agda       |  7 ++--
 2 files changed, 42 insertions(+), 3 deletions(-)
 create mode 100644 formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient/Linear/Properties.agda

diff --git a/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient/Linear/Properties.agda b/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient/Linear/Properties.agda
new file mode 100644
index 0000000..9e8312b
--- /dev/null
+++ b/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient/Linear/Properties.agda
@@ -0,0 +1,38 @@
+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 _ _ _)
diff --git a/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient/Semantics.agda b/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient/Semantics.agda
index cd5d6ed..cc851e2 100644
--- a/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient/Semantics.agda
+++ b/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
-- 
GitLab