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

align

Browse source
This commit is contained in:
Leon Vatthauer 2023-11-30 10:41:02 +01:00
parent 2f4441a2ae
commit ac3b80c4f6
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 40 additions and 54 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -174,20 +174,6 @@ 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 ⟩