leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

Compare commits

base: leonv:b2eb9119aef59fcb0f85bc4b6a40a986655a78ab
Branches Tags
leonv:main
leonv:Abgabe
...
compare: leonv:ac3b80c4f6b0f421bd419faf7f0cf66932aa874c
Branches Tags
leonv:main
leonv:Abgabe

2 commits
b2eb9119ae ... ac3b80c4f6

Author SHA1 Message Date
Leon Vatthauer
ac3b80c4f6
align 2023-11-30 10:41:02 +01:00
Leon Vatthauer
2f4441a2ae
minor 2023-11-30 10:32:43 +01:00
1 changed files with 40 additions and 56 deletions
Show stats Expand all files Collapse all files

96
src/Algebra/Elgot.lagda.md
View file

@ -115,57 +115,55 @@ Here we give a different Characterization and show that it is equal.
#-Stutter : ∀ {X Y} (f : X ⇒ (Y + Y) + X) (h : Y ⇒ A) → (([ h , h ] +₁ idC) ∘ f)# ≈ [ i₁ ∘ h , [ h +₁ i₁ , i₂ ∘ i₂ ] ∘ f ] # ∘ i₂ #-Stutter : ∀ {X Y} (f : X ⇒ (Y + Y) + X) (h : Y ⇒ A) → (([ h , h ] +₁ idC) ∘ f)# ≈ [ i₁ ∘ h , [ h +₁ i₁ , i₂ ∘ i₂ ] ∘ f ] # ∘ i₂
#-Stutter {X} {Y} f h = begin #-Stutter {X} {Y} f h = begin
(([ h , h ] +₁ idC) ∘ f)# ≈⟨ #-resp-≈ ((+₁-cong₂ (sym help) refl) ⟩∘⟨refl) ⟩ (([ h , h ] +₁ idC) ∘ f)# ≈⟨ #-resp-≈ ((+₁-cong₂ (sym help) refl) ⟩∘⟨refl) ⟩
(((h +₁ i₁) # +₁ idC) ∘ f) # ≈⟨ #-Compositionality ⟩ (((h +₁ i₁) # +₁ idC) ∘ f) # ≈⟨ #-Compositionality ⟩
([ (idC +₁ i₁) ∘ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) # ∘ i₂ ≈⟨ ((#-resp-≈ (([]-cong₂ (+₁∘+₁ ○ +₁-cong₂ identityˡ refl) refl) ⟩∘⟨refl)) ⟩∘⟨refl) ⟩ ([ (idC +₁ i₁) ∘ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) # ∘ i₂ ≈⟨ ((#-resp-≈ (([]-cong₂ (+₁∘+₁ ○ +₁-cong₂ identityˡ refl) refl) ⟩∘⟨refl)) ⟩∘⟨refl) ⟩
([ (h +₁ i₁ ∘ i₁) , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) # ∘ i₂ ≈˘⟨ (refl⟩∘⟨ (+₁∘i₂ ○ identityʳ)) ⟩ ([ (h +₁ i₁ ∘ i₁) , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) # ∘ i₂ ≈˘⟨ (refl⟩∘⟨ (+₁∘i₂ ○ identityʳ)) ⟩
([ (h +₁ i₁ ∘ i₁) , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) # ∘ (i₁ +₁ idC) ∘ i₂ ≈⟨ pullˡ (sym (#-Uniformity (sym by-uni))) ⟩ ([ (h +₁ i₁ ∘ i₁) , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) # ∘ (i₁ +₁ idC) ∘ i₂ ≈⟨ pullˡ (sym (#-Uniformity (sym by-uni))) ⟩
[ i₁ ∘ h , [ h +₁ i₁ , i₂ ∘ i₂ ] ∘ f ] # ∘ i₂ ∎ [ i₁ ∘ h , [ h +₁ i₁ , i₂ ∘ i₂ ] ∘ f ] # ∘ i₂ ∎
where where
help : (h +₁ i₁) # ≈ [ h , h ] help : (h +₁ i₁) # ≈ [ h , h ]
help = begin help = begin
((h +₁ i₁) #) ≈⟨ #-Fixpoint ⟩ ((h +₁ i₁) #) ≈⟨ #-Fixpoint ⟩
[ idC , (h +₁ i₁) # ] ∘ (h +₁ i₁) ≈⟨ []∘+₁ ○ []-cong₂ identityˡ refl ⟩ [ idC , (h +₁ i₁) # ] ∘ (h +₁ i₁) ≈⟨ []∘+₁ ○ []-cong₂ identityˡ refl ⟩
[ h , (h +₁ i₁) # ∘ i₁ ] ≈⟨ []-cong₂ refl (#-Fixpoint ⟩∘⟨refl) ⟩ [ h , (h +₁ i₁) # ∘ i₁ ] ≈⟨ []-cong₂ refl (#-Fixpoint ⟩∘⟨refl) ⟩
[ h , ([ idC , (h +₁ i₁) # ] ∘ (h +₁ i₁)) ∘ i₁ ] ≈⟨ []-cong₂ refl (pullʳ +₁∘i₁) ⟩ [ h , ([ idC , (h +₁ i₁) # ] ∘ (h +₁ i₁)) ∘ i₁ ] ≈⟨ []-cong₂ refl (pullʳ +₁∘i₁) ⟩
[ h , [ idC , (h +₁ i₁) # ] ∘ i₁ ∘ h ] ≈⟨ []-cong₂ refl (cancelˡ inject₁) ⟩ [ h , [ idC , (h +₁ i₁) # ] ∘ i₁ ∘ h ] ≈⟨ []-cong₂ refl (cancelˡ inject₁) ⟩
[ h , h ] ∎ [ h , h ] ∎
by-uni : ([ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) ∘ (i₁ +₁ idC) ≈ (idC +₁ (i₁ +₁ idC)) ∘ [ i₁ ∘ h , [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ] by-uni : ([ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) ∘ (i₁ +₁ idC) ≈ (idC +₁ (i₁ +₁ idC)) ∘ [ i₁ ∘ h , [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ]
by-uni = begin by-uni = begin
([ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) ∘ (i₁ +₁ idC) ≈⟨ ((∘[] ○ []-cong₂ inject₁ refl) ⟩∘⟨refl) ⟩ ([ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) ∘ (i₁ +₁ idC) ≈⟨ ((∘[] ○ []-cong₂ inject₁ refl) ⟩∘⟨refl) ⟩
[ h +₁ i₁ ∘ i₁ , [ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ f ] ∘ (i₁ +₁ idC) ≈⟨ ([]∘+₁ ○ []-cong₂ +₁∘i₁ identityʳ) ⟩ [ h +₁ i₁ ∘ i₁ , [ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ f ] ∘ (i₁ +₁ idC) ≈⟨ ([]∘+₁ ○ []-cong₂ +₁∘i₁ identityʳ) ⟩
[ i₁ ∘ h , [ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ f ] ≈˘⟨ []-cong₂ (pullˡ (+₁∘i₁ ○ identityʳ)) (([]-cong₂ (+₁∘+₁ ○ +₁-cong₂ identityˡ +₁∘i₁) (pullˡ +₁∘i₂ ○ pullʳ (+₁∘i₂ ○ identityʳ))) ⟩∘⟨refl) ⟩ [ i₁ ∘ h , [ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ f ] ≈˘⟨ []-cong₂ (pullˡ (+₁∘i₁ ○ identityʳ)) (([]-cong₂ (+₁∘+₁ ○ +₁-cong₂ identityˡ +₁∘i₁) (pullˡ +₁∘i₂ ○ pullʳ (+₁∘i₂ ○ identityʳ))) ⟩∘⟨refl) ⟩
[ (idC +₁ (i₁ +₁ idC)) ∘ i₁ ∘ h , [ (idC +₁ (i₁ +₁ idC)) ∘ (h +₁ i₁) , (idC +₁ (i₁ +₁ idC)) ∘ i₂ ∘ i₂ ] ∘ f ] ≈˘⟨ []-cong₂ refl (pullˡ ∘[]) ⟩ [ (idC +₁ (i₁ +₁ idC)) ∘ i₁ ∘ h , [ (idC +₁ (i₁ +₁ idC)) ∘ (h +₁ i₁) , (idC +₁ (i₁ +₁ idC)) ∘ i₂ ∘ i₂ ] ∘ f ] ≈˘⟨ []-cong₂ refl (pullˡ ∘[]) ⟩
[ (idC +₁ (i₁ +₁ idC)) ∘ i₁ ∘ h , (idC +₁ (i₁ +₁ idC)) ∘ [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ] ≈˘⟨ ∘[] ⟩ [ (idC +₁ (i₁ +₁ idC)) ∘ i₁ ∘ h , (idC +₁ (i₁ +₁ idC)) ∘ [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ] ≈˘⟨ ∘[] ⟩
(idC +₁ (i₁ +₁ idC)) ∘ [ i₁ ∘ h , [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ] ∎ (idC +₁ (i₁ +₁ idC)) ∘ [ i₁ ∘ h , [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ] ∎
-- TODO Proposition 41 -- TODO Proposition 41
#-Diamond : ∀ {X} (f : X ⇒ A + (X + X)) → ((idC +₁ [ idC , idC ]) ∘ f)# ≈ ([ i₁ , ((idC +₁ [ idC , idC ]) ∘ f) # +₁ idC ] ∘ f) # #-Diamond : ∀ {X} (f : X ⇒ A + (X + X)) → ((idC +₁ [ idC , idC ]) ∘ f)# ≈ ([ i₁ , ((idC +₁ [ idC , idC ]) ∘ f) # +₁ idC ] ∘ f) #
#-Diamond {X} f = begin #-Diamond {X} f = begin
g # ≈⟨ introʳ inject₂ ⟩ g # ≈⟨ introʳ inject₂ ⟩
g # ∘ [ idC , idC ] ∘ i₂ ≈⟨ pullˡ (sym (#-Uniformity by-uni₁)) ⟩ g # ∘ [ idC , idC ] ∘ i₂ ≈⟨ pullˡ (sym (#-Uniformity by-uni₁)) ⟩
[ (idC +₁ i₁) ∘ g , f ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl (elimˡ ([]-unique id-comm-sym id-comm-sym)))) ⟩∘⟨refl) ⟩ [ (idC +₁ i₁) ∘ g , f ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl (elimˡ ([]-unique id-comm-sym id-comm-sym)))) ⟩∘⟨refl) ⟩
[ (idC +₁ i₁) ∘ g , (idC +₁ idC) ∘ f ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ inject₁ identityˡ)) (pullˡ (+₁∘+₁ ○ +₁-cong₂ inject₂ identityˡ)))) ⟩∘⟨refl) ⟩ [ (idC +₁ i₁) ∘ g , (idC +₁ idC) ∘ f ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ inject₁ identityˡ)) (pullˡ (+₁∘+₁ ○ +₁-cong₂ inject₂ identityˡ)))) ⟩∘⟨refl) ⟩
[ ([ idC , idC ] +₁ idC) ∘ ((i₁ +₁ i₁) ∘ g) , ([ idC , idC ] +₁ idC) ∘ ((i₂ +₁ idC) ∘ f) ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ∘[]) ⟩∘⟨refl) ⟩ [ ([ idC , idC ] +₁ idC) ∘ ((i₁ +₁ i₁) ∘ g) , ([ idC , idC ] +₁ idC) ∘ ((i₂ +₁ idC) ∘ f) ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ∘[]) ⟩∘⟨refl) ⟩
(([ idC , idC ] +₁ idC) ∘ [ ((i₁ +₁ i₁) ∘ g) , ((i₂ +₁ idC) ∘ f) ]) # ∘ i₂ ≈⟨ ((#-Stutter [ (i₁ +₁ i₁) ∘ g , (i₂ +₁ idC) ∘ f ] idC) ⟩∘⟨refl) ⟩ (([ idC , idC ] +₁ idC) ∘ [ ((i₁ +₁ i₁) ∘ g) , ((i₂ +₁ idC) ∘ f) ]) # ∘ i₂ ≈⟨ ((#-Stutter [ (i₁ +₁ i₁) ∘ g , (i₂ +₁ idC) ∘ f ] idC) ⟩∘⟨refl) ⟩
([ i₁ ∘ idC , [ idC +₁ i₁ , i₂ ∘ i₂ ] ∘ [ (i₁ +₁ i₁) ∘ g , (i₂ +₁ idC) ∘ f ] ] # ∘ i₂) ∘ i₂ ≈⟨ (assoc ○ ((#-resp-≈ ([]-cong₂ identityʳ refl)) ⟩∘⟨refl)) ⟩ ([ i₁ ∘ idC , [ idC +₁ i₁ , i₂ ∘ i₂ ] ∘ [ (i₁ +₁ i₁) ∘ g , (i₂ +₁ idC) ∘ f ] ] # ∘ i₂) ∘ i₂ ≈⟨ (assoc ○ ((#-resp-≈ ([]-cong₂ identityʳ refl)) ⟩∘⟨refl)) ⟩
[ i₁ , ([ idC +₁ i₁ , i₂ ∘ i₂ ] ∘ [ (i₁ +₁ i₁) ∘ g , (i₂ +₁ idC) ∘ f ]) ] # ∘ i₂ ∘ i₂ ≈⟨ ((#-resp-≈ ([]-cong₂ refl (∘[] ○ []-cong₂ (pullˡ []∘+₁) (pullˡ []∘+₁)))) ⟩∘⟨refl) ⟩ [ i₁ , ([ idC +₁ i₁ , i₂ ∘ i₂ ] ∘ [ (i₁ +₁ i₁) ∘ g , (i₂ +₁ idC) ∘ f ]) ] # ∘ i₂ ∘ i₂ ≈⟨ ((#-resp-≈ ([]-cong₂ refl (∘[] ○ []-cong₂ (pullˡ []∘+₁) (pullˡ []∘+₁)))) ⟩∘⟨refl) ⟩
[ i₁ , [ [ (idC +₁ i₁) ∘ i₁ , (i₂ ∘ i₂) ∘ i₁ ] ∘ g , [ (idC +₁ i₁) ∘ i₂ , (i₂ ∘ i₂) ∘ idC ] ∘ f ] ] # ∘ i₂ ∘ i₂ ≈⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (([]-cong₂ (+₁∘i₁ ○ identityʳ) assoc) ⟩∘⟨refl) (([]-cong₂ +₁∘i₂ identityʳ) ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩ [ i₁ , [ [ (idC +₁ i₁) ∘ i₁ , (i₂ ∘ i₂) ∘ i₁ ] ∘ g , [ (idC +₁ i₁) ∘ i₂ , (i₂ ∘ i₂) ∘ idC ] ∘ f ] ] # ∘ i₂ ∘ i₂ ≈⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (([]-cong₂ (+₁∘i₁ ○ identityʳ) assoc) ⟩∘⟨refl) (([]-cong₂ +₁∘i₂ identityʳ) ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩
[ i₁ , [ [ i₁ , i₂ ∘ i₂ ∘ i₁ ] ∘ g , [ i₂ ∘ i₁ , i₂ ∘ i₂ ] ∘ f ] ] # ∘ i₂ ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (pullˡ ([]∘+₁ ○ []-cong₂ identityʳ refl)) (∘[] ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩ [ i₁ , [ [ i₁ , i₂ ∘ i₂ ∘ i₁ ] ∘ g , [ i₂ ∘ i₁ , i₂ ∘ i₂ ] ∘ f ] ] # ∘ i₂ ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (pullˡ ([]∘+₁ ○ []-cong₂ identityʳ refl)) (∘[] ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩
[ i₁ , [ [ i₁ , i₂ ] ∘ (idC +₁ i₂ ∘ i₁) ∘ g , (i₂ ∘ [ i₁ , i₂ ]) ∘ f ] ] # ∘ i₂ ∘ i₂ ≈⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (elimˡ +-η) ((elimʳ +-η) ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩ [ i₁ , [ [ i₁ , i₂ ] ∘ (idC +₁ i₂ ∘ i₁) ∘ g , (i₂ ∘ [ i₁ , i₂ ]) ∘ f ] ] # ∘ i₂ ∘ i₂ ≈⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (elimˡ +-η) ((elimʳ +-η) ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩
[ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] # ∘ i₂ ∘ i₂ {A = X} {B = X} ≈⟨ sym (#-Uniformity (sym by-uni₂)) ⟩ [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] # ∘ i₂ ∘ i₂ {A = X} {B = X} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩ [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂ {A = A + X} {B = X} ≈˘⟨ ((#-resp-≈ ([]-cong₂ (∘[] ○ []-cong₂ (+₁∘i₁ ○ identityʳ) (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl))) refl)) ⟩∘⟨refl) ⟩
(([ {! !} , {! !} ] ∘ f) #) ≈⟨ #-Uniformity (sym by-uni₃) ⟩ [ (idC +₁ i₁) ∘ [ i₁ , (idC +₁ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂ ≈⟨ (sym #-Folding) ⟩∘⟨refl ⟩
[ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ (∘[] ○ []-cong₂ (+₁∘i₁ ○ identityʳ) (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl))) refl)) ⟩∘⟨refl) ⟩ ([ i₁ , (idC +₁ i₂) ∘ g ] # +₁ h)# ∘ i₂ ≈⟨ ((#-resp-≈ (+₁-cong₂ by-fix refl)) ⟩∘⟨refl) ⟩
[ (idC +₁ i₁) ∘ [ i₁ , (idC +₁ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂ ≈⟨ (sym #-Folding) ⟩∘⟨refl ⟩ ([ idC , g # ] +₁ h ) # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl ((sym ∘[] ○ elimʳ +-η) ⟩∘⟨refl))) ⟩∘⟨refl) ⟩
([ i₁ , (idC +₁ i₂) ∘ g ] # +₁ h)# ∘ i₂ ≈⟨ ((#-resp-≈ (+₁-cong₂ by-fix refl)) ⟩∘⟨refl) ⟩ [ i₁ ∘ [ idC , g # ] , [ i₂ ∘ i₁ , i₂ ∘ i₂ ] ∘ h ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl (pullˡ ([]∘+₁ ○ []-cong₂ inject₂ identityʳ)))) ⟩∘⟨refl) ⟩
([ idC , g # ] +₁ h ) # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl ((sym ∘[] ○ elimʳ +-η) ⟩∘⟨refl))) ⟩∘⟨refl) ⟩ [ i₁ ∘ [ idC , g # ] , [ [ idC , g # ] +₁ i₁ , i₂ ∘ i₂ ] ∘ (i₂ +₁ idC) ∘ h ] # ∘ i₂ ≈⟨ sym (#-Stutter ((i₂ +₁ idC) ∘ h) [ idC , g # ]) ⟩
[ i₁ ∘ [ idC , g # ] , [ i₂ ∘ i₁ , i₂ ∘ i₂ ] ∘ h ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl (pullˡ ([]∘+₁ ○ []-cong₂ inject₂ identityʳ)))) ⟩∘⟨refl) ⟩ (([ [ idC , g # ] , [ idC , g # ] ] +₁ idC) ∘ (i₂ +₁ idC) ∘ h) # ≈⟨ #-resp-≈ (pullˡ (+₁∘+₁ ○ +₁-cong₂ inject₂ identity²)) ⟩
[ i₁ ∘ [ idC , g # ] , [ [ idC , g # ] +₁ i₁ , i₂ ∘ i₂ ] ∘ (i₂ +₁ idC) ∘ h ] # ∘ i₂ ≈⟨ sym (#-Stutter ((i₂ +₁ idC) ∘ h) [ idC , g # ]) ⟩ ((([ idC , g # ] +₁ idC)) ∘ h) # ≈⟨ #-resp-≈ (pullˡ (∘[] ○ []-cong₂ (pullˡ +₁∘i₁) +₁∘+₁)) ⟩
(([ [ idC , g # ] , [ idC , g # ] ] +₁ idC) ∘ (i₂ +₁ idC) ∘ h) # ≈⟨ #-resp-≈ (pullˡ (+₁∘+₁ ○ +₁-cong₂ inject₂ identity²)) ⟩ ([ (i₁ ∘ [ idC , g # ]) ∘ i₁ , [ idC , g # ] ∘ i₂ +₁ idC ∘ idC ] ∘ f) # ≈⟨ #-resp-≈ (([]-cong₂ (cancelʳ inject₁) (+₁-cong₂ inject₂ identity²)) ⟩∘⟨refl) ⟩
((([ idC , g # ] +₁ idC)) ∘ h) # ≈⟨ #-resp-≈ (pullˡ (∘[] ○ []-cong₂ (pullˡ +₁∘i₁) +₁∘+₁)) ⟩ ([ i₁ , g # +₁ idC ] ∘ f) # ∎
([ (i₁ ∘ [ idC , g # ]) ∘ i₁ , [ idC , g # ] ∘ i₂ +₁ idC ∘ idC ] ∘ f) # ≈⟨ #-resp-≈ (([]-cong₂ (cancelʳ inject₁) (+₁-cong₂ inject₂ identity²)) ⟩∘⟨refl) ⟩
([ i₁ , g # +₁ idC ] ∘ f) # ∎
where where
g = (idC +₁ [ idC , idC ]) ∘ f g = (idC +₁ [ idC , idC ]) ∘ f
h = [ i₁ ∘ i₁ , i₂ +₁ idC ] ∘ f h = [ i₁ ∘ i₁ , i₂ +₁ idC ] ∘ f
@ -176,27 +174,13 @@ Here we give a different Characterization and show that it is equal.
[ (idC +₁ idC) ∘ g , (idC +₁ [ idC , idC ]) ∘ f ] ≈⟨ []-cong₂ (elimˡ ([]-unique id-comm-sym id-comm-sym)) refl ⟩ [ (idC +₁ idC) ∘ g , (idC +₁ [ idC , idC ]) ∘ f ] ≈⟨ []-cong₂ (elimˡ ([]-unique id-comm-sym id-comm-sym)) refl ⟩
[ g , g ] ≈⟨ sym (∘[] ○ []-cong₂ identityʳ identityʳ) ⟩ [ g , g ] ≈⟨ sym (∘[] ○ []-cong₂ identityʳ identityʳ) ⟩
g ∘ [ idC , idC ] ∎ g ∘ [ idC , idC ] ∎
by-uni₂ : [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] ∘ i₂ ∘ i₂ ≈ (idC +₁ i₂ ∘ i₂) ∘ {! !}
by-uni₂ = begin
[ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] ∘ i₂ ∘ i₂ ≈⟨ (pullˡ inject₂) ○ inject₂ ⟩
i₂ ∘ f ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ∎
by-uni₃ : [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ i₂ ≈ (idC +₁ i₂) ∘ {! !}
by-uni₃ = begin
[ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ i₂ ≈⟨ inject₂ ⟩
i₂ ∘ [ i₁ ∘ i₁ , i₂ +₁ idC ] ∘ f ≈⟨ pullˡ ∘[] ⟩
[ i₂ ∘ i₁ ∘ i₁ , i₂ ∘ (i₂ +₁ idC) ] ∘ f ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
(idC +₁ i₂) ∘ [ i₁ , {! i₂ !} ] ∘ f ∎
by-fix : [ i₁ , (idC +₁ i₂) ∘ g ] # ≈ [ idC , g # ] by-fix : [ i₁ , (idC +₁ i₂) ∘ g ] # ≈ [ idC , g # ]
by-fix = sym (begin by-fix = sym (begin
[ idC , g # ] ≈⟨ []-cong₂ refl #-Fixpoint ⟩ [ idC , g # ] ≈⟨ []-cong₂ refl #-Fixpoint ⟩
[ idC , [ idC , g # ] ∘ g ] ≈⟨ []-cong₂ refl (([]-cong₂ refl (#-Uniformity (sym inject₂))) ⟩∘⟨refl) ⟩ [ idC , [ idC , g # ] ∘ g ] ≈⟨ []-cong₂ refl (([]-cong₂ refl (#-Uniformity (sym inject₂))) ⟩∘⟨refl) ⟩
[ idC , [ idC , [ i₁ , (idC +₁ i₂) ∘ g ] # ∘ i₂ ] ∘ g ] ≈˘⟨ ∘[] ○ []-cong₂ inject₁ (pullˡ ([]∘+₁ ○ []-cong₂ identity² refl)) ⟩ [ idC , [ idC , [ i₁ , (idC +₁ i₂) ∘ g ] # ∘ i₂ ] ∘ g ] ≈˘⟨ ∘[] ○ []-cong₂ inject₁ (pullˡ ([]∘+₁ ○ []-cong₂ identity² refl)) ⟩
[ idC , [ i₁ , (idC +₁ i₂) ∘ g ] # ] ∘ [ i₁ , (idC +₁ i₂) ∘ g ] ≈˘⟨ #-Fixpoint ⟩ [ idC , [ i₁ , (idC +₁ i₂) ∘ g ] # ] ∘ [ i₁ , (idC +₁ i₂) ∘ g ] ≈˘⟨ #-Fixpoint ⟩
([ i₁ , (idC +₁ i₂) ∘ g ] #) ∎) ([ i₁ , (idC +₁ i₂) ∘ g ] #) ∎)
-- every elgot-algebra comes with a divergence constant -- every elgot-algebra comes with a divergence constant
!ₑ : ⊥ ⇒ A !ₑ : ⊥ ⇒ A