mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
improve proofs
This commit is contained in:
parent
e6e1a9cb68
commit
7986abb134
SSH key fingerprint:
SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 71 additions and 71 deletions
|
|
@ -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))
|
||||
```
|
||||
Loading…
Reference in a new issue