stuck on final proof for stability

2024-05-31 07:28:34 +02:00 · 2024-02-02 17:59:59 +01:00 · 2024-02-02 17:59:59 +01:00 · b31d3e2540
commit b31d3e2540
parent 75e61fcc33
2 changed files with 89 additions and 25 deletions
--- a/agda/src/Algebra/Elgot/Properties.lagda.md
+++ b/agda/src/Algebra/Elgot/Properties.lagda.md
@ -26,10 +26,11 @@ module Algebra.Elgot.Properties {o ℓ e} {C : Category o ℓ e} (distributive :
  open Category C
  open HomReasoning
  open Equiv
+  open MR C
  open Distributive distributive
  open import Categories.Category.Distributive.Properties distributive
  open Cartesian cartesian
-  open BinaryProducts products
+  open BinaryProducts products hiding (η) renaming (unique to ⟨⟩-unique)
  open Cocartesian cocartesian
  ccc : CartesianClosed C
  ccc = record { cartesian = cartesian ; exp = expos }
@ -39,19 +40,43 @@ module Algebra.Elgot.Properties {o ℓ e} {C : Category o ℓ e} (distributive :
  open import Category.Construction.ElgotAlgebras {C = C}
  open Cat cocartesian
  open Exponentials distributive expos
+  open import Algebra.Elgot cocartesian
  open import Algebra.Elgot.Free cocartesian
  open import Algebra.Elgot.Stable distributive

  open CartesianClosed Elgot-CCC using () renaming (λg to λg#; _^_ to _^#_)

+  open Elgot-Algebra-Morphism renaming (h to <_>)
+
  stable : ∀ {Y} (fe : FreeElgotAlgebra Y) → IsStableFreeElgotAlgebraˡ fe
-  IsStableFreeElgotAlgebraˡ.[_,_]♯ˡ (stable {Y} fe) {X} A f = (eval′ ∘ (Elgot-Algebra-Morphism.h ((fe FreeObject.*) {A = B^A-Helper {A} {X}} (λg f)) ⁂ id))
+  IsStableFreeElgotAlgebraˡ.[_,_]♯ˡ (stable {Y} fe) {X} A f = (eval′ ∘ (< FreeObject._* fe {B^A-Helper {A} {X}} (λg f) > ⁂ id))
+    where open FreeObject fe
  IsStableFreeElgotAlgebraˡ.♯ˡ-law (stable {Y} fe) {X} {A} f = sym (begin 
-    {! [ stable fe , A ]♯ˡ f ∘ (η fe ⁂ id) !} ≈⟨ {!   !} ⟩ 
-    {!   !} ≈⟨ {!   !} ⟩ 
-    {!   !} ≈⟨ {!   !} ⟩ 
-    {!   !} ≈⟨ {!   !} ⟩ 
+    (eval′ ∘ (< (λg f)* > ⁂ id)) ∘ (η ⁂ id) ≈⟨ pullʳ ⁂∘⁂ ⟩ 
+    eval′ ∘ ((< (λg f)* > ∘ η) ⁂ id ∘ id)   ≈⟨ refl⟩∘⟨ (⁂-cong₂ (*-lift (λg f)) identity²) ⟩ 
+    eval′ ∘ (λg f ⁂ id)                     ≈⟨ β′ ⟩ 
    f                                       ∎)
-  IsStableFreeElgotAlgebraˡ.♯ˡ-preserving (stable {Y} fe) {X} {B} f {Z} h = {!   !}
-  IsStableFreeElgotAlgebraˡ.♯ˡ-unique (stable {Y} fe) {X} {B} f g eq₁ eq₂ = {!   !}
+    where open FreeObject fe
+  IsStableFreeElgotAlgebraˡ.♯ˡ-preserving (stable {Y} fe) {X} {B} f {Z} h = begin 
+    (eval′ ∘ (< (λg f)* > ⁂ id)) ∘ (h #ʸ ⁂ id)                                              ≈⟨ pullʳ ⁂∘⁂ ⟩ 
+    eval′ ∘ (< (λg f)* > ∘ h #ʸ ⁂ id ∘ id)                                                  ≈⟨ refl⟩∘⟨ (⁂-cong₂ (preserves ((λg f)*)) identity²) ⟩ 
+    eval′ ∘ (λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((< (λg f)* > +₁ id) ∘ h ⁂ id)) #ᵇ) ⁂ id) ≈⟨ β′ ⟩ 
+    ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((< (λg f)* > +₁ id) ∘ h ⁂ id)) #ᵇ                     ≈˘⟨ #ᵇ-resp-≈ (refl⟩∘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²)) ⟩ 
+    ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((< (λg f)* > +₁ id) ⁂ id) ∘ (h ⁂ id)) #ᵇ              ≈⟨ #ᵇ-resp-≈ (refl⟩∘⟨ pullˡ (sym (distributeʳ⁻¹-natural id < (λg f) * > id))) ⟩ 
+    ((eval′ +₁ id) ∘ ((< (λg f)* > ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹) ∘ (h ⁂ id)) #ᵇ         ≈⟨ #ᵇ-resp-≈ (refl⟩∘⟨ assoc ○ pullˡ (+₁∘+₁ ○ +₁-cong₂ refl (elimʳ (⟨⟩-unique id-comm id-comm)))) ⟩ 
+    ((eval′ ∘ (< (λg f)* > ⁂ id) +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) #ᵇ                      ∎
+    where 
+      open FreeObject fe renaming (FX to KY)
+      open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-resp-≈ to #ᵇ-resp-≈)
+      open Elgot-Algebra KY using () renaming (_# to _#ʸ)
+  IsStableFreeElgotAlgebraˡ.♯ˡ-unique (stable {Y} fe) {X} {B} f g eq₁ eq₂ = sym (begin 
+    eval′ ∘ (< (λg f)* > ⁂ id)              ≈⟨ refl⟩∘⟨ (⁂-cong₂ (*-cong (λ-cong eq₁)) refl) ⟩ 
+    eval′ ∘ (< (λg (g ∘ (η ⁂ id)))* > ⁂ id) ≈˘⟨ refl⟩∘⟨ (⁂-cong₂ (*-cong subst) refl) ⟩ 
+    eval′ ∘ (< (λg g ∘ η)* > ⁂ id)          ≈˘⟨ refl⟩∘⟨ (⁂-cong₂ (*-uniq (λg g ∘ η) (record { h = λg g ; preserves = {!   !} }) refl) refl) ⟩ 
+    eval′ ∘ (λg g ⁂ id)                     ≈⟨ β′ ⟩ 
+    g                                       ∎)
+    where 
+      open FreeObject fe renaming (FX to KY)
+      open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-resp-≈ to #ᵇ-resp-≈)
+      open Elgot-Algebra KY using () renaming (_# to _#ʸ)
 ```
--- a/agda/src/Category/Construction/ElgotAlgebras.lagda.md
+++ b/agda/src/Category/Construction/ElgotAlgebras.lagda.md
@ -314,7 +314,7 @@ module Category.Construction.ElgotAlgebras {o ℓ e} {C : Category o ℓ e} wher
          [ (id +₁ i₁) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ≈˘⟨ cancelʳ (IsIso.isoˡ isIsoʳ) ⟩ 
          ([ (id +₁ i₁) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ∘ distributeʳ⁻¹) ∘ distributeʳ ∎)

-    <_> = Elgot-Algebra-Morphism.h
+    open Elgot-Algebra-Morphism renaming (h to <_>)

    cccc : CanonicalCartesianClosed Elgot-Algebras
    CanonicalCartesianClosed.⊤ cccc = Terminal.⊤ Terminal-Elgot-Algebras
@ -366,21 +366,60 @@ module Category.Construction.ElgotAlgebras {o ℓ e} {C : Category o ℓ e} wher
            (eval′ +₁ id) ∘ (i₂ ∘ (id ⁂ id)) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ pullˡ (pullˡ inject₂) ⟩ 
            ((i₂ ∘ id) ∘ (id ⁂ id)) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ (cancelʳ (identityˡ ○ ⟨⟩-unique id-comm id-comm)) ⟩∘⟨refl ⟩ 
            i₂ ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ∎
-    Elgot-Algebra-Morphism.h (CanonicalCartesianClosed.curry cccc {A} {B} {C} f) = λg < f >
-    Elgot-Algebra-Morphism.preserves (CanonicalCartesianClosed.curry cccc {A} {B} {C} f) {X} {g} = λ-unique′ (begin 
-      eval′ ∘ ((λg < f > ∘ (Elgot-Algebra._# A) g) ⁂ id) ≈⟨ refl⟩∘⟨ ⁂-cong₂ subst refl ⟩ 
-      eval′ ∘ ((λg (< f > ∘ (((Elgot-Algebra._# A) g) ⁂ id))) ⁂ id) ≈⟨ β′ ⟩ 
-      < f > ∘ (((Elgot-Algebra._# A) g) ⁂ id) ≈⟨ {!   !} ⟩ 
+    < CanonicalCartesianClosed.curry cccc {A} {B} {C} f > = λg < f >
+    preserves (CanonicalCartesianClosed.curry cccc {A} {B} {C} f) {X} {g} = begin 
+      λg < f > ∘ g #ᵃ ≈⟨ subst ⟩ 
+      λg (< f > ∘ (g #ᵃ ⁂ id)) ≈⟨ {!   !} ⟩ 
      {!   !} ≈⟨ {!   !} ⟩ 
-      {!   !} ≈˘⟨ {!   !} ⟩ 
-      {!   !} ≈˘⟨ {!   !} ⟩ 
-      {!   !} ≈˘⟨ {!   !} ⟩ 
-      < f > ∘ ⟨ [ id , (Elgot-Algebra._# A) ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) ] ∘ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) ] ∘ ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) ⟩ ≈˘⟨ refl⟩∘⟨ (⟨⟩-cong₂ (Elgot-Algebra.#-Fixpoint A) (Elgot-Algebra.#-Fixpoint B)) ⟩ 
-      < f > ∘ ⟨ (Elgot-Algebra._# A) ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) ⟩ ≈⟨ Elgot-Algebra-Morphism.preserves f ⟩ 
-      (Elgot-Algebra._# C) ((< f > +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) ≈˘⟨ {!   !} ⟩ 
-      (Elgot-Algebra._# C) ((eval′ +₁ id) ∘ (((λg < f > ⁂ id) +₁ (id ⁂ id)) ∘ distributeʳ⁻¹) ∘ (g ⁂ id)) ≈˘⟨ Elgot-Algebra.#-resp-≈ C (refl⟩∘⟨ (pullˡ (sym (distributeʳ⁻¹-natural id (λg < f >) id)))) ⟩ 
-      (Elgot-Algebra._# C) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((λg < f > +₁ id) ⁂ id) ∘ (g ⁂ id)) ≈⟨ Elgot-Algebra.#-resp-≈ C (refl⟩∘⟨ (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²))) ⟩ 
-      (Elgot-Algebra._# C) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((λg < f > +₁ id) ∘ g) ⁂ id)) ∎)
+      {!   !} ≈⟨ {!   !} ⟩ 
+      λg (< f > ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩) ≈⟨ λ-cong (preserves f) ⟩ 
+      λg (((< f > +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) #ᶜ) ≈⟨ {!   !} ⟩ 
+      {!   !} ≈⟨ {!   !} ⟩ 
+      {!   !} ≈⟨ {!   !} ⟩ 
+      λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((λg < f > +₁ id) ∘ g) ⁂ id)) #ᶜ) ∎
+      where
+      open Elgot-Algebra A using () renaming (_# to _#ᵃ; #-Uniformity to #ᵃ-Uniformity)
+      open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity)
+      open Elgot-Algebra C using () renaming (_# to _#ᶜ; #-resp-≈ to #ᶜ-resp-≈)
+    -- Elgot-Algebra-Morphism.preserves (CanonicalCartesianClosed.curry cccc {A} {B} {C} f) {X} {g} = λ-unique′ (begin 
+    --   eval′ ∘ ((λg < f > ∘ g #ᵃ) ⁂ id) ≈⟨ refl⟩∘⟨ ⁂-cong₂ subst refl ⟩ 
+    --   eval′ ∘ ((λg (< f > ∘ (g #ᵃ ⁂ id))) ⁂ id) ≈⟨ β′ ⟩ 
+    --   < f > ∘ (g #ᵃ ⁂ id) ≈⟨ refl⟩∘⟨ (⟨⟩-unique by-π₁ by-π₂) ⟩ 
+    --   < f > ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩ ≈⟨ Elgot-Algebra-Morphism.preserves f ⟩ 
+    --   ((< f > +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) #ᶜ ≈˘⟨ #ᶜ-resp-≈ (refl⟩∘⟨ assoc ○ pullˡ (+₁∘+₁ ○ +₁-cong₂ β′ (elimʳ (⟨⟩-unique id-comm id-comm)))) ⟩ 
+    --   ((eval′ +₁ id) ∘ (((λg < f > ⁂ id) +₁ (id ⁂ id)) ∘ distributeʳ⁻¹) ∘ (g ⁂ id)) #ᶜ ≈˘⟨ Elgot-Algebra.#-resp-≈ C (refl⟩∘⟨ (pullˡ (sym (distributeʳ⁻¹-natural id (λg < f >) id)))) ⟩ 
+    --   ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((λg < f > +₁ id) ⁂ id) ∘ (g ⁂ id)) #ᶜ ≈⟨ Elgot-Algebra.#-resp-≈ C (refl⟩∘⟨ (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²))) ⟩ 
+    --   ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((λg < f > +₁ id) ∘ g) ⁂ id)) #ᶜ ∎)
+    --   where
+    --   open Elgot-Algebra A using () renaming (_# to _#ᵃ; #-Uniformity to #ᵃ-Uniformity)
+    --   open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity)
+    --   open Elgot-Algebra C using () renaming (_# to _#ᶜ; #-resp-≈ to #ᶜ-resp-≈)
+    --   by-π₁ : π₁ ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩ ≈ g #ᵃ ∘ π₁
+    --   by-π₁ = project₁ ○ #ᵃ-Uniformity by-uni
+    --     where
+    --     by-uni : (id +₁ π₁) ∘ (π₁ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id) ≈ g ∘ π₁
+    --     by-uni = begin 
+    --       (id +₁ π₁) ∘ (π₁ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩ 
+    --       (π₁ +₁ π₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ id) ≈⟨ pullˡ distributeʳ⁻¹-π₁ ⟩ 
+    --       π₁ ∘ (g ⁂ id) ≈⟨ project₁ ⟩ 
+    --       g ∘ π₁ ∎
+    --   by-π₂ : π₂ ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩ ≈ id ∘ π₂
+    --   by-π₂ = begin 
+    --     π₂ ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩ ≈⟨ project₂ ⟩ 
+    --     ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ≈⟨ #ᵇ-Uniformity by-uni ⟩ 
+    --     {!   !} #ᵇ ∘ π₂ ≈⟨ {!   !} ⟩ 
+    --     {!   !} ≈⟨ {!   !} ⟩ 
+    --     {!   !} ≈⟨ {!   !} ⟩ 
+    --     {!   !} ≈⟨ {!   !} ⟩ 
+    --     id ∘ π₂ ∎
+    --     where 
+    --     by-uni : (id +₁ π₂) ∘ (π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)) ≈ {!   !} ∘ π₂
+    --     by-uni = begin 
+    --       {!   !} ≈⟨ {!   !} ⟩ 
+    --       {!   !} ≈⟨ {!   !} ⟩ 
+    --       {!   !} ≈⟨ {!   !} ⟩ 
+    --       {!   !} ≈⟨ {!   !} ⟩ 
+    --       {!   !} ∎
    CanonicalCartesianClosed.eval-comp cccc {A} {B} {C} {f} = β′
    CanonicalCartesianClosed.curry-unique cccc {A} {B} {C} {f} {g} eq = λ-unique′ eq