From 7986abb1343f9eaec21641cc7d9a07dcfd97921b Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Mon, 4 Mar 2024 17:09:22 +0100 Subject: [PATCH] improve proofs --- .../ElgotAlgebras/Exponentials.lagda.md | 142 +++++++++--------- 1 file changed, 71 insertions(+), 71 deletions(-) diff --git a/agda/src/Category/Construction/ElgotAlgebras/Exponentials.lagda.md b/agda/src/Category/Construction/ElgotAlgebras/Exponentials.lagda.md index 7704532..586e5c2 100644 --- a/agda/src/Category/Construction/ElgotAlgebras/Exponentials.lagda.md +++ b/agda/src/Category/Construction/ElgotAlgebras/Exponentials.lagda.md @@ -41,77 +41,77 @@ module Category.Construction.ElgotAlgebras.Exponentials {o ℓ e} {C : Category open import Algebra.Elgot cocartesian open import Category.Construction.ElgotAlgebras cocartesian open import Category.Construction.ElgotAlgebras.Products cocartesian cartesian + open Elgot-Algebra using (algebra) renaming (A to ∣_∣) + open Elgot-Algebra-on using (#-Fixpoint; #-Uniformity; #-Folding; #-resp-≈) renaming (_# to [_,_]#) - Exponential-Elgot-Algebra : ∀ {EA : Elgot-Algebra} {X : Obj} → Elgot-Algebra - Exponential-Elgot-Algebra {EA} {X} = record - { A = A ^ X - ; algebra = record - { _# = λ {Z} f → λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) - ; #-Fixpoint = λ {X} {f} → begin - λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) ≈⟨ λ-cong #ᵃ-Fixpoint ⟩ - λg ([ id , ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ ] ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) ≈⟨ λ-cong ((pullˡ []∘+₁) ○ ([]-cong₂ identityˡ identityʳ) ⟩∘⟨refl) ⟩ - λg ([ eval′ , ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ ] ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) ≈˘⟨ λ-unique′ (begin - eval′ ∘ (([ id , λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) ] ∘ f) ⁂ id) ≈˘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²) ⟩ - eval′ ∘ ([ id , λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) ] ⁂ id) ∘ (f ⁂ id) ≈⟨ refl⟩∘⟨ (⟨⟩-unique (begin - π₁ ∘ [ id , (λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ)) ⁂ id ] ∘ distributeʳ⁻¹ ≈⟨ pullˡ (∘[] ○ []-cong₂ id-comm π₁∘⁂) ⟩ - [ id ∘ π₁ , (λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ)) ∘ π₁ ] ∘ distributeʳ⁻¹ ≈˘⟨ pullˡ []∘+₁ ⟩ - [ id , (λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ)) ] ∘ (π₁ +₁ π₁) ∘ distributeʳ⁻¹ ≈⟨ refl⟩∘⟨ distributeʳ⁻¹-π₁ ⟩ - [ id , λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) ] ∘ π₁ ∎) - (begin - π₂ ∘ [ id , (λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ)) ⁂ id ] ∘ distributeʳ⁻¹ ≈⟨ pullˡ (∘[] ○ []-cong₂ identityʳ (π₂∘⁂ ○ identityˡ)) ⟩ - [ π₂ , π₂ ] ∘ distributeʳ⁻¹ ≈⟨ distributeʳ⁻¹-π₂ ○ (sym identityˡ) ⟩ - id ∘ π₂ ∎) - ⟩∘⟨refl) ⟩ - eval′ ∘ ([ id , (λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ)) ⁂ id ] ∘ distributeʳ⁻¹) ∘ (f ⁂ id) ≈⟨ pullˡ (pullˡ ∘[]) ⟩ - ([ eval′ ∘ id , eval′ ∘ ((λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ)) ⁂ id) ] ∘ distributeʳ⁻¹) ∘ (f ⁂ id) ≈⟨ assoc ○ ([]-cong₂ identityʳ β′) ⟩∘⟨refl ⟩ - [ eval′ , ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ ] ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ∎) ⟩ - [ id , λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) ] ∘ f ∎ - ; #-Uniformity = #-Uniformity - ; #-Folding = #-Folding - ; #-resp-≈ = λ {Z} {f} {g} f≈g → λ-cong (#ᵃ-resp-≈ (refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ f≈g refl)) - } - } + Exponential-Elgot-Algebra : ∀ {E : Elgot-Algebra} {X : Obj} → Elgot-Algebra + + ∣ Exponential-Elgot-Algebra {E} {X} ∣ = ∣ E ∣ ^ X + + [ algebra (Exponential-Elgot-Algebra {E} {X} ) , f ]# = λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# + + algebra (Exponential-Elgot-Algebra {E} {X}) .#-Fixpoint {Y} {f} = sym (λ-unique′ (begin + eval′ ∘ (([ id , λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# ] ∘ f) ⁂ id) ≈˘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²) ⟩ + eval′ ∘ ([ id , λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# ] ⁂ id) ∘ (f ⁂ id) ≈⟨ refl⟩∘⟨ pushˡ (⟨⟩-unique proj₁ proj₂) ⟩ + eval′ ∘ [ id , (λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]#) ⁂ id ] ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ≈⟨ pullˡ ∘[] ⟩ + [ eval′ ∘ id , eval′ ∘ ((λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]#) ⁂ id) ] ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ≈⟨ ([]-cong₂ identityʳ β′) ⟩∘⟨refl ⟩ + [ eval′ , [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# ] ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ≈˘⟨ pullˡ ([]∘+₁ ○ []-cong₂ identityˡ identityʳ) ⟩ + [ id , [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# ] ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ≈˘⟨ #-Fixpoint (algebra E) ⟩ + [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# ∎)) where - open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ; #-Fixpoint to #ᵃ-Fixpoint; #-Uniformity to #ᵃ-Uniformity; #-Folding to #ᵃ-Folding; #-resp-≈ to #ᵃ-resp-≈) - #-Uniformity : ∀ {D E} {f : D ⇒ A ^ X + D} {g : E ⇒ A ^ X + E} {h : D ⇒ E} → (id +₁ h) ∘ f ≈ g ∘ h → λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) ≈ λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) #ᵃ) ∘ h - #-Uniformity {D} {E} {f} {g} {h} eq = sym (λ-unique′ (begin - eval′ ∘ ((λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) #ᵃ) ∘ h) ⁂ id) ≈˘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identityˡ) ⟩ - eval′ ∘ ((λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) #ᵃ)) ⁂ id) ∘ (h ⁂ id) ≈⟨ pullˡ β′ ⟩ - ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) #ᵃ ∘ (h ⁂ id) ≈˘⟨ #ᵃ-Uniformity by-uni ⟩ - ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ ∎)) - where - by-uni : (id +₁ (h ⁂ id)) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ≈ ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) ∘ (h ⁂ id) - by-uni = begin - (id +₁ (h ⁂ id)) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩ - (eval′ +₁ (h ⁂ id)) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ identityˡ) ⟩ - (eval′ +₁ id) ∘ (id +₁ (h ⁂ id)) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ≈⟨ refl⟩∘⟨ pullˡ ((+₁-cong₂ (sym (⟨⟩-unique id-comm id-comm)) refl) ⟩∘⟨refl ○ distributeʳ⁻¹-natural id id h) ⟩ - (eval′ +₁ id) ∘ (distributeʳ⁻¹ ∘ ((id +₁ h) ⁂ id)) ∘ (f ⁂ id) ≈⟨ refl⟩∘⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ eq identity²) ⟩ - (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ∘ h ⁂ id) ≈˘⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ refl identity²)) ⟩ - ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) ∘ (h ⁂ id) ∎ - #-Folding : ∀ {D E} {f : D ⇒ A ^ X + D} {h : E ⇒ D + E} → λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) +₁ h) ⁂ id)) #ᵃ) ≈ λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) #ᵃ) - #-Folding {D} {E} {f} {h} = λ-cong (begin - ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) +₁ h) ⁂ id)) #ᵃ ≈⟨ #ᵃ-resp-≈ (refl⟩∘⟨ sym (distributeʳ⁻¹-natural id (λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ)) h)) ⟩ - ((eval′ +₁ id) ∘ ((λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) ⁂ id) +₁ (h ⁂ id)) ∘ distributeʳ⁻¹) #ᵃ ≈⟨ #ᵃ-resp-≈ (pullˡ (+₁∘+₁ ○ +₁-cong₂ β′ identityˡ)) ⟩ - ((((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ +₁ h ⁂ id) ∘ distributeʳ⁻¹) #ᵃ ≈⟨ #ᵃ-Uniformity by-uni₁ ⟩ - (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ +₁ distributeʳ⁻¹ ∘ (h ⁂ id)) #ᵃ ∘ distributeʳ⁻¹ ≈⟨ #ᵃ-Folding ⟩∘⟨refl ⟩ - [ ((id +₁ i₁) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) , (i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) ] #ᵃ ∘ distributeʳ⁻¹ ≈˘⟨ #ᵃ-Uniformity by-uni₂ ⟩ - ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) #ᵃ ∎) - where - by-uni₁ : (id +₁ distributeʳ⁻¹) ∘ (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ +₁ h ⁂ id) ∘ distributeʳ⁻¹ ≈ ((((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ +₁ distributeʳ⁻¹ ∘ (h ⁂ id))) ∘ distributeʳ⁻¹ - by-uni₁ = begin - (id +₁ distributeʳ⁻¹) ∘ (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ +₁ h ⁂ id) ∘ distributeʳ⁻¹ ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ refl) ⟩ - ((((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ +₁ distributeʳ⁻¹ ∘ (h ⁂ id))) ∘ distributeʳ⁻¹ ∎ - by-uni₂ : (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id) ≈ [ (id +₁ i₁) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ∘ distributeʳ⁻¹ - by-uni₂ = Iso⇒Epi (IsIso.iso isIsoʳ) ((id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) ([ (id +₁ i₁) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ∘ distributeʳ⁻¹) (begin - ((id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) ∘ distributeʳ ≈⟨ ∘[] ⟩ - [ (((id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) ∘ (i₁ ⁂ id)) , (((id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) ∘ (i₂ ⁂ id)) ] ≈⟨ []-cong₂ (pullʳ (pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ inject₁ identity²)))) (pullʳ (pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ inject₂ identity²)))) ⟩ - [ (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((id +₁ i₁) ∘ f) ⁂ id) , (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((i₂ ∘ h) ⁂ id) ] ≈⟨ []-cong₂ (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ refl identity²)) (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ refl identity²)) ⟩ - [ (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((id +₁ i₁)) ⁂ id) ∘ (f ⁂ id) , (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (i₂ ⁂ id) ∘ (h ⁂ id) ] ≈⟨ []-cong₂ (refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym (distributeʳ⁻¹-natural id id i₁))) (refl⟩∘⟨ refl⟩∘⟨ pullˡ distributeʳ⁻¹-i₂) ⟩ - [ (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ ((id ⁂ id +₁ i₁ ⁂ id) ∘ distributeʳ⁻¹) ∘ (f ⁂ id) , (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ i₂ ∘ (h ⁂ id) ] ≈⟨ []-cong₂ (pullˡ +₁∘+₁) (pullˡ +₁∘+₁) ⟩ - [ (id ∘ eval′ +₁ distributeʳ⁻¹ ∘ id) ∘ ((id ⁂ id +₁ i₁ ⁂ id) ∘ distributeʳ⁻¹) ∘ (f ⁂ id) , (id ∘ eval′ +₁ distributeʳ⁻¹ ∘ id) ∘ i₂ ∘ (h ⁂ id) ] ≈⟨ []-cong₂ (pullˡ (pullˡ +₁∘+₁)) (pullˡ +₁∘i₂) ⟩ - [ ((((id ∘ eval′) ∘ (id ⁂ id)) +₁ ((distributeʳ⁻¹ ∘ id) ∘ (i₁ ⁂ id))) ∘ distributeʳ⁻¹) ∘ (f ⁂ id) , (i₂ ∘ (distributeʳ⁻¹ ∘ id)) ∘ (h ⁂ id) ] ≈⟨ []-cong₂ (((+₁-cong₂ (identityˡ ⟩∘⟨refl) (identityʳ ⟩∘⟨refl ○ distributeʳ⁻¹-i₁)) ⟩∘⟨refl) ⟩∘⟨refl) (pullʳ (pullʳ identityˡ)) ⟩ - [ (((eval′ ∘ (id ⁂ id)) +₁ i₁) ∘ distributeʳ⁻¹) ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ≈⟨ []-cong₂ (assoc ○ (+₁-cong₂ (elimʳ (⟨⟩-unique id-comm id-comm)) refl) ⟩∘⟨refl) refl ⟩ - [ (eval′ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ≈˘⟨ []-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ)) refl ⟩ - [ (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ʳ ∎) + proj₁ : π₁ ∘ [ id , (λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]#) ⁂ id ] ∘ distributeʳ⁻¹ ≈ [ id , λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# ] ∘ π₁ + proj₁ = begin + π₁ ∘ [ id , (λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]#) ⁂ id ] ∘ distributeʳ⁻¹ ≈⟨ pullˡ ∘[] ⟩ + [ π₁ ∘ id , π₁ ∘ ((λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]#) ⁂ id) ] ∘ distributeʳ⁻¹ ≈⟨ ([]-cong₂ id-comm project₁) ⟩∘⟨refl ⟩ + [ id ∘ π₁ , λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# ∘ π₁ ] ∘ distributeʳ⁻¹ ≈˘⟨ pullˡ []∘+₁ ⟩ + [ id , λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# ] ∘ (π₁ +₁ π₁) ∘ distributeʳ⁻¹ ≈⟨ refl⟩∘⟨ distributeʳ⁻¹-π₁ ⟩ + [ id , λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# ] ∘ π₁ ∎ + proj₂ : π₂ ∘ [ id , (λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]#) ⁂ id ] ∘ distributeʳ⁻¹ ≈ id ∘ π₂ + proj₂ = begin + π₂ ∘ [ id , (λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]#) ⁂ id ] ∘ distributeʳ⁻¹ ≈⟨ pullˡ ∘[] ⟩ + [ π₂ ∘ id , π₂ ∘ ((λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]#) ⁂ id) ] ∘ distributeʳ⁻¹ ≈⟨ ([]-cong₂ identityʳ (project₂ ○ identityˡ)) ⟩∘⟨refl ⟩ + [ π₂ , π₂ ] ∘ distributeʳ⁻¹ ≈⟨ distributeʳ⁻¹-π₂ ○ sym identityˡ ⟩ + id ∘ π₂ ∎ + + algebra (Exponential-Elgot-Algebra {E} {X}) .#-Uniformity {B} {D} {f} {g} {h} eq = sym (λ-unique′ (begin + eval′ ∘ ((λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)]# ∘ h) ⁂ id) ≈˘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identityʳ) ⟩ + eval′ ∘ (λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)]# ⁂ id) ∘ (h ⁂ id) ≈⟨ pullˡ β′ ⟩ + [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)]# ∘ (h ⁂ id) ≈˘⟨ #-Uniformity (algebra E) by-uni ⟩ + [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# ∎)) + where + by-uni : (id +₁ (h ⁂ id)) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ≈ ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) ∘ (h ⁂ id) + by-uni = begin + (id +₁ (h ⁂ id)) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩ + (eval′ +₁ (h ⁂ id)) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ identityˡ) ⟩ + (eval′ +₁ id) ∘ (id +₁ (h ⁂ id)) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ≈⟨ refl⟩∘⟨ pullˡ ((+₁-cong₂ (sym (⟨⟩-unique id-comm id-comm)) refl) ⟩∘⟨refl ○ distributeʳ⁻¹-natural id id h) ⟩ + (eval′ +₁ id) ∘ (distributeʳ⁻¹ ∘ ((id +₁ h) ⁂ id)) ∘ (f ⁂ id) ≈⟨ refl⟩∘⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ eq identity²) ⟩ + (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ∘ h ⁂ id) ≈˘⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ refl identity²)) ⟩ + ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) ∘ (h ⁂ id) ∎ + + algebra (Exponential-Elgot-Algebra {E} {X}) .#-Folding {B} {D} {f} {h} = λ-cong (begin + [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# +₁ h) ⁂ id) ]# ≈⟨ #-resp-≈ (algebra E) (refl⟩∘⟨ (sym (distributeʳ⁻¹-natural id (λg ((E Elgot-Algebra.#) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)))) h))) ⟩ + [ algebra E , (eval′ +₁ id) ∘ ((λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# ⁂ id) +₁ (h ⁂ id)) ∘ distributeʳ⁻¹ ]# ≈⟨ #-resp-≈ (algebra E) (pullˡ (+₁∘+₁ ○ +₁-cong₂ β′ identityˡ)) ⟩ + [ algebra E , ([ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# +₁ (h ⁂ id)) ∘ distributeʳ⁻¹ ]# ≈⟨ #-Uniformity (algebra E) by-uni₁ ⟩ + [ algebra E , [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)]# +₁ distributeʳ⁻¹ ∘ (h ⁂ id) ]# ∘ distributeʳ⁻¹ ≈⟨ (#-Folding (algebra E)) ⟩∘⟨refl ⟩ + [ algebra E , [ ((id +₁ i₁) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) , (i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) ] ]# ∘ distributeʳ⁻¹ ≈˘⟨ #-Uniformity (algebra E) by-uni₂ ⟩ + [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id) ]# ∎) + where + by-uni₁ : (id +₁ distributeʳ⁻¹) ∘ ([ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# +₁ h ⁂ id) ∘ distributeʳ⁻¹ ≈ (([ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# +₁ distributeʳ⁻¹ ∘ (h ⁂ id))) ∘ distributeʳ⁻¹ + by-uni₁ = pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ refl) + by-uni₂ : (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id) ≈ [ (id +₁ i₁) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ∘ distributeʳ⁻¹ + by-uni₂ = Iso⇒Epi (IsIso.iso isIsoʳ) ((id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) ([ (id +₁ i₁) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ∘ distributeʳ⁻¹) (begin + ((id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) ∘ distributeʳ ≈⟨ ∘[] ⟩ + [ (((id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) ∘ (i₁ ⁂ id)) + , (((id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) ∘ (i₂ ⁂ id)) ] ≈⟨ []-cong₂ (pullʳ (pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ inject₁ identity²)))) (pullʳ (pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ inject₂ identity²)))) ⟩ + [ (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((id +₁ i₁) ∘ f) ⁂ id) , (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((i₂ ∘ h) ⁂ id) ] ≈⟨ []-cong₂ (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ refl identity²)) (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ refl identity²)) ⟩ + [ (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((id +₁ i₁)) ⁂ id) ∘ (f ⁂ id) , (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (i₂ ⁂ id) ∘ (h ⁂ id) ] ≈⟨ []-cong₂ (refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym (distributeʳ⁻¹-natural id id i₁))) (refl⟩∘⟨ refl⟩∘⟨ pullˡ distributeʳ⁻¹-i₂) ⟩ + [ (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ ((id ⁂ id +₁ i₁ ⁂ id) ∘ distributeʳ⁻¹) ∘ (f ⁂ id) , (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ i₂ ∘ (h ⁂ id) ] ≈⟨ []-cong₂ (pullˡ +₁∘+₁) (pullˡ +₁∘+₁) ⟩ + [ (id ∘ eval′ +₁ distributeʳ⁻¹ ∘ id) ∘ ((id ⁂ id +₁ i₁ ⁂ id) ∘ distributeʳ⁻¹) ∘ (f ⁂ id) , (id ∘ eval′ +₁ distributeʳ⁻¹ ∘ id) ∘ i₂ ∘ (h ⁂ id) ] ≈⟨ []-cong₂ (pullˡ (pullˡ +₁∘+₁)) (pullˡ +₁∘i₂) ⟩ + [ ((((id ∘ eval′) ∘ (id ⁂ id)) +₁ ((distributeʳ⁻¹ ∘ id) ∘ (i₁ ⁂ id))) ∘ distributeʳ⁻¹) ∘ (f ⁂ id) , (i₂ ∘ (distributeʳ⁻¹ ∘ id)) ∘ (h ⁂ id) ] ≈⟨ []-cong₂ (((+₁-cong₂ (identityˡ ⟩∘⟨refl) (identityʳ ⟩∘⟨refl ○ distributeʳ⁻¹-i₁)) ⟩∘⟨refl) ⟩∘⟨refl) (pullʳ (pullʳ identityˡ)) ⟩ + [ (((eval′ ∘ (id ⁂ id)) +₁ i₁) ∘ distributeʳ⁻¹) ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ≈⟨ []-cong₂ (assoc ○ (+₁-cong₂ (elimʳ (⟨⟩-unique id-comm id-comm)) refl) ⟩∘⟨refl) refl ⟩ + [ (eval′ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ≈˘⟨ []-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ)) refl ⟩ + [ (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ʳ ∎) + + algebra (Exponential-Elgot-Algebra {E} {X}) .#-resp-≈ {Y} {f} {g} eq = λ-cong (#-resp-≈ (algebra E) (refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ eq refl)) ``` \ No newline at end of file