From 14c41b3666d5755e9b1ab43e0e8be78f64167764 Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Mon, 16 Oct 2023 11:07:30 +0200
Subject: [PATCH] =?UTF-8?q?=E2=9C=A8=20Added=20missing=20proof=20principle?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Monad/Instance/Delay.lagda.md | 39 +++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)

diff --git a/src/Monad/Instance/Delay.lagda.md b/src/Monad/Instance/Delay.lagda.md
index dad34bb..f50a4dd 100644
--- a/src/Monad/Instance/Delay.lagda.md
+++ b/src/Monad/Instance/Delay.lagda.md
@@ -13,6 +13,7 @@ open import Categories.Monad.Construction.Kleisli
 open import Categories.Category.Construction.F-Coalgebras
 open import Categories.NaturalTransformation
 open import Category.Instance.AmbientCategory using (Ambient)
+open import Data.Product using (∃-syntax; _,_; Σ-syntax)
 ```
 -->
 ```agda
@@ -232,12 +233,50 @@ and second that `extend f` is the unique morphism satisfying the commutative dia
       ▷∘extendʳ : extend' f ∘ ▷ ≈ extend' (▷ ∘ f)
       ▷∘extendʳ = (sym ▷∘extend-comm) ○ ▷∘extendˡ
 
+    is-guarded : ∀ {X Y} (g : X ⇒ D₀ (Y + X)) → Set (ℓ ⊔ e)
+    is-guarded {X} {Y} g = ∃[ h ] (i₁ +₁ idC) ∘ h ≈ out ∘ g
+
+    guarded-unique : ∀ {X Y} (g : X ⇒ D₀ (Y + X)) (f i : X ⇒ D₀ Y) → is-guarded g → f ≈ extend' ([ now , f ]) ∘ g → i ≈ extend' ([ now , i ]) ∘ g → f ≈ i
+    guarded-unique {X} {Y} g f i (h , guarded) eqf eqi = begin 
+      f ≈⟨ eqf ⟩ 
+      extend' ([ now , f ]) ∘ g ≈⟨ (sym (Terminal.!-unique (coalgebras Y) (record { f = extend' ([ now , f ]) ; commutes = begin 
+        out ∘ extend' ([ now , f ]) ≈⟨ extendlaw ([ now , f ]) ⟩ 
+        [ out ∘ [ now , f ] , i₂ ∘ extend' ([ now , f ]) ] ∘ out ≈⟨ ([]-cong₂ ∘[] refl) ⟩∘⟨refl ⟩ 
+        [ [ out ∘ now , out ∘ f ] , i₂ ∘ extend' ([ now , f ]) ] ∘ out ≈⟨ ([]-cong₂ ([]-cong₂ unitlaw (helper f eqf)) refl) ⟩∘⟨refl ⟩
+        [ [ i₁ , (idC +₁ extend' ([ now , f ])) ∘ h ] , i₂ ∘ extend' ([ now , f ]) ] ∘ out ≈˘⟨ ([]-cong₂ ([]-cong₂ identityʳ refl) refl) ⟩∘⟨refl ⟩
+        [ [ i₁ ∘ idC , (idC +₁ extend' ([ now , f ])) ∘ h ] , i₂ ∘ extend' ([ now , f ]) ] ∘ out ≈˘⟨ ([]-cong₂ ([]-cong₂ +₁∘i₁ refl) refl) ⟩∘⟨refl ⟩ 
+        [ [ (idC +₁ extend' ([ now , f ])) ∘ i₁ , (idC +₁ extend' ([ now , f ])) ∘ h ] , i₂ ∘ extend' ([ now , f ]) ] ∘ out ≈˘⟨ ([]-cong₂ ∘[] +₁∘i₂) ⟩∘⟨refl ⟩ 
+        [ (idC +₁ extend' ([ now , f ])) ∘ [ i₁ , h ] , (idC +₁ extend' ([ now , f ])) ∘ i₂ ] ∘ out ≈˘⟨ pullˡ ∘[] ⟩ 
+        (idC +₁ extend' ([ now , f ])) ∘ [ [ i₁ , h ] , i₂ ] ∘ out ∎ }))) ⟩∘⟨refl ⟩ 
+      u (Terminal.! (coalgebras Y)) ∘ g ≈⟨ (Terminal.!-unique (coalgebras Y) (record { f = extend' ([ now , i ]) ; commutes = begin 
+        out ∘ extend' ([ now , i ]) ≈⟨ extendlaw ([ now , i ]) ⟩ 
+        [ out ∘ [ now , i ] , i₂ ∘ extend' ([ now , i ]) ] ∘ out ≈⟨ ([]-cong₂ ∘[] refl) ⟩∘⟨refl ⟩ 
+        [ [ out ∘ now , out ∘ i ] , i₂ ∘ extend' ([ now , i ]) ] ∘ out ≈⟨ ([]-cong₂ ([]-cong₂ unitlaw (helper i eqi)) refl) ⟩∘⟨refl ⟩ 
+        [ [ i₁ , (idC +₁ extend' ([ now , i ])) ∘ h ] , i₂ ∘ extend' ([ now , i ]) ] ∘ out ≈˘⟨ ([]-cong₂ ([]-cong₂ identityʳ refl) refl) ⟩∘⟨refl ⟩
+        [ [ i₁ ∘ idC , (idC +₁ extend' ([ now , i ])) ∘ h ] , i₂ ∘ extend' ([ now , i ]) ] ∘ out ≈˘⟨ ([]-cong₂ ([]-cong₂ +₁∘i₁ refl) refl) ⟩∘⟨refl ⟩ 
+        [ [ (idC +₁ extend' ([ now , i ])) ∘ i₁ , (idC +₁ extend' ([ now , i ])) ∘ h ] , i₂ ∘ extend' ([ now , i ]) ] ∘ out ≈˘⟨ ([]-cong₂ ∘[] +₁∘i₂) ⟩∘⟨refl ⟩ 
+        [ (idC +₁ extend' ([ now , i ])) ∘ [ i₁ , h ] , (idC +₁ extend' ([ now , i ])) ∘ i₂ ] ∘ out ≈˘⟨ pullˡ ∘[] ⟩ 
+        (idC +₁ extend' ([ now , i ])) ∘ [ [ i₁ , h ] , i₂ ] ∘ out ∎ })) ⟩∘⟨refl ⟩ 
+      extend' ([ now , i ]) ∘ g ≈⟨ sym eqi ⟩ 
+      i ∎
+      where
+        helper : ∀ (f : X ⇒ D₀ Y) → f ≈ extend' ([ now , f ]) ∘ g → out ∘ f ≈ (idC +₁ extend' ([ now , f ])) ∘ h
+        helper f eqf = begin 
+          out ∘ f ≈⟨ refl⟩∘⟨ eqf ⟩ 
+          out ∘ extend' ([ now , f ]) ∘ g ≈⟨ pullˡ (extendlaw ([ now , f ])) ⟩
+          ([ out ∘ [ now , f ] , i₂ ∘ extend' ([ now , f ]) ] ∘ out) ∘ g ≈⟨ pullʳ (sym guarded) ⟩
+          [ out ∘ [ now , f ] , i₂ ∘ extend' ([ now , f ]) ] ∘ (i₁ +₁ idC) ∘ h ≈⟨ pullˡ []∘+₁ ⟩
+          [ (out ∘ [ now , f ]) ∘ i₁ , (i₂ ∘ extend' ([ now , f ])) ∘ idC ] ∘ h ≈⟨ ([]-cong₂ (pullʳ inject₁) identityʳ) ⟩∘⟨refl ⟩
+          [ out ∘ now , i₂ ∘ extend' ([ now , f ]) ] ∘ h ≈⟨ ([]-cong₂ (unitlaw ○ sym identityʳ) refl) ⟩∘⟨refl ⟩
+          (idC +₁ extend' ([ now , f ])) ∘ h ∎
+
     out-law : ∀ {X Y} (f : X ⇒ Y) → out {Y} ∘ extend' (now ∘ f) ≈ (f +₁ extend' (now ∘ f)) ∘ out {X}
     out-law {X} {Y} f = begin 
       out ∘ extend' (now ∘ f)                          ≈⟨ extendlaw (now ∘ f) ⟩ 
       [ out ∘ now ∘ f , i₂ ∘ extend' (now ∘ f) ] ∘ out ≈⟨ ([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl ⟩
       (f +₁ extend' (now ∘ f)) ∘ out                   ∎
 
+
     kleisli : KleisliTriple C
     kleisli = record
       { F₀ = D₀