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

Work on commutativity

Browse source
This commit is contained in:
Leon Vatthauer 2023-11-22 09:44:20 +01:00
parent bfb437ea36
commit bb2e7c5061
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
2 changed files with 22 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -112,6 +112,8 @@ Here we give a different Characterization and show that it is equal.
⟩ ⟩
([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂ ∎ ([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂ ∎
-- TODO Proposition 41
-- every elgot-algebra comes with a divergence constant -- every elgot-algebra comes with a divergence constant
!ₑ : ⊥ ⇒ A !ₑ : ⊥ ⇒ A
!ₑ = i₂ # !ₑ = i₂ #

40
src/Monad/Instance/K/Commutative.lagda.md
View file

@ -164,6 +164,12 @@ KCommutative = record { commutes = commutes' }
where where
ψ : ∀ {X Y} → K.₀ X × K.₀ Y ⇒ K.₀ (X × Y) ψ : ∀ {X Y} → K.₀ X × K.₀ Y ⇒ K.₀ (X × Y)
ψ = extend (τ _) ∘ σ _ ψ = extend (τ _) ∘ σ _
ψ-left-iter : ∀ {X Y U} (h : X ⇒ K.₀ Y + X) → ψ {Y} {U} ∘ (h # ⁂ idC) ≈ ((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #
ψ-left-iter {X} {Y} {U} h = begin
ψ ∘ (h # ⁂ idC) ≈⟨ pullʳ (σ-comm h) ⟩
extend (τ _) ∘ ((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC))# ≈⟨ extend-preserve (τ (Y , U)) (((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC))) ⟩
((extend (τ _) +₁ idC) ∘ (σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC))# ≈⟨ #-resp-≈ (algebras (Y × U)) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
(((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #) ∎
comm₅ : (ψ ∘ (idC ⁂ (h #))) ∘ (η _ ⁂ idC) ≈ τ _ ∘ (idC ⁂ h #) comm₅ : (ψ ∘ (idC ⁂ (h #))) ∘ (η _ ⁂ idC) ≈ τ _ ∘ (idC ⁂ h #)
comm₅ = begin comm₅ = begin
(ψ ∘ (idC ⁂ (h #))) ∘ (η _ ⁂ idC) ≈⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ id-comm-sym id-comm) ⟩ (ψ ∘ (idC ⁂ (h #))) ∘ (η _ ⁂ idC) ≈⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ id-comm-sym id-comm) ⟩
@ -204,25 +210,19 @@ KCommutative = record { commutes = commutes' }
(idC +₁ (idC ⁂ h #)) ∘ ((ψ ∘ (idC ⁂ h #)) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) ∎ (idC +₁ (idC ⁂ h #)) ∘ ((ψ ∘ (idC ⁂ h #)) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) ∎
comm₈ : ∀ {U} (g : U ⇒ K.₀ X + U) → ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ (g # ⁂ idC) ≈ ((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))# comm₈ : ∀ {U} (g : U ⇒ K.₀ X + U) → ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ (g # ⁂ idC) ≈ ((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#
comm₈ {U} g = begin comm₈ {U} g = begin
((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (g # ⁂ idC) ≈⟨ {!!} ⟩ -- Uniformity ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (g # ⁂ idC) ≈⟨ sym (#-Uniformity (algebras (X × Y)) (sym by-uni)) ⟩
((((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) # +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ {! !} ⟩ ((ψ ∘ ((g #) ⁂ idC) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ (ψ-left-iter g) refl) ⟩∘⟨refl) ⟩
( [ (idC +₁ i₁) ∘ (ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , i₂ ∘ i₂ ] ∘ [ i₁ , distributeˡ⁻¹ ∘ (idC ⁂ h) ]) # ∘ i₂ ≈⟨ {!!} ⟩ (((((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) # +₁ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ {! !} ⟩
([ (ψ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , i₂ ∘ i₂ ] ∘ [ i₁ , distributeˡ⁻¹ ∘ (idC ⁂ h) ]) # ∘ i₂ ≈⟨ {!!} ⟩ {! !} ≈⟨ {! !} ⟩
[ [ (ψ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , i₂ ∘ i₂ ] ∘ i₁ , [ (ψ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , i₂ ∘ i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ] # ∘ i₂ ≈⟨ {!!} ⟩ {! !} ≈⟨ {! !} ⟩
[ (ψ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , [ (ψ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , i₂ ∘ i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ] # ∘ i₂ ≈⟨ {!!} ⟩ {! !} ≈⟨ {! !} ⟩
([ (ψ +₁ i₁) ∘ distributeʳ⁻¹ , [ (ψ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , i₂ ∘ i₂ ] ∘ distributeˡ⁻¹ ] ∘ (g ⁂ idC +₁ idC ⁂ h)) # ∘ i₂ ≈⟨ {!!} ⟩
{!!} ≈⟨ {!!} ⟩
{!!} ≈⟨ {!!} ⟩
{!!} ≈⟨ {!!} ⟩
{!!} ≈⟨ {!!} ⟩
{!!} ≈⟨ {!!} ⟩
{!!} ≈⟨ {!!} ⟩
([((ψ +₁ i₁) ∘ distributeʳ⁻¹) , (i₂ ∘ i₂ ∘ distributeʳ⁻¹) ] ∘ distributeˡ⁻¹ ∘ {!!}) # ∘ i₂ ∘ i₂ ≈⟨ {!!} ⟩
{!!} ≈˘⟨ {!!} ⟩
{!!} ≈˘⟨ {!!} ⟩
{!!} ≈˘⟨ {!!} ⟩
{!!} ≈˘⟨ {!!} ⟩
([ (idC +₁ i₁) ∘ (ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) , i₂ ∘ i₂ ] ∘ [ i₁ , distributeʳ⁻¹ ∘ (g ⁂ idC) ]) # ∘ i₂ ≈˘⟨ {! !} ⟩
((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))# ∎ ((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))# ∎
where
by-uni : ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ ((g #) ⁂ idC) ≈ (idC +₁ (g #) ⁂ idC) ∘ (ψ ∘ ((g #) ⁂ idC) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)
by-uni = begin
((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ ((g #) ⁂ idC) ≈⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ id-comm-sym id-comm ○ sym ⁂∘⁂)) ⟩
(ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ ((g #) ⁂ idC) ∘ (idC ⁂ h) ≈⟨ {! !} ⟩
(ψ +₁ idC) ∘ ((((g #) ⁂ idC) +₁ ((g #) ⁂ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h) ≈⟨ pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (sym identityˡ) id-comm-sym ○ sym +₁∘+₁)) ⟩
(((idC +₁ (g #) ⁂ idC) ∘ (ψ ∘ ((g #) ⁂ idC) +₁ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h) ≈⟨ assoc² ⟩
(idC +₁ (g #) ⁂ idC) ∘ (ψ ∘ ((g #) ⁂ idC) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ∎
``` ```