mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
Progress on commutativity
This commit is contained in:
parent
c7f9ccf05a
commit
9437ad8e7c
SSH key fingerprint:
SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 82 additions and 28 deletions
|
|
@ -77,6 +77,16 @@ private
|
|||
((σ _ +₁ swap) ∘ distributeʳ⁻¹) ∘ (h ⁂ idC) ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ○ sym-assoc ⟩
|
||||
(idC +₁ swap) ∘ (σ (X , Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ∎
|
||||
|
||||
σ-natural : ∀ {X Y Z U} (f : X ⇒ Y) (g : Z ⇒ U) → σ _ ∘ (K.₁ f ⁂ g) ≈ K.₁ (f ⁂ g) ∘ σ _
|
||||
σ-natural {X} {Y} {Z} {U} f g = begin
|
||||
σ _ ∘ (K.₁ f ⁂ g) ≈⟨ pullʳ (pullʳ swap∘⁂) ⟩
|
||||
K.₁ swap ∘ τ _ ∘ (g ⁂ K.₁ f) ∘ swap ≈⟨ refl⟩∘⟨ ((pullˡ (strengthen.commute (g , f))) ○ assoc) ⟩
|
||||
K.₁ swap ∘ K.₁ (g ⁂ f) ∘ τ _ ∘ swap ≈⟨ pullˡ (sym monadK.F.homomorphism) ⟩
|
||||
K.₁ (swap ∘ (g ⁂ f)) ∘ τ _ ∘ swap ≈⟨ (monadK.F.F-resp-≈ swap∘⁂) ⟩∘⟨refl ⟩
|
||||
K.₁ ((f ⁂ g) ∘ swap) ∘ τ _ ∘ swap ≈⟨ monadK.F.homomorphism ⟩∘⟨refl ⟩
|
||||
(K.₁ ((f ⁂ g)) ∘ K.₁ swap) ∘ τ _ ∘ swap ≈⟨ assoc ⟩
|
||||
K.₁ (f ⁂ g) ∘ σ _ ∎
|
||||
|
||||
extend-preserve : ∀ {X Y Z} (f : X ⇒ K.₀ Y) (h : Z ⇒ K.₀ X + Z) → extend f ∘ h # ≈ ((extend f +₁ idC) ∘ h) #
|
||||
extend-preserve {X} {Y} {Z} f h = begin
|
||||
(μ.η _ ∘ K.₁ f) ∘ h # ≈⟨ pullʳ (Elgot-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η _ ∘ f))) ⟩
|
||||
|
|
@ -117,6 +127,34 @@ proof-principle {X} {Y} f g η-eq f-iter₁ f-iter₂ g-iter₁ g-iter₂ = begi
|
|||
(k +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ∘ idC ⁂ idC ∘ η Y) ≈˘⟨ pullʳ (pullʳ ⁂∘⁂) ⟩
|
||||
((k +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) ∘ (idC ⁂ η Y) ∎
|
||||
|
||||
private
|
||||
comm-helper : ∀ {X Y Z U} (f : X ⇒ K.₀ Y + X) (g : Z ⇒ K.₀ U + Z) → extend (τ _) ∘ σ _ ∘ (((η _ +₁ idC) ∘ f) # ⁂ ((η _ +₁ idC) ∘ g) #) ≈ extend (σ _) ∘ τ _ ∘ (((η _ +₁ idC) ∘ f) # ⁂ ((η _ +₁ idC) ∘ g) #)
|
||||
comm-helper {X} {Y} {Z} {U} f g = begin
|
||||
extend (τ _) ∘ σ _ ∘ (f' # ⁂ g' #) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ w-law₁ w-law₂ ⟩
|
||||
extend (τ _) ∘ σ _ ∘ ⟨ extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w # , extend [ η _ ∘ π₂ , g' # ∘ π₂ ] ∘ w # ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym ⁂∘⟨⟩ ⟩
|
||||
extend (τ _) ∘ σ _ ∘ (extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ⁂ extend [ η _ ∘ π₂ , g' # ∘ π₂ ]) ∘ ⟨ w # , w # ⟩ ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
extend (σ _) ∘ τ _ ∘ (((η _ +₁ idC) ∘ f) # ⁂ ((η _ +₁ idC) ∘ g) #) ∎
|
||||
where
|
||||
f' = (η _ +₁ idC) ∘ f
|
||||
g' = (η _ +₁ idC) ∘ g
|
||||
w = [ i₁ ∘ K.₁ i₁ ∘ τ _ , (K.₁ i₂ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')
|
||||
w-law₁ : f' # ∘ π₁ ≈ extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w #
|
||||
w-law₁ = {! !}
|
||||
w-law₂ : g' # ∘ π₂ ≈ extend [ η _ ∘ π₂ , g' # ∘ π₂ ] ∘ w #
|
||||
w-law₂ = {! !}
|
||||
|
||||
KCommutative : CommutativeMonad {C = C} {V = monoidal} symmetric KStrong
|
||||
KCommutative = record { commutes = commutes' }
|
||||
where
|
||||
|
|
@ -211,47 +249,63 @@ KCommutative = record { commutes = commutes' }
|
|||
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
|
||||
((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (g # ⁂ idC) ≈⟨ στ ⟩
|
||||
extend ψ ∘ extend (σ _) ∘ τ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ {! !} ⟩ -- lemma 42
|
||||
extend ψ ∘ extend (σ _) ∘ τ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ refl⟩∘⟨ (sym (comm-helper g h)) ⟩ -- lemma 42
|
||||
extend ψ ∘ extend (τ _) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ sym τσ ⟩
|
||||
((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))# ∎
|
||||
where
|
||||
τσ : ((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))# ≈ extend ψ ∘ extend (τ _) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #)
|
||||
τσ = begin
|
||||
(((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#) ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
extend ψ ∘ extend (τ _) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #) ∎
|
||||
(((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#) ≈˘⟨ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ kleisliK.identityʳ identity²)) ⟩
|
||||
((extend (((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) +₁ idC) ∘ (η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) # ≈˘⟨ extend-preserve (((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ((η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) ⟩
|
||||
extend (((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ∘ ((η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) # ≈⟨ refl⟩∘⟨ (#-resp-≈ (algebras _) ((+₁-cong₂ (sym σ-η) refl) ⟩∘⟨refl)) ⟩
|
||||
extend (((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ∘ ((σ _ ∘ (η _ ⁂ idC) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) # ≈˘⟨ refl⟩∘⟨ (σ-comm _ ○ #-resp-≈ (algebras _) comm) ⟩
|
||||
extend (((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g)# ⁂ idC) ≈˘⟨ (kleisliK.extend-≈ (#-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ kleisliK.identityʳ identity²)))) ⟩∘⟨refl ⟩
|
||||
extend ((((extend ψ +₁ idC) ∘ (η _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#)) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g)# ⁂ idC) ≈˘⟨ (kleisliK.extend-≈ (extend-preserve ψ _)) ⟩∘⟨refl ⟩
|
||||
extend (extend ψ ∘ (((η _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#)) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g)# ⁂ idC) ≈˘⟨ pullˡ kleisliK.sym-assoc ⟩
|
||||
extend ψ ∘ extend (((η _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g)# ⁂ idC) ≈˘⟨ refl⟩∘⟨ ((kleisliK.extend-≈ (#-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (sym (distribute₁ idC _ idC)))) ○ #-resp-≈ (algebras _) (pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (τ-η _) (elimʳ (⟨⟩-unique id-comm id-comm)))) ○ assoc))) ⟩∘⟨refl) ⟩
|
||||
extend ψ ∘ extend (((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC)) ∘ (idC ⁂ h)) #) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g)# ⁂ idC) ≈⟨ refl⟩∘⟨ (kleisliK.extend-≈ (#-resp-≈ (algebras _) (refl⟩∘⟨ (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identity² refl))))) ⟩∘⟨refl ⟩
|
||||
extend ψ ∘ extend (((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC) ∘ h)) #) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g)# ⁂ idC) ≈˘⟨ refl⟩∘⟨ ((kleisliK.extend-≈ (τ-comm _)) ⟩∘⟨refl) ⟩
|
||||
extend ψ ∘ extend (τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #)) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g)# ⁂ idC) ≈˘⟨ refl⟩∘⟨ (pullˡ (extend∘F₁ monadK (τ _) _)) ⟩
|
||||
extend ψ ∘ extend (τ _) ∘ K.₁ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g)# ⁂ idC) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym (σ-natural idC (((η (K.₀ Y) +₁ idC) ∘ h) #))) ⟩
|
||||
extend ψ ∘ extend (τ _) ∘ (σ _ ∘ (K.₁ idC ⁂ ((η _ +₁ idC) ∘ h) #)) ∘ (((η _ +₁ idC) ∘ g)# ⁂ idC) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ (elimˡ monadK.F.identity) identityʳ)) ⟩
|
||||
extend ψ ∘ extend (τ _) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #) ∎
|
||||
where
|
||||
comm : (σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (((η _ +₁ idC) ∘ g ⁂ idC)) ≈ (σ _ ∘ (η _ ⁂ idC) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)
|
||||
comm = sym (begin
|
||||
(σ _ ∘ (η _ ⁂ idC) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²) ⟩
|
||||
(σ _ +₁ idC) ∘ ((η _ ⁂ idC) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) ≈⟨ refl⟩∘⟨ (pullˡ ((+₁-cong₂ refl (sym (⟨⟩-unique id-comm id-comm))) ⟩∘⟨refl ○ distribute₁' idC (η (K.₀ X)) idC)) ⟩
|
||||
(σ _ +₁ idC) ∘ (distributeʳ⁻¹ ∘ ((η _ +₁ idC) ⁂ idC)) ∘ (g ⁂ idC) ≈⟨ refl⟩∘⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ refl identity²) ⟩
|
||||
(σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (((η _ +₁ idC) ∘ g ⁂ idC)) ∎)
|
||||
στ : ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (g # ⁂ idC) ≈ extend ψ ∘ extend (σ _) ∘ τ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #)
|
||||
στ = begin
|
||||
((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (g # ⁂ idC) ≈⟨ sym (#-Uniformity (algebras (X × Y)) (sym by-uni)) ⟩
|
||||
((ψ ∘ ((g #) ⁂ idC) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ (ψ-left-iter g) refl) ⟩∘⟨refl) ⟩
|
||||
(((((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) # +₁ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈˘⟨ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ kleisliK.identityʳ identity²)) ⟩
|
||||
(((extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) +₁ idC) ∘ (η _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ≈˘⟨ extend-preserve (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ((η (U × K.₀ Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ⟩
|
||||
extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ∘ ((η _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ refl⟩∘⟨ (#-resp-≈ (algebras _) ((+₁-cong₂ (sym (τ-η _)) refl) ⟩∘⟨refl)) ⟩
|
||||
extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ∘ ((τ _ ∘ (idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈˘⟨ refl⟩∘⟨ (τ-comm ((η (K.₀ Y) +₁ idC) ∘ h) ○ #-resp-≈ (algebras _) comm) ⟩
|
||||
extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h)#) ≈˘⟨ (kleisliK.extend-≈ (#-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ kleisliK.identityʳ identity²)))) ⟩∘⟨refl ⟩
|
||||
extend ((((extend ψ +₁ idC) ∘ (η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#)) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ (kleisliK.extend-≈ (extend-preserve ψ ((η (K.₀ X × K.₀ Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)))) ⟩∘⟨refl ⟩
|
||||
extend (extend ψ ∘ (((η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#)) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ pullˡ kleisliK.sym-assoc ⟩
|
||||
extend ψ ∘ extend (((η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ refl⟩∘⟨ ((kleisliK.extend-≈ (#-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (sym (distribute₁' idC (η (K.₀ X)) idC)))) ○ #-resp-≈ (algebras _) (pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ σ-η (elimʳ (⟨⟩-unique id-comm id-comm)))) ○ assoc))) ⟩∘⟨refl) ⟩
|
||||
((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (g # ⁂ idC) ≈⟨ sym (#-Uniformity (algebras (X × Y)) (sym by-uni)) ⟩
|
||||
((ψ ∘ ((g #) ⁂ idC) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ (ψ-left-iter g) refl) ⟩∘⟨refl) ⟩
|
||||
(((((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) # +₁ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈˘⟨ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ kleisliK.identityʳ identity²)) ⟩
|
||||
((extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) +₁ idC) ∘ (η _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈˘⟨ extend-preserve (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ((η (U × K.₀ Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ⟩
|
||||
extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ∘ ((η _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ refl⟩∘⟨ (#-resp-≈ (algebras _) ((+₁-cong₂ (sym (τ-η _)) refl) ⟩∘⟨refl)) ⟩
|
||||
extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ∘ ((τ _ ∘ (idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈˘⟨ refl⟩∘⟨ (τ-comm ((η (K.₀ Y) +₁ idC) ∘ h) ○ #-resp-≈ (algebras _) comm) ⟩
|
||||
extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h)#) ≈˘⟨ (kleisliK.extend-≈ (#-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ kleisliK.identityʳ identity²)))) ⟩∘⟨refl ⟩
|
||||
extend ((((extend ψ +₁ idC) ∘ (η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#)) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ (kleisliK.extend-≈ (extend-preserve ψ ((η (K.₀ X × K.₀ Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)))) ⟩∘⟨refl ⟩
|
||||
extend (extend ψ ∘ (((η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#)) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ pullˡ kleisliK.sym-assoc ⟩
|
||||
extend ψ ∘ extend (((η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ refl⟩∘⟨ ((kleisliK.extend-≈ (#-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (sym (distribute₁' idC (η (K.₀ X)) idC)))) ○ #-resp-≈ (algebras _) (pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ σ-η (elimʳ (⟨⟩-unique id-comm id-comm)))) ○ assoc))) ⟩∘⟨refl) ⟩
|
||||
extend ψ ∘ extend (((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ ((η (K.₀ X) +₁ idC) ⁂ idC) ∘ (g ⁂ idC)) #) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ refl⟩∘⟨ (kleisliK.extend-≈ (#-resp-≈ (algebras _) (refl⟩∘⟨ (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²))))) ⟩∘⟨refl ⟩
|
||||
extend ψ ∘ extend (((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ ((η (K.₀ X) +₁ idC) ∘ g ⁂ idC)) #) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ refl⟩∘⟨ ((kleisliK.extend-≈ (σ-comm ((η (K.₀ X) +₁ idC) ∘ g))) ⟩∘⟨refl) ⟩
|
||||
extend ψ ∘ extend (σ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ idC)) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ refl⟩∘⟨ (pullˡ (extend∘F₁ monadK (σ _) (((η _ +₁ idC) ∘ g) # ⁂ idC))) ⟩
|
||||
extend ψ ∘ extend (σ _) ∘ K.₁ (((η _ +₁ idC) ∘ g) # ⁂ idC) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym (strengthen.commute (((η (K.₀ X) +₁ idC) ∘ g) # , idC))) ⟩
|
||||
extend ψ ∘ extend (σ _) ∘ (τ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ K.₁ idC)) ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identityʳ (elimˡ monadK.F.identity))) ⟩
|
||||
extend ψ ∘ extend (σ _) ∘ τ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #) ∎
|
||||
extend ψ ∘ extend (((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ ((η (K.₀ X) +₁ idC) ∘ g ⁂ idC)) #) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ refl⟩∘⟨ ((kleisliK.extend-≈ (σ-comm ((η (K.₀ X) +₁ idC) ∘ g))) ⟩∘⟨refl) ⟩
|
||||
extend ψ ∘ extend (σ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ idC)) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ refl⟩∘⟨ (pullˡ (extend∘F₁ monadK (σ _) (((η _ +₁ idC) ∘ g) # ⁂ idC))) ⟩
|
||||
extend ψ ∘ extend (σ _) ∘ K.₁ (((η _ +₁ idC) ∘ g) # ⁂ idC) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym (strengthen.commute (((η (K.₀ X) +₁ idC) ∘ g) # , idC))) ⟩
|
||||
extend ψ ∘ extend (σ _) ∘ (τ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ K.₁ idC)) ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identityʳ (elimˡ monadK.F.identity))) ⟩
|
||||
extend ψ ∘ extend (σ _) ∘ τ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #) ∎
|
||||
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) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ ((g #) ⁂ idC) ≈⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ id-comm-sym id-comm ○ sym ⁂∘⁂)) ⟩
|
||||
(ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ ((g #) ⁂ idC) ∘ (idC ⁂ h) ≈˘⟨ refl⟩∘⟨ ((distribute₁ (g #) idC idC ○ refl⟩∘⟨ ⁂-cong₂ refl ([]-unique id-comm-sym id-comm-sym)) ⟩∘⟨refl ○ assoc) ⟩
|
||||
(ψ +₁ 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) ∎
|
||||
(idC +₁ (g #) ⁂ idC) ∘ (ψ ∘ ((g #) ⁂ idC) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ∎
|
||||
comm : (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC) ∘ h) ≈ (τ _ ∘ (idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)
|
||||
comm = sym (begin
|
||||
(τ _ ∘ (idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²) ⟩
|
||||
(τ _ +₁ idC) ∘ ((idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ (pullˡ ((+₁-cong₂ refl (sym (⟨⟩-unique id-comm id-comm))) ⟩∘⟨refl ○ distribute₁ idC (η (K.₀ Y)) idC)) ⟩
|
||||
(τ _ ∘ (idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²) ⟩
|
||||
(τ _ +₁ idC) ∘ ((idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ (pullˡ ((+₁-cong₂ refl (sym (⟨⟩-unique id-comm id-comm))) ⟩∘⟨refl ○ distribute₁ idC (η (K.₀ Y)) idC)) ⟩
|
||||
(τ _ +₁ idC) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC))) ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩
|
||||
(τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC) ∘ h) ∎)
|
||||
(τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC) ∘ h) ∎)
|
||||
```
|
||||
|
|
|
|||
Loading…
Reference in a new issue