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 new proof principle

Browse source
This commit is contained in:
Leon Vatthauer 2023-11-03 17:33:44 +01:00
parent 446d55f1f5
commit 7f336282ed
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
3 changed files with 154 additions and 106 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

52
src/Algebra/Properties.lagda.md
View file

@ -66,7 +66,57 @@ This file contains some typedefs and records concerning different algebras.
→ f ≈ g ∘ (idC ⁂ η)
→ (∀ {Z : Obj} (h : Z ⇒ Uniform-Iteration-Algebra.A FY + Z) → g ∘ (idC ⁂ h #) ≈ Uniform-Iteration-Algebra._# B ((g +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)))
→ g ≈ [ B , f ]♯
[_,_]♯ˡ : ∀ {X : Obj} (A : Uniform-Iteration-Algebra) (f : Y × X ⇒ Uniform-Iteration-Algebra.A A) → Uniform-Iteration-Algebra.A FY × X ⇒ Uniform-Iteration-Algebra.A A
[_,_]♯ˡ {X} A f = [ A , (f ∘ swap) ]♯ ∘ swap
♯ˡ-law : ∀ {X : Obj} {A : Uniform-Iteration-Algebra} (f : Y × X ⇒ Uniform-Iteration-Algebra.A A) → f ≈ [ A , f ]♯ˡ ∘ (η ⁂ idC)
♯ˡ-law {X} {A} f = begin
f ≈⟨ introʳ swap∘swap ⟩
f ∘ swap ∘ swap ≈⟨ pullˡ (♯-law (f ∘ swap)) ⟩
([ A , f ∘ swap ]♯ ∘ (idC ⁂ η)) ∘ swap ≈⟨ pullʳ (sym swap∘⁂) ⟩
[ A , (f ∘ swap) ]♯ ∘ swap ∘ (η ⁂ idC) ≈⟨ sym-assoc ⟩
([ A , (f ∘ swap) ]♯ ∘ swap) ∘ (η ⁂ idC) ∎
♯ˡ-preserving : ∀ {X : Obj} {B : Uniform-Iteration-Algebra} (f : Y × X ⇒ Uniform-Iteration-Algebra.A B) {Z : Obj} (h : Z ⇒ Uniform-Iteration-Algebra.A FY + Z) → [ B , f ]♯ˡ ∘ (h # ⁂ idC) ≈ Uniform-Iteration-Algebra._# B (([ B , f ]♯ˡ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC))
♯ˡ-preserving {X} {B} f {Z} h = begin
([ B , (f ∘ swap) ]♯ ∘ swap) ∘ ((h #) ⁂ idC) ≈⟨ pullʳ swap∘⁂ ⟩
[ B , (f ∘ swap) ]♯ ∘ (idC ⁂ h #) ∘ swap ≈⟨ pullˡ (♯-preserving (f ∘ swap) h) ⟩
(([ B , (f ∘ swap) ]♯ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #ᵇ ∘ swap ≈⟨ sym (#ᵇ-Uniformity uni-helper) ⟩
((([ B , (f ∘ swap) ]♯ ∘ swap) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #ᵇ ∎
where
open Uniform-Iteration-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity)
uni-helper : (idC +₁ swap) ∘ ([ B , f ∘ swap ]♯ ∘ swap +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈ (([ B , f ∘ swap ]♯ coproducts.+₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ swap
uni-helper = begin
(idC +₁ swap) ∘ ([ B , f ∘ swap ]♯ ∘ swap +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ pullˡ +₁∘+₁ ⟩
(idC ∘ [ B , f ∘ swap ]♯ ∘ swap +₁ swap ∘ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩
([ B , f ∘ swap ]♯ ∘ swap +₁ idC ∘ swap) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ (sym +₁∘+₁) ⟩∘⟨refl ⟩
(([ B , f ∘ swap ]♯ +₁ idC) ∘ (swap +₁ swap)) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ pullʳ (pullˡ (sym distributeˡ⁻¹∘swap)) ⟩
([ B , f ∘ swap ]♯ +₁ idC) ∘ (distributeˡ⁻¹ ∘ swap) ∘ (h ⁂ idC) ≈⟨ (refl⟩∘⟨ (pullʳ swap∘⁂ ○ sym-assoc)) ○ sym-assoc ⟩
(([ B , f ∘ swap ]♯ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ swap ∎
♯ˡ-unique : ∀ {X : Obj} {B : Uniform-Iteration-Algebra} (f : Y × X ⇒ Uniform-Iteration-Algebra.A B) (g : Uniform-Iteration-Algebra.A FY × X ⇒ Uniform-Iteration-Algebra.A B)
→ f ≈ g ∘ (η ⁂ idC)
→ ({Z : Obj} (h : Z ⇒ Uniform-Iteration-Algebra.A FY + Z) → g ∘ (h # ⁂ idC) ≈ Uniform-Iteration-Algebra._# B ((g +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)))
→ g ≈ [ B , f ]♯ˡ
♯ˡ-unique {X} {B} f g g-law g-preserving = begin
g ≈⟨ introʳ swap∘swap ⟩
g ∘ swap ∘ swap ≈⟨ sym-assoc ⟩
(g ∘ swap) ∘ swap ≈⟨ (♯-unique (f ∘ swap) (g ∘ swap) helper₁ helper₂) ⟩∘⟨refl ⟩
[ B , (f ∘ swap) ]♯ ∘ swap ∎
where
open Uniform-Iteration-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity)
helper₁ : f ∘ swap ≈ (g ∘ swap) ∘ (idC ⁂ η)
helper₁ = begin
f ∘ swap ≈⟨ g-law ⟩∘⟨refl ⟩
(g ∘ (η ⁂ idC)) ∘ swap ≈⟨ pullʳ (sym swap∘⁂) ⟩
g ∘ swap ∘ (idC ⁂ η) ≈⟨ sym-assoc ⟩
(g ∘ swap) ∘ (idC ⁂ η) ∎
helper₂ : ∀ {Z : Obj} (h : Z ⇒ Uniform-Iteration-Algebra.A FY + Z) → (g ∘ swap) ∘ (idC ⁂ h #) ≈ ((g ∘ swap +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #ᵇ
helper₂ {Z} h = begin
(g ∘ swap) ∘ (idC ⁂ h #) ≈⟨ pullʳ swap∘⁂ ⟩
g ∘ (h # ⁂ idC) ∘ swap ≈⟨ pullˡ (g-preserving h) ⟩
((g +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #ᵇ ∘ swap ≈⟨ sym (#ᵇ-Uniformity uni-helper) ⟩
((g ∘ swap +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #ᵇ ∎
where
uni-helper : (idC +₁ swap) ∘ (g ∘ swap +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈ ((g +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) ∘ swap
uni-helper = pullˡ +₁∘+₁ ○ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ○ (sym +₁∘+₁) ⟩∘⟨refl ○ pullʳ (pullˡ (sym distributeʳ⁻¹∘swap)) ○ (refl⟩∘⟨ (pullʳ swap∘⁂ ○ sym-assoc)) ○ sym-assoc
record StableFreeUniformIterationAlgebra : Set (suc o ⊔ suc ℓ ⊔ suc e) where
field
Y : Obj

9
src/Category/Instance/AmbientCategory.lagda.md
View file

@ -88,6 +88,15 @@ module Category.Instance.AmbientCategory where
[ (idC ⁂ i₁) ∘ swap , (idC ⁂ i₂) ∘ swap ] ∘ distributeʳ⁻¹ ≈⟨ sym (pullˡ []∘+₁) ⟩
distributeˡ ∘ (swap +₁ swap) ∘ distributeʳ⁻¹ ∎)
distributeʳ⁻¹∘swap : ∀ {A B C : Obj} → distributeʳ⁻¹ ∘ swap ≈ (swap +₁ swap) ∘ distributeˡ⁻¹ {A} {B} {C}
distributeʳ⁻¹∘swap = Iso⇒Mono C (IsIso.iso isIsoʳ) (distributeʳ⁻¹ ∘ swap) ((swap +₁ swap) ∘ distributeˡ⁻¹) (begin
(distributeʳ ∘ distributeʳ⁻¹ ∘ swap) ≈⟨ cancelˡ (IsIso.isoʳ isIsoʳ) ⟩
swap ≈⟨ sym (cancelʳ (IsIso.isoʳ isIsoˡ)) ⟩
((swap ∘ distributeˡ) ∘ distributeˡ⁻¹) ≈⟨ (∘[] ⟩∘⟨refl) ⟩
[ swap ∘ (idC ⁂ i₁) , swap ∘ (idC ⁂ i₂) ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ (sym swap∘⁂) (sym swap∘⁂)) ⟩∘⟨refl) ⟩
[ (i₁ ⁂ idC) ∘ swap , (i₂ ⁂ idC) ∘ swap ] ∘ distributeˡ⁻¹ ≈⟨ sym (pullˡ []∘+₁) ⟩
(distributeʳ ∘ (swap +₁ swap) ∘ distributeˡ⁻¹) ∎)
dstr-law₁ : ∀ {A B C} → distributeˡ⁻¹ {A} {B} {C} ∘ (idC ⁂ i₁) ≈ i₁
dstr-law₁ = (refl⟩∘⟨ (sym inject₁)) ○ (cancelˡ (IsIso.isoˡ isIsoˡ))
dstr-law₂ : ∀ {A B C} → distributeˡ⁻¹ {A} {B} {C} ∘ (idC ⁂ i₂) ≈ i₂

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

@ -13,17 +13,17 @@ import Monad.Instance.K as MIK
```agda
module Monad.Instance.K.Commutative {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
open Ambient ambient
open MIK ambient
open MonadK MK
open import Monad.Instance.K.Strong ambient MK
open import Category.Construction.UniformIterationAlgebras ambient
open import Algebra.UniformIterationAlgebra ambient
open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra)
open Ambient ambient
open MIK ambient
open MonadK MK
open import Monad.Instance.K.Strong ambient MK
open import Category.Construction.UniformIterationAlgebras ambient
open import Algebra.UniformIterationAlgebra ambient
open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra)
open Equiv
open HomReasoning
open MR C
open Equiv
open HomReasoning
open MR C
-- open M C
```
@ -34,101 +34,90 @@ The proof is analogous to the ones for strength, the relevant diagram is:
<iframe class="quiver-embed" src="https://q.uiver.app/#q=WzAsNyxbMCwxLCJLWCBcXHRpbWVzIEtZIl0sWzEsMCwiSyhLWCBcXHRpbWVzIFkpIl0sWzIsMCwiSyhLKFggXFx0aW1lcyBZKSkiXSxbMywxLCJLKFggXFx0aW1lcyBZKSJdLFsxLDIsIksoWCBcXHRpbWVzIEtZKSJdLFsyLDIsIksoSyhYIFxcdGltZXMgWSkpIl0sWzAsNCwiS1ggXFx0aW1lcyBZIl0sWzAsMSwiXFx0YXUiXSxbMSwyLCJLXFxoYXR7XFx0YXV9Il0sWzIsMywiXFxtdSJdLFswLDQsIlxcaGF0e1xcdGF1fSIsMl0sWzQsNSwiS1xcdGF1IiwyXSxbNSwzLCJcXG11IiwyXSxbNiwwLCJpZCBcXHRpbWVzIFxcZXRhIl0sWzYsMywiXFxoYXR7XFx0YXV9IiwwLHsiY3VydmUiOjV9XSxbMCwzLCJcXGhhdHtcXHRhdX1eXFwjIl1d&embed" width="974" height="688" style="border-radius: 8px; border: none;"></iframe>
```agda
KCommutative : CommutativeMonad {C = C} {V = monoidal} symmetric KStrong
KCommutative = record { commutes = commutes' }
where
open monadK using (μ)
open StrongMonad KStrong using (strengthen)
open IsStableFreeUniformIterationAlgebra using (♯-law; ♯-preserving; ♯-unique)
open Uniform-Iteration-Algebra using (#-Uniformity; #-Fixpoint; #-resp-≈)
-- some helper definitions to make our life easier
η = λ Z → FreeObject.η (freealgebras Z)
_♯ = λ {A X Y} f → IsStableFreeUniformIterationAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} (algebras Y) f
_# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f
open monadK using (μ)
open StrongMonad KStrong using (strengthen)
open IsStableFreeUniformIterationAlgebra using (♯-law; ♯-preserving; ♯-unique; ♯ˡ-unique; ♯ˡ-preserving; ♯ˡ-law)
open Uniform-Iteration-Algebra using (#-Uniformity; #-Fixpoint; #-resp-≈)
σ : ∀ ((X , Y) : Obj ×f Obj) → K.₀ X × Y ⇒ K.₀ (X × Y)
σ _ = K.₁ swap ∘ (τ _) ∘ swap
-- some helper definitions to make our life easier
private
η = λ Z → FreeObject.η (freealgebras Z)
_♯ = λ {A X Y} f → IsStableFreeUniformIterationAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} (algebras Y) f
_♯ˡ = λ {A X Y} f → IsStableFreeUniformIterationAlgebra.[_,_]♯ˡ {Y = X} (stable X) {X = A} (algebras Y) f
_# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f
σ-preserve : ∀ {X Y Z : Obj} (h : Z ⇒ K.₀ Y + Z) → σ (Y , X) ∘ (h # ⁂ idC) ≈ ((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC))#
{-
K.₁ swap ∘ τ ∘ swap ∘ (h # ⁂ idC)
≈ K.₁ swap ∘ τ ∘ (idC ⁂ h #) ∘ swap
≈ K.₁ swap ∘ ()# ∘ swap
≈ ((K.₁ swap +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ swap
-}
σ-preserve {Z} h = {! !}
σ-preserve' : ∀ {X Y Z : Obj} (h : Z ⇒ K.₀ Y + Z) → σ (X , K.₀ Y) ∘ (idC ⁂ h #) ≈ ((σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
σ-preserve' {Z} h = {! !}
commutes' : ∀ {X Y : Obj} → μ.η _ ∘ K.₁ (σ _) ∘ τ (K.₀ X , Y) ≈ μ.η _ ∘ K.₁ (τ _) ∘ σ _
commutes' {X} {Y} = begin
μ.η _ ∘ K.₁ (σ _) ∘ τ _ ≈⟨ ♯-unique (stable _) (σ _) (μ.η (X × Y) ∘ K.₁ (σ _) ∘ τ _) comm₁ comm₂ ⟩
(σ _) ♯ ≈⟨ sym (♯-unique (stable _) (σ _) (μ.η _ ∘ K.₁ (τ _) ∘ σ _) comm₃ comm₄) ⟩
{! !} ≈⟨ {! !} ⟩
μ.η _ ∘ K.₁ (τ _) ∘ σ _ ∎
where
comm₁ : σ _ ≈ (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ η _)
comm₁ = sym (begin
(μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ η _) ≈⟨ pullʳ (pullʳ (τ-η _)) ⟩
μ.η _ ∘ K.₁ (σ _) ∘ η _ ≈⟨ refl⟩∘⟨ (K₁η _) ⟩
μ.η _ ∘ η _ ∘ σ _ ≈⟨ cancelˡ monadK.identityʳ ⟩
σ _ ∎)
comm₂ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ h #) ≈ ((μ.η _ ∘ K.₁ (σ _) ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
comm₂ {Z} h = begin
(μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ h #) ≈⟨ pullʳ (pullʳ (♯-preserving (stable _) (η _) h)) ⟩
μ.η _ ∘ K.₁ (σ _) ∘ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ refl⟩∘⟨ (Uniform-Iteration-Algebra-Morphism.preserves ((freealgebras _ FreeObject.*) (η _ ∘ σ _))) ⟩
μ.η _ ∘ ((K.₁ (σ _) +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) idC) ⟩
((μ.η _ +₁ idC) ∘ (K.₁ (σ _) +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩
((μ.η _ ∘ K.₁ (σ _) +₁ idC ∘ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩
(((μ.η _ ∘ K.₁ (σ _)) ∘ τ _ +₁ (idC ∘ idC) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ assoc (elimˡ identity²)) ⟩∘⟨refl) ⟩
((μ.η _ ∘ K.₁ (σ _) ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎
comm₃ : σ _ ≈ (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ η _)
comm₃ = sym (begin
(μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ η _) ≈⟨ pullʳ (pullʳ (pullʳ (pullʳ swap∘⁂))) ⟩
μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ τ _ ∘ (η _ ⁂ idC) ∘ swap ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (sym K.identity) ⟩∘⟨refl ⟩
μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ τ _ ∘ (η _ ⁂ K.₁ idC) ∘ swap ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (strengthen.commute (η _ , idC)) ⟩
μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ (K.₁ (η _ ⁂ idC) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (pullˡ (sym K.homomorphism)) ⟩
μ.η _ ∘ K.₁ (τ _) ∘ (K.₁ (swap ∘ (η _ ⁂ idC)) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ (pullˡ (pullˡ (sym K.homomorphism))) ⟩
μ.η _ ∘ (K.₁ (τ _ ∘ swap ∘ (η _ ⁂ idC)) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ (((K.F-resp-≈ (refl⟩∘⟨ swap∘⁂)) ⟩∘⟨refl) ⟩∘⟨refl) ⟩
μ.η _ ∘ (K.₁ (τ _ ∘ (idC ⁂ η _) ∘ swap) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ (K.F-resp-≈ (pullˡ (τ-η _))) ⟩∘⟨refl ⟩∘⟨refl ⟩
μ.η _ ∘ (K.₁ (η _ ∘ swap) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ ((K.homomorphism ⟩∘⟨refl) ⟩∘⟨refl) ⟩
μ.η _ ∘ ((K.₁ (η _) ∘ K.₁ swap) ∘ τ _) ∘ swap ≈⟨ pullˡ (pullˡ (cancelˡ monadK.identityˡ)) ⟩
(K.₁ swap ∘ τ _) ∘ swap ≈⟨ assoc ⟩
σ _ ∎)
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.₁ (τ _) ∘ σ _) ∘ (((i₁ #) ⁂ h #)) ≈˘⟨ refl⟩∘⟨ ⟨⟩-cong₂ (#-Uniformity (algebras _) helper₁) {! !} ⟩
(μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ ⟨ ((π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # , ((π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ⟩ ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
((μ.η _ ∘ K.₁ (τ _) ∘ σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎
where
-- this leads nowhere
helper₁ : (idC +₁ π₁) ∘ (π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈ i₁ ∘ π₁
helper₁ = begin
(idC +₁ π₁) ∘ (π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩
(π₁ +₁ π₁) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ {! !} ⟩
i₁ ∘ π₁ ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ π₁∘⁂ ⟩
i₁ ∘ idC ∘ π₁ ≈⟨ refl⟩∘⟨ identityˡ ⟩
i₁ ∘ π₁ ∎
test : ((τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ swap ≈ ((τ (X , Y) ∘ swap +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #
test = sym (#-Uniformity (algebras _) (sym (begin
((τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ swap ≈⟨ pullʳ (pullʳ (sym swap∘⁂)) ⟩
(τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ swap ∘ (h ⁂ idC) ≈⟨ refl⟩∘⟨ (pullˡ distributeˡ⁻¹∘swap) ⟩
(τ (X , Y) +₁ idC) ∘ ((swap +₁ swap) ∘ distributeʳ⁻¹) ∘ (h ⁂ idC) ≈⟨ pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (sym identityˡ) id-comm-sym)) ⟩
((idC ∘ τ (X , Y) ∘ swap +₁ swap ∘ idC) ∘ distributeʳ⁻¹) ∘ (h ⁂ idC) ≈⟨ assoc ○ (sym +₁∘+₁) ⟩∘⟨refl ⟩
((idC +₁ swap) ∘ (τ (X , Y) ∘ swap +₁ idC)) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ assoc ⟩
(idC +₁ swap) ∘ (τ (X , Y) ∘ swap +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ∎)))
helper : τ _ ∘ (h # ⁂ idC) ∘ swap ≈ ((τ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) # ∘ swap
helper = {! !}
τ∘swap-preserving : τ (K.₀ Y , X) ∘ (h # ⁂ idC) ≈ ((τ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #
τ∘swap-preserving = begin
τ (K.₀ Y , X) ∘ (h # ⁂ idC) ≈⟨ {! !} ⟩
τ (K.₀ Y , X) ∘ (h # ⁂ K.₁ idC) ≈⟨ {! !} ⟩
K.₁ (h # ⁂ idC) ∘ τ _ ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
((τ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) # ∎
σ : ∀ ((X , Y) : Obj ×f Obj) → K.₀ X × Y ⇒ K.₀ (X × Y)
σ _ = K.₁ swap ∘ (τ _) ∘ swap
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₁ {! !}) ⟩
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)) ♯ˡ ≈⟨ {! !} ⟩
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)) # ∎
where
uni-helper : (idC +₁ idC ⁂ η Y) ∘ (f ∘ (idC ⁂ η Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈ ((f +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) ∘ (idC ⁂ η Y)
uni-helper = {! !}
KCommutative : CommutativeMonad {C = C} {V = monoidal} symmetric KStrong
KCommutative = record { commutes = commutes' }
where
commutes' : ∀ {X Y : Obj} → μ.η _ ∘ K.₁ (σ _) ∘ τ (K.₀ X , Y) ≈ μ.η _ ∘ K.₁ (τ _) ∘ σ _
commutes' {X} {Y} = begin
μ.η _ ∘ K.₁ (σ _) ∘ τ _ ≈⟨ ♯-unique (stable _) (σ _) (μ.η (X × Y) ∘ K.₁ (σ _) ∘ τ _) comm₁ comm₂ ⟩
(σ _) ♯ ≈⟨ sym (♯-unique (stable _) (σ _) (μ.η _ ∘ K.₁ (τ _) ∘ σ _) comm₃ comm₄) ⟩
{! !} ≈⟨ {! !} ⟩
μ.η _ ∘ K.₁ (τ _) ∘ σ _ ∎
where
comm₁ : σ _ ≈ (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ η _)
comm₁ = sym (begin
(μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ η _) ≈⟨ pullʳ (pullʳ (τ-η _)) ⟩
μ.η _ ∘ K.₁ (σ _) ∘ η _ ≈⟨ refl⟩∘⟨ (K₁η _) ⟩
μ.η _ ∘ η _ ∘ σ _ ≈⟨ cancelˡ monadK.identityʳ ⟩
σ _ ∎)
comm₂ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ h #) ≈ ((μ.η _ ∘ K.₁ (σ _) ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
comm₂ {Z} h = begin
(μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ h #) ≈⟨ pullʳ (pullʳ (♯-preserving (stable _) (η _) h)) ⟩
μ.η _ ∘ K.₁ (σ _) ∘ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ refl⟩∘⟨ (Uniform-Iteration-Algebra-Morphism.preserves ((freealgebras _ FreeObject.*) (η _ ∘ σ _))) ⟩
μ.η _ ∘ ((K.₁ (σ _) +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) idC) ⟩
((μ.η _ +₁ idC) ∘ (K.₁ (σ _) +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩
((μ.η _ ∘ K.₁ (σ _) +₁ idC ∘ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩
(((μ.η _ ∘ K.₁ (σ _)) ∘ τ _ +₁ (idC ∘ idC) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ assoc (elimˡ identity²)) ⟩∘⟨refl) ⟩
((μ.η _ ∘ K.₁ (σ _) ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎
comm₃ : σ _ ≈ (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ η _)
comm₃ = sym (begin
(μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ η _) ≈⟨ pullʳ (pullʳ (pullʳ (pullʳ swap∘⁂))) ⟩
μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ τ _ ∘ (η _ ⁂ idC) ∘ swap ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (sym K.identity) ⟩∘⟨refl ⟩
μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ τ _ ∘ (η _ ⁂ K.₁ idC) ∘ swap ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (strengthen.commute (η _ , idC)) ⟩
μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ (K.₁ (η _ ⁂ idC) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (pullˡ (sym K.homomorphism)) ⟩
μ.η _ ∘ K.₁ (τ _) ∘ (K.₁ (swap ∘ (η _ ⁂ idC)) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ (pullˡ (pullˡ (sym K.homomorphism))) ⟩
μ.η _ ∘ (K.₁ (τ _ ∘ swap ∘ (η _ ⁂ idC)) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ (((K.F-resp-≈ (refl⟩∘⟨ swap∘⁂)) ⟩∘⟨refl) ⟩∘⟨refl) ⟩
μ.η _ ∘ (K.₁ (τ _ ∘ (idC ⁂ η _) ∘ swap) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ (K.F-resp-≈ (pullˡ (τ-η _))) ⟩∘⟨refl ⟩∘⟨refl ⟩
μ.η _ ∘ (K.₁ (η _ ∘ swap) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ ((K.homomorphism ⟩∘⟨refl) ⟩∘⟨refl) ⟩
μ.η _ ∘ ((K.₁ (η _) ∘ K.₁ swap) ∘ τ _) ∘ swap ≈⟨ pullˡ (pullˡ (cancelˡ monadK.identityˡ)) ⟩
(K.₁ swap ∘ τ _) ∘ swap ≈⟨ assoc ⟩
σ _ ∎)
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))# ∎
```