From 96578640925d4cff4b8f40e45cf37edc92937eeb Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Fri, 8 Sep 2023 21:21:54 +0200 Subject: [PATCH] Finished extend congruence proof --- src/FinalCoalgebras.lagda.md | 41 +++++++++++++++++++++++ src/Monad/Instance/Delay.lagda.md | 54 ++++++++++++++++--------------- 2 files changed, 69 insertions(+), 26 deletions(-) create mode 100644 src/FinalCoalgebras.lagda.md diff --git a/src/FinalCoalgebras.lagda.md b/src/FinalCoalgebras.lagda.md new file mode 100644 index 0000000..afbfa6b --- /dev/null +++ b/src/FinalCoalgebras.lagda.md @@ -0,0 +1,41 @@ +```agda +open import Level +open import Categories.Category +open import Categories.Functor +import Categories.Morphism as M +import Categories.Morphism.Reasoning as MR + +module FinalCoalgebras {o ℓ e} {C : Category o ℓ e} (F : Endofunctor C) where +open Category C renaming (id to idC) +open import Categories.Object.Terminal +open import Categories.Functor.Coalgebra +open import Categories.Category.Construction.F-Coalgebras +open Functor F +open MR C +open HomReasoning +open Equiv + +lemma : ∀ {X} → {f g : X ⇒ F₀ X} → f ≈ g → (terminal : Terminal (F-Coalgebras F)) → F-Coalgebra-Morphism.f (Terminal.! terminal {A = (to-Coalgebra f)}) ≈ F-Coalgebra-Morphism.f (Terminal.! terminal {A = (to-Coalgebra g)}) +lemma {X} {f} {g} eq terminal = begin + F-Coalgebra-Morphism.f (Terminal.! terminal) ≈⟨ Terminal.!-unique terminal (record + { f = F-Coalgebra-Morphism.f (Terminal.! terminal {A = (to-Coalgebra g)}) ∘ F-Coalgebra-Morphism.f from + ; commutes = begin + F-Coalgebra.α (Terminal.⊤ terminal) ∘ F-Coalgebra-Morphism.f (IsTerminal.! (Terminal.⊤-is-terminal terminal)) ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ○ F-Coalgebra-Morphism.commutes (Terminal.! terminal) ⟩ + F₁ (F-Coalgebra-Morphism.f (Terminal.! terminal)) ∘ g ≈⟨ refl⟩∘⟨ ⟺ eq ⟩ + F₁ (F-Coalgebra-Morphism.f (Terminal.! terminal)) ∘ f ≈˘⟨ F-resp-≈ identityʳ ⟩∘⟨refl ⟩ + F₁ (F-Coalgebra-Morphism.f (Terminal.! terminal) ∘ idC) ∘ f ∎ + }) ⟩ + F-Coalgebra-Morphism.f (Terminal.! terminal) ∘ idC ≈⟨ identityʳ ⟩ + F-Coalgebra-Morphism.f (Terminal.! terminal) ∎ + where + eq' : M._≅_ (F-Coalgebras F) (to-Coalgebra f) (to-Coalgebra g) + eq' = record + { from = record { f = idC ; commutes = id-comm ○ ⟺ identity ⟩∘⟨ ⟺ eq } + ; to = record { f = idC ; commutes = id-comm ○ ⟺ identity ⟩∘⟨ eq } + ; iso = record + { isoˡ = identity² + ; isoʳ = identity² + } + } + open M._≅_ eq' +``` \ No newline at end of file diff --git a/src/Monad/Instance/Delay.lagda.md b/src/Monad/Instance/Delay.lagda.md index 7cf811c..4044ba6 100644 --- a/src/Monad/Instance/Delay.lagda.md +++ b/src/Monad/Instance/Delay.lagda.md @@ -20,6 +20,7 @@ open import Categories.Functor.Algebra open import Categories.Monad.Construction.Kleisli open import Categories.Category.Construction.F-Coalgebras open import Categories.NaturalTransformation +open import FinalCoalgebras import Categories.Morphism as M import Categories.Morphism.Reasoning as MR ``` @@ -92,7 +93,6 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ coit-commutes : ∀ (f : Y ⇒ X + Y) → out ∘ (coit f) ≈ (idC +₁ coit f) ∘ f coit-commutes f = F-Coalgebra-Morphism.commutes (! {A = record { A = Y ; α = f }}) - monad : Monad C monad = Kleisli⇒Monad C (record { F₀ = D₀ @@ -119,31 +119,14 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ (idC +₁ extend (now X)) ∘ out X ∎ }) ; assoc = {! !} ; sym-assoc = {! !} - ; extend-≈ = λ {X} {Y} {f} {g} eq → {! !} - - -- begin - -- extend f ≈⟨ sym (Terminal.!-unique (algebras Y) (record { f = extend f ; commutes = F-Coalgebra-Morphism.commutes {! !} })) ⟩ - -- F-Coalgebra-Morphism.f ((Terminal.! (algebras Y) {A = alg' {X} {Y}})) ≈˘⟨ sym (Terminal.!-unique (algebras Y) (record { f = extend g ; commutes = {! !} })) ⟩ - -- extend g ∎ - - -- let - -- h : F-Coalgebra-Morphism (alg f) (alg g) - -- h = record { f = idC ; commutes = begin - -- F-Coalgebra.α (alg g) ∘ idC ≈⟨ id-comm ⟩ - -- idC ∘ F-Coalgebra.α (alg g) ≈⟨ refl⟩∘⟨ []-cong₂ (([]-cong₂ (refl⟩∘⟨ (refl⟩∘⟨ (sym eq))) refl) ⟩∘⟨refl) refl ⟩ - -- idC ∘ F-Coalgebra.α (alg f) ≈˘⟨ ([]-cong₂ identityʳ identityʳ ○ +-η) ⟩∘⟨refl ⟩ - -- (idC +₁ idC) ∘ F-Coalgebra.α (alg f) ∎ } - -- x : F-Coalgebra-Morphism (alg f) (Terminal.⊤ (algebras Y)) - -- x = (F-Coalgebras (delayF Y)) [ Terminal.! (algebras Y) ∘ h ] - -- in Terminal.!-unique₂ (algebras Y) {f = Terminal.! (algebras Y)} {g = {! !} } ⟩∘⟨refl - - -- extend f ≈⟨ insertˡ (_≅_.isoˡ (out-≅ Y)) ⟩ - -- out⁻¹ Y ∘ out Y ∘ extend f ≈⟨ refl⟩∘⟨ pullˡ (F-Coalgebra-Morphism.commutes (Terminal.! (algebras Y) {A = alg f})) ⟩ - -- out⁻¹ Y ∘ ((idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras Y)))) ∘ [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ]) ∘ i₁ ≈⟨ refl⟩∘⟨ ((+₁-cong₂ refl (Terminal.!-unique₂ (algebras Y) {f = Terminal.! (algebras Y) {A = alg f}} {g = Terminal.! (algebras Y) {A = alg f}}) ⟩∘⟨ ([]-cong₂ (([]-cong₂ (refl⟩∘⟨ (refl⟩∘⟨ eq)) refl) ⟩∘⟨refl) refl)) ⟩∘⟨refl) ⟩ - -- out⁻¹ Y ∘ ((idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras Y)))) ∘ [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ g) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ]) ∘ i₁ ≈⟨ refl⟩∘⟨ (((+₁-cong₂ refl (Terminal.!-unique₂ (algebras Y) {f = Terminal.! (algebras Y)} {g = record { f = F-Coalgebra-Morphism.f (Terminal.! (algebras Y)) ; commutes = {! !} }})) ⟩∘⟨refl) ⟩∘⟨refl) ⟩ - -- out⁻¹ Y ∘ ((idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras Y)))) ∘ [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ g) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ]) ∘ i₁ ≈˘⟨ refl⟩∘⟨ pullˡ (F-Coalgebra-Morphism.commutes (Terminal.! (algebras Y) {A = alg g})) ⟩ - -- out⁻¹ Y ∘ out Y ∘ extend g ≈˘⟨ insertˡ (_≅_.isoˡ (out-≅ Y)) ⟩ - -- extend g ∎ + ; extend-≈ = λ {X} {Y} {f} {g} eq → begin + F-Coalgebra-Morphism.f (Terminal.! (algebras Y) {A = alg f }) ∘ i₁ {B = D₀ Y} ≈⟨ (Terminal.!-unique (algebras Y) (record { f = (F-Coalgebra-Morphism.f (Terminal.! (algebras Y) {A = alg g }) ∘ idC) ; commutes = begin + F-Coalgebra.α (Terminal.⊤ (algebras Y)) ∘ F-Coalgebra-Morphism.f (Terminal.! (algebras Y)) ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩ + F-Coalgebra.α (Terminal.⊤ (algebras Y)) ∘ F-Coalgebra-Morphism.f (Terminal.! (algebras Y)) ≈⟨ F-Coalgebra-Morphism.commutes (Terminal.! (algebras Y)) ⟩ + Functor.F₁ (delayF Y) (F-Coalgebra-Morphism.f (Terminal.! (algebras Y))) ∘ F-Coalgebra.α (alg g) ≈˘⟨ (Functor.F-resp-≈ (delayF Y) identityʳ) ⟩∘⟨ (αf≈αg eq) ⟩ + Functor.F₁ (delayF Y) (F-Coalgebra-Morphism.f (Terminal.! (algebras Y)) ∘ idC) ∘ F-Coalgebra.α (alg f) ∎ })) ⟩∘⟨refl ⟩ + (F-Coalgebra-Morphism.f (Terminal.! (algebras Y) {A = alg g }) ∘ idC) ∘ i₁ {B = D₀ Y} ≈⟨ identityʳ ⟩∘⟨refl ⟩ + extend g ∎ }) where alg' : ∀ {X Y} → F-Coalgebra (delayF Y) @@ -169,6 +152,25 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ [ [ i₁ ∘ idC , (i₂ ∘ (F-Coalgebra-Morphism.f !)) ∘ i₂ ] ∘ (out Y ∘ f) , (i₂ ∘ (F-Coalgebra-Morphism.f !)) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ (elimˡ (([]-cong₂ identityʳ (cancelʳ !∘i₂)) ○ +-η)) assoc) ⟩∘⟨refl ⟩ [ out Y ∘ f , i₂ ∘ extend ] ∘ out X ∎ + αf≈αg : ∀ {X Y} {f g : X ⇒ D₀ Y} → f ≈ g → F-Coalgebra.α (alg f) ≈ F-Coalgebra.α (alg g) + αf≈αg {X} {Y} {f} {g} eq = []-cong₂ ([]-cong₂ (refl⟩∘⟨ refl⟩∘⟨ eq) refl ⟩∘⟨refl) refl + alg-f≈alg-g : ∀ {X Y} {f g : X ⇒ D₀ Y} → f ≈ g → M._≅_ (F-Coalgebras (delayF Y)) (alg f) (alg g) + alg-f≈alg-g {X} {Y} {f} {g} eq = record + { from = record { f = idC ; commutes = begin + F-Coalgebra.α (alg g) ∘ idC ≈⟨ identityʳ ⟩ + F-Coalgebra.α (alg g) ≈⟨ ⟺ (αf≈αg eq) ⟩ + F-Coalgebra.α (alg f) ≈˘⟨ elimˡ (Functor.identity (delayF Y)) ⟩ + Functor.F₁ (delayF Y) idC ∘ F-Coalgebra.α (alg f) ∎ } + ; to = record { f = idC ; commutes = begin + F-Coalgebra.α (alg f) ∘ idC ≈⟨ identityʳ ⟩ + F-Coalgebra.α (alg f) ≈⟨ αf≈αg eq ⟩ + F-Coalgebra.α (alg g) ≈˘⟨ elimˡ (Functor.identity (delayF Y)) ⟩ + Functor.F₁ (delayF Y) idC ∘ F-Coalgebra.α (alg g) ∎ } + ; iso = record + { isoˡ = identity² + ; isoʳ = identity² + } + } ``` ### Old definitions: