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

minor

Browse source
This commit is contained in:
Leon Vatthauer 2023-11-11 15:44:16 +01:00
parent 21c98bab4f
commit 4d052891cd
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 19 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

33
src/Monad/Instance/K/PreElgot.lagda.md
View file

@ -477,20 +477,6 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A), (f : X
w : X × N ⇒ X
w = universal idC (case f inl π₁ inr π₂) --([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩)
ww' : w' ∘ (idC ⁂ s) ≈ w
ww' = unique (sym IB) {! !}
where
IB : (w' ∘ (idC ⁂ s)) ∘ ⟨ idC , z ∘ ! ⟩ ≈ idC
IB = begin
(w' ∘ (idC ⁂ s)) ∘ ⟨ idC , z ∘ ! ⟩ ≈⟨ (p-rec-IS idC _) ⟩∘⟨refl ⟩
(([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _) ∘ ⟨ idC , z ∘ ! ⟩ ≈⟨ pullʳ (sym commute₁) ⟩
([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ ⟨ idC , ⟨ idC , z ∘ ! ⟩ ⟩ ≈⟨ pullʳ (pullʳ ⁂∘⟨⟩) ⟩
[ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC ∘ idC , (f ∘ π₁) ∘ ⟨ idC , z ∘ ! ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ identity² (cancelʳ project₁) ⟩
[ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ≈⟨ {! !} ⟩
(case f inl π₁ inr π₂) ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
idC ∎
-- TODO this depends on (8) and (9)
stronger : ((extend [ i₂ # , f ]#⟩ ∘ τ (X , N) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ ⟨ π₁ , ⟨ w , π₂ ⟩ ⟩ ≈ f # ∘ w
stronger = begin
@ -498,6 +484,25 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A), (f : X
((π₂ +₁ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ idC ⁂ s , f ∘ w ⟩ )# ≈⟨ #-Uniformity (algebras _) by-uni₂ ⟩
f # ∘ w ∎
where
f#⟩-fact : [ i₂ # , f ]#⟩ ∘ (idC ⁂ s) ≈ case (f ∘ w) inl π₂ inr (i₂ #)
f#⟩-fact = begin
[ i₂ # , f ]#⟩ ∘ (idC ⁂ s) ≈⟨ {! !} ⟩
universal (case f inl (π₂) inr (i₂ #)) {! case f inl ? inr ? !} ≈⟨ sym (unique (sym IB₁) (sym IS₁)) ⟩
(case (f ∘ w) inl π₂ inr (i₂ #)) ∎
where
IB₁ : (case f ∘ w inl π₂ inr (i₂ #)) ∘ ⟨ idC , z ∘ ! ⟩ ≈ case f inl (π₂) inr (i₂ #)
IB₁ = begin
(case f ∘ w inl π₂ inr (i₂ #)) ∘ ⟨ idC , z ∘ ! ⟩ ≈⟨ case∘ʳ (f ∘ w) π₂ (i₂ #) ⟨ idC , z ∘ ! ⟩ ⟩
(case (f ∘ w) ∘ ⟨ idC , z ∘ ! ⟩ inl (π₂ ∘ (⟨ idC , z ∘ ! ⟩ ⁂ idC)) inr (i₂ # ∘ (⟨ idC , z ∘ ! ⟩ ⁂ idC))) ≈⟨ (case⟩ (cancelʳ (sym commute₁)) ⟨inl⟩ (π₂∘⁂ ○ identityˡ) ⟨inr⟩ {! !}) ⟩
(case f inl (π₂) inr (i₂ #)) ∎
IS₁ : (case f ∘ w inl π₂ inr (i₂ #)) ∘ (idC ⁂ s) ≈ {! (case f inl π₂ inr (i₂ #)) ∘ w !} ∘ (case f ∘ w inl π₂ inr (i₂ #))
IS₁ = begin
(case f ∘ w inl π₂ inr (i₂ #)) ∘ (idC ⁂ s) ≈⟨ case∘ʳ (f ∘ w) π₂ (i₂ #) (idC ⁂ s) ⟩
(case ((f ∘ w) ∘ (idC ⁂ s)) inl (π₂ ∘ ((idC ⁂ s) ⁂ idC)) inr ((i₂ #) ∘ ((idC ⁂ s) ⁂ idC))) ≈⟨ (case⟩ (pullʳ (sym commute₂)) ⟨inl⟩ (π₂∘⁂ ○ identityˡ) ⟨inr⟩ {! !}) ⟩
(case (f ∘ (case f inl π₁ inr π₂) ∘ w) inl (π₂) inr (i₂ #)) ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ∎
by-uni₁ : (idC +₁ ⟨ π₁ , ⟨ w , π₂ ⟩ ⟩) ∘ (π₂ +₁ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ idC ⁂ s , f ∘ w ⟩ ≈ ((extend [ i₂ # , f ]#⟩ ∘ τ (X , N) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ ⟨ π₁ , ⟨ w , π₂ ⟩ ⟩
by-uni₁ = {! !}
by-uni₂ : (idC +₁ w) ∘ (π₂ +₁ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ idC ⁂ s , f ∘ w ⟩ ≈ f ∘ w