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

✨ Show equational lifting law, added proof principle

Browse source
This commit is contained in:
Leon Vatthauer 2023-11-04 09:52:36 +01:00
parent 7f336282ed
commit 28cee7138e
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
2 changed files with 85 additions and 35 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -8,6 +8,7 @@ open import Categories.Monad.Strong
open import Data.Product using (_,_) renaming (_×_ to _×f_)
open import Categories.FreeObjects.Free
import Monad.Instance.K as MIK
open import Categories.Morphism.Properties
```
-->
@ -24,7 +25,7 @@ open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; unifo
open Equiv
open HomReasoning
open MR C
-- open M C
open M C
```
# K is a commutative monad
@ -53,26 +54,35 @@ private
proof-principle : ∀ {X Y} (f g : K.₀ X × K.₀ Y ⇒ K.₀ (X × Y)) → f ∘ (η _ ⁂ η _) ≈ g ∘ (η _ ⁂ η _) → (∀ {A} (h : A ⇒ K.₀ Y + A) → f ∘ (idC ⁂ h #) ≈ ((f +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#) → (∀ {A} (h : A ⇒ K.₀ X + A) → f ∘ (h # ⁂ idC) ≈ ((f +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #) → (∀ {A} (h : A ⇒ K.₀ Y + A) → g ∘ (idC ⁂ h #) ≈ ((g +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#) → (∀ {A} (h : A ⇒ K.₀ X + A) → g ∘ (h # ⁂ idC) ≈ ((g +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #) → f ≈ g
proof-principle {X} {Y} f g η-eq f-iter₁ f-iter₂ g-iter₁ g-iter₂ = begin
f ≈⟨ ♯-unique (stable _) (f ∘ (idC ⁂ η Y)) f refl (λ h → f-iter₁ h) ⟩
(f ∘ (idC ⁂ η _)) ♯ ≈⟨ sym (♯-unique (stable _) (f ∘ (idC ⁂ η Y)) g helper₁ {! !}) ⟩
(f ∘ (idC ⁂ η _)) ♯ ≈⟨ sym (♯-unique (stable _) (f ∘ (idC ⁂ η Y)) g helper₁ g-iter₁) ⟩
g ∎
where
helper₁ : f ∘ (idC ⁂ η Y) ≈ g ∘ (idC ⁂ η Y)
helper₁ = begin
f ∘ (idC ⁂ η Y) ≈⟨ ♯ˡ-unique (stable _) (f ∘ (η X ⁂ η Y)) (f ∘ (idC ⁂ η Y)) (sym (pullʳ (⁂∘⁂ ○ (⁂-cong₂ identityˡ identityʳ)))) {! !} ⟩
(f ∘ (η X ⁂ η Y)) ♯ˡ ≈⟨ {! !} ⟩
f ∘ (idC ⁂ η Y) ≈⟨ ♯ˡ-unique (stable _) (f ∘ (η X ⁂ η Y)) (f ∘ (idC ⁂ η Y)) (sym (pullʳ (⁂∘⁂ ○ (⁂-cong₂ identityˡ identityʳ)))) (comm₁ f f-iter₂) ⟩
(f ∘ (η X ⁂ η Y)) ♯ˡ ≈⟨ sym (♯ˡ-unique (stable _) (f ∘ (η X ⁂ η Y)) (g ∘ (idC ⁂ η Y)) (sym (pullʳ (⁂∘⁂ ○ (⁂-cong₂ identityˡ identityʳ)) ○ sym η-eq)) (comm₁ g g-iter₂)) ⟩
g ∘ (idC ⁂ η Y) ∎
where
comm₁ : ∀ {Z : Obj} (h : Z ⇒ K.₀ X + Z) → (f ∘ (idC ⁂ η Y)) ∘ (h # ⁂ idC) ≈ ((f ∘ (idC ⁂ η Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #
comm₁ {Z} h = begin
(f ∘ (idC ⁂ η Y)) ∘ (h # ⁂ idC) ≈⟨ pullʳ ⁂∘⁂ ⟩
f ∘ (idC ∘ h # ⁂ η Y ∘ idC) ≈⟨ refl⟩∘⟨ (⁂-cong₂ id-comm-sym id-comm) ⟩
f ∘ (h # ∘ idC ⁂ idC ∘ η Y) ≈⟨ refl⟩∘⟨ sym ⁂∘⁂ ⟩
f ∘ (h # ⁂ idC) ∘ (idC ⁂ η Y) ≈⟨ pullˡ (f-iter₂ h) ⟩
(((f +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #) ∘ (idC ⁂ η Y) ≈⟨ sym (#-Uniformity (algebras _) uni-helper) ⟩
((f ∘ (idC ⁂ η Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) # ∎
comm₁ : ∀ (k : K.₀ X × K.₀ Y ⇒ K.₀ (X × Y)) (k-iter₂ : ∀ {A} (h : A ⇒ K.₀ X + A) → k ∘ (h # ⁂ idC) ≈ ((k +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #) {Z : Obj} (h : Z ⇒ K.₀ X + Z) → (k ∘ (idC ⁂ η Y)) ∘ (h # ⁂ idC) ≈ ((k ∘ (idC ⁂ η Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #
comm₁ k k-iter₂ {Z} h = begin
(k ∘ (idC ⁂ η Y)) ∘ (h # ⁂ idC) ≈⟨ pullʳ ⁂∘⁂ ⟩
k ∘ (idC ∘ h # ⁂ η Y ∘ idC) ≈⟨ refl⟩∘⟨ (⁂-cong₂ id-comm-sym id-comm) ⟩
k ∘ (h # ∘ idC ⁂ idC ∘ η Y) ≈⟨ refl⟩∘⟨ sym ⁂∘⁂ ⟩
k ∘ (h # ⁂ idC) ∘ (idC ⁂ η Y) ≈⟨ pullˡ (k-iter₂ h) ⟩
(((k +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #) ∘ (idC ⁂ η Y) ≈⟨ sym (#-Uniformity (algebras _) uni-helper) ⟩
((k ∘ (idC ⁂ η Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) # ∎
where
uni-helper : (idC +₁ idC ⁂ η Y) ∘ (f ∘ (idC ⁂ η Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈ ((f +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) ∘ (idC ⁂ η Y)
uni-helper = {! !}
uni-helper : (idC +₁ idC ⁂ η Y) ∘ (k ∘ (idC ⁂ η Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈ ((k +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) ∘ (idC ⁂ η Y)
uni-helper = begin
(idC +₁ idC ⁂ η Y) ∘ (k ∘ (idC ⁂ η Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ pullˡ +₁∘+₁ ⟩
(idC ∘ k ∘ (idC ⁂ η Y) +₁ (idC ⁂ η Y) ∘ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩
(k ∘ (idC ⁂ η Y) +₁ idC ∘ (idC ⁂ η Y)) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ (sym +₁∘+₁) ⟩∘⟨refl ⟩
((k +₁ idC) ∘ ((idC ⁂ η Y) +₁ (idC ⁂ η Y))) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ pullʳ (pullˡ (distribute₁' (η Y) idC idC)) ⟩
(k +₁ idC) ∘ (distributeʳ⁻¹ ∘ ((idC +₁ idC) ⁂ η Y)) ∘ (h ⁂ idC) ≈⟨ refl⟩∘⟨ pullʳ ⁂∘⁂ ⟩
(k +₁ idC) ∘ distributeʳ⁻¹ ∘ ((idC +₁ idC) ∘ h ⁂ η Y ∘ idC) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ (elimˡ ([]-unique id-comm-sym id-comm-sym)) identityʳ ⟩
(k +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ η Y) ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ identityʳ identityˡ ⟩
(k +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ∘ idC ⁂ idC ∘ η Y) ≈˘⟨ pullʳ (pullʳ ⁂∘⁂) ⟩
((k +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) ∘ (idC ⁂ η Y) ∎
KCommutative : CommutativeMonad {C = C} {V = monoidal} symmetric KStrong
KCommutative = record { commutes = commutes' }
@ -115,9 +125,20 @@ KCommutative = record { commutes = commutes' }
comm₄ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ h #) ≈ ((μ.η _ ∘ K.₁ (τ _) ∘ σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
comm₄ {Z} h = begin
(μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ h #) ≈⟨ {! !} ⟩
(μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ ((i₁ # ∘ idC) ⁂ h #) ≈˘⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
(μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ ⟨ ((π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # , ((π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ⟩ ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
((μ.η _ ∘ K.₁ (τ _) ∘ σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎
where
π₁-iter : ((π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈ π₁ ∘ (idC ⁂ h #)
π₁-iter = {! !}
distrib : (π₁ +₁ idC) ∘ distributeˡ⁻¹ ≈ i₁ ∘ π₁
distrib = Iso⇒Epi C (IsIso.iso isIsoˡ) ((π₁ +₁ idC) ∘ distributeˡ⁻¹) (i₁ ∘ π₁) (begin
((π₁ +₁ idC) ∘ distributeˡ⁻¹) ∘ distributeˡ ≈⟨ cancelʳ {! !} ⟩
(π₁ +₁ idC) ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
i₁ ∘ [ π₁ , π₁ ] ≈˘⟨ {! !} ⟩
[ i₁ ∘ π₁ , i₁ ∘ π₁ ] ≈˘⟨ {! !} ⟩
[ i₁ ∘ idC ∘ π₁ , i₁ ∘ idC ∘ π₁ ] ≈˘⟨ []-cong₂ (pullʳ π₁∘⁂) (pullʳ π₁∘⁂) ⟩
[ (i₁ ∘ π₁) ∘ (idC ⁂ i₁) , (i₁ ∘ π₁) ∘ (idC ⁂ i₂) ] ≈˘⟨ ∘[] ⟩
(i₁ ∘ π₁) ∘ distributeˡ ∎)
```

65
src/Monad/Instance/K/EquationalLifting.lagda.md
View file

@ -8,6 +8,8 @@ open import Categories.FreeObjects.Free
open import Categories.Category.Construction.Kleisli
open import Categories.Category.Restriction
import Monad.Instance.K as MIK
open import Categories.Morphism.Properties
```
-->
@ -24,9 +26,12 @@ open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; unifo
open HomReasoning
open Equiv
open M C
open MR C
open kleisliK using (extend)
open monadK using (μ)
open FreeObject using (*-uniq)
open Uniform-Iteration-Algebra using (#-Uniformity; #-Fixpoint; #-resp-≈)
-- some helper definitions to make our life easier
private
@ -39,29 +44,53 @@ private
```agda
equationalLifting : ∀ {X} → τ (K.₀ X , X) ∘ Δ {K.₀ X} ≈ K.₁ ⟨ η X , idC ⟩
equationalLifting = {! !}
equationalLifting {X} = *-uniq (freealgebras _) (η _ ∘ ⟨ η X , idC ⟩) (record { h = τ (K.₀ X , X) ∘ Δ ; preserves = preserves' }) commute
where
preserves' : ∀ {Z} {f : Z ⇒ K.₀ X + Z} → (τ (K.₀ X , X) ∘ Δ) ∘ f # ≈ ((τ (K.₀ X , X) ∘ Δ +₁ idC) ∘ f) #
preserves' {Z} {f} = begin
(τ (K.₀ X , X) ∘ Δ) ∘ f # ≈⟨ pullʳ Δ∘ ⟩
τ (K.₀ X , X) ∘ ⟨ f # , f # ⟩ ≈⟨ helper₁ ⟩
((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ f))# ∘ ⟨ f # , idC ⟩ ≈⟨ helper₂ ⟩ -- lemma20
((τ (K.₀ X , X) ∘ Δ +₁ idC) ∘ f) # ∎
where
helper₁ : τ (K.₀ X , X) ∘ ⟨ f # , f # ⟩ ≈ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ f))# ∘ ⟨ f # , idC ⟩
helper₁ = begin
τ (K.₀ X , X) ∘ ⟨ f # , f # ⟩ ≈⟨ refl⟩∘⟨ ((⟨⟩-cong₂ (sym identityˡ) (sym identityʳ)) ○ sym ⁂∘⟨⟩) ⟩
τ (K.₀ X , X) ∘ (idC ⁂ f #) ∘ ⟨ f # , idC ⟩ ≈⟨ pullˡ (τ-comm f) ⟩
((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ f))# ∘ ⟨ f # , idC ⟩ ∎
helper₂ : ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ f))# ∘ ⟨ f # , idC ⟩ ≈ ((τ (K.₀ X , X) ∘ Δ +₁ idC) ∘ f) #
helper₂ = sym (#-Uniformity (algebras _) (begin
(idC +₁ ⟨ f # , idC ⟩) ∘ (τ (K.₀ X , X) ∘ Δ +₁ idC) ∘ f ≈⟨ pullˡ +₁∘+₁ ⟩
(idC ∘ τ (K.₀ X , X) ∘ Δ +₁ ⟨ f # , idC ⟩ ∘ idC) ∘ f ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩
(τ (K.₀ X , X) ∘ Δ +₁ idC ∘ ⟨ f # , idC ⟩) ∘ f ≈⟨ (sym +₁∘+₁) ⟩∘⟨refl ⟩
((τ _ +₁ idC) ∘ (Δ +₁ ⟨ f # , idC ⟩)) ∘ f ≈⟨ assoc ⟩
(τ _ +₁ idC) ∘ (Δ +₁ ⟨ f # , idC ⟩) ∘ f ≈⟨ refl⟩∘⟨ distrib ⟩
(τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ ⟨ f # , f ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ identityˡ identityʳ ⟩
(τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ ⟨ idC ∘ f # , f ∘ idC ⟩ ≈˘⟨ pullʳ (pullʳ ⁂∘⟨⟩) ⟩
((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ f)) ∘ ⟨ f # , idC ⟩ ∎))
where
distrib : (Δ +₁ ⟨ f # , idC ⟩) ∘ f ≈ distributeˡ⁻¹ ∘ ⟨ f # , f ⟩
distrib = Iso⇒Mono C (IsIso.iso isIsoˡ) ((Δ +₁ ⟨ f # , idC ⟩) ∘ f) (distributeˡ⁻¹ ∘ ⟨ f # , f ⟩) (begin
distributeˡ ∘ (Δ +₁ ⟨ f # , idC ⟩) ∘ f ≈⟨ pullˡ []∘+₁ ⟩
[ (idC ⁂ i₁) ∘ Δ , (idC ⁂ i₂) ∘ ⟨ f # , idC ⟩ ] ∘ f ≈⟨ ([]-cong₂ ⁂∘Δ ⁂∘⟨⟩) ⟩∘⟨refl ⟩
[ ⟨ idC , i₁ ⟩ , ⟨ idC ∘ f # , i₂ ∘ idC ⟩ ] ∘ f ≈⟨ ([]-unique
(⟨⟩∘ ○ (⟨⟩-cong₂ inject₁ identityˡ))
(⟨⟩∘ ○ (⟨⟩-cong₂ (inject₂ ○ sym identityˡ) id-comm-sym))) ⟩∘⟨refl ⟩
⟨ [ idC , f # ] , idC ⟩ ∘ f ≈⟨ ⟨⟩∘ ⟩
⟨ [ idC , f # ] ∘ f , idC ∘ f ⟩ ≈˘⟨ ⟨⟩-cong₂ (#-Fixpoint (algebras _)) (sym identityˡ) ⟩
⟨ f # , f ⟩ ≈˘⟨ cancelˡ (IsIso.isoʳ isIsoˡ) ⟩
distributeˡ ∘ distributeˡ⁻¹ ∘ ⟨ f # , f ⟩ ∎)
commute : (τ (K.₀ X , X) ∘ Δ) ∘ η _ ≈ η _ ∘ ⟨ η X , idC ⟩
commute = begin
(τ (K.₀ X , X) ∘ Δ) ∘ η _ ≈⟨ pullʳ Δ∘ ⟩
τ (K.₀ X , X) ∘ ⟨ η X , η X ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (sym identityˡ) (sym identityʳ) ○ sym ⁂∘⟨⟩) ⟩
τ (K.₀ X , X) ∘ (idC ⁂ η X) ∘ ⟨ η X , idC ⟩ ≈⟨ pullˡ (τ-η _) ⟩
η _ ∘ ⟨ η X , idC ⟩ ∎
```
From this we can follow that the kleisli category of **K** is a *restriction category*.
```agda
-- TODO this a trivial restriction structure, since η is identity in the kleisli category...
kleisli-restriction : Restriction (Kleisli monadK)
kleisli-restriction = record
{ _↓ = λ f → η _
; pidʳ = kleisliK.identityʳ
; ↓-comm = refl
; ↓-denestʳ = begin
η _ ≈˘⟨ cancelˡ monadK.identityʳ ⟩
μ.η _ ∘ η _ ∘ η _ ≈˘⟨ pullʳ (K₁η (η _)) ⟩
(μ.η _ ∘ K.₁ (η _)) ∘ η _ ∎
; ↓-skew-comm = λ {A} {B} {C} {g} {f} → begin
(μ.η _ ∘ K.₁ (η _)) ∘ f ≈⟨ elimˡ monadK.identityˡ ⟩
f ≈˘⟨ kleisliK.identityʳ ⟩
extend f ∘ η _ ∎
; ↓-cong = λ _ → refl
}
kleisli-restriction' : Restriction (Kleisli monadK)
kleisli-restriction' = record
{ _↓ = λ f → K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩