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

Proof that maybe is equational lifting

Browse source
This commit is contained in:
Leon Vatthauer 2024-02-08 16:16:21 +01:00
parent acac2d6ee4
commit 24a1bbee0e
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
4 changed files with 301 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

53
agda/src/Monad/Instance/Maybe.lagda.md Normal file
View file

@ -0,0 +1,53 @@
<!--
```agda
open import Level
open import Categories.Category.Core
open import Categories.Category.Cocartesian
open import Categories.Category.Cartesian
open import Categories.Category.Distributive
open import Categories.Functor hiding (id)
open import Categories.Object.Terminal
open import Categories.Monad
open import Categories.NaturalTransformation hiding (id)
import Categories.Morphism.Reasoning as MR
```
-->
# The maybe monad
```agda
module Monad.Instance.Maybe {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) where
open Category C
open MR C
open HomReasoning
open Equiv
open Distributive distributive
open Cocartesian cocartesian
open Cartesian cartesian using (terminal)
open Terminal terminal
maybeFunctor : Endofunctor C
maybeFunctor = record
{ F₀ = λ X → X + ⊤
; F₁ = λ f → f +₁ id
; identity = +-unique id-comm-sym id-comm-sym
; homomorphism = λ {X} {Y} {Z} {f} {g} → sym (+₁∘+₁ ○ +₁-cong₂ refl identity²)
; F-resp-≈ = λ eq → +₁-cong₂ eq refl
}
open Monad renaming (identityˡ to m-identityˡ; identityʳ to m-identityʳ; assoc to m-assoc; sym-assoc to m-sym-assoc)
maybeMonad : Monad C
maybeMonad .F = maybeFunctor
maybeMonad .η = ntHelper (record { η = λ X → i₁ ; commute = λ f → sym inject₁ })
maybeMonad .μ = ntHelper (record { η = λ X → [ id , i₂ ] ; commute = λ f → []∘+₁ ○ []-cong₂ id-comm-sym (sym inject₂) ○ sym ∘[]})
maybeMonad .m-assoc = begin
[ id , i₂ ] ∘ ([ id , i₂ ] +₁ id) ≈⟨ []∘+₁ ⟩
[ id ∘ [ id , i₂ ] , i₂ ∘ id ] ≈˘⟨ []-cong₂ id-comm (inject₂ ○ introʳ refl) ⟩
[ [ id , i₂ ] ∘ id , [ id , i₂ ] ∘ i₂ ] ≈˘⟨ ∘[] ⟩
[ id , i₂ ] ∘ [ id , i₂ ] ∎
maybeMonad .m-sym-assoc = sym (m-assoc maybeMonad)
maybeMonad .m-identityˡ = []∘+₁ ○ +-unique refl id-comm-sym
maybeMonad .m-identityʳ = inject₁
```

85
agda/src/Monad/Instance/Maybe/Commutative.lagda.md Normal file
View file

@ -0,0 +1,85 @@
<!--
```agda
open import Level
open import Categories.Category.Core
open import Categories.Category.Cocartesian
open import Categories.Category.Cartesian
open import Categories.Category.BinaryProducts
open import Categories.Category.Cartesian.Monoidal
open import Categories.Category.Cartesian.SymmetricMonoidal
open import Categories.Category.Distributive
open import Categories.Functor hiding (id)
open import Categories.Object.Terminal
open import Categories.Monad
open import Categories.Monad.Strong
open import Categories.Monad.Commutative
open import Categories.NaturalTransformation hiding (id)
open import Data.Product using (_,_)
open import Categories.Category.Monoidal.Braided
open import Categories.Category.Monoidal.Symmetric
import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR
import Categories.Morphism.Properties as MP
```
-->
# The maybe monad
```agda
module Monad.Instance.Maybe.Commutative {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) where
open Category C
open M C
open MR C
open MP C
open HomReasoning
open Equiv
open Distributive distributive
open import Categories.Category.Distributive.Properties distributive
open Cocartesian cocartesian
open Cartesian cartesian using (terminal; products)
open BinaryProducts products renaming (unique to ⟨⟩-unique)
open Terminal terminal
open CartesianMonoidal cartesian using (monoidal)
open import Monad.Instance.Maybe distributive
open import Monad.Instance.Maybe.Strong distributive
open Symmetric (symmetric C cartesian) using (braided)
open Commutative
distribute₄ : ∀ {A B C D} → (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ {A + B} {C} {D} ≈ [ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹
distribute₄ = Iso⇒Epi (IsIso.iso isIsoʳ) ((distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) ([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) (begin
(((distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) ∘ distributeʳ) ≈⟨ ∘[] ⟩
[ (((distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) ∘ (i₁ ⁂ id)) , (((distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) ∘ (i₂ ⁂ id)) ] ≈⟨ []-cong₂ (pullʳ ((refl⟩∘⟨ (⁂-cong₂ refl (sym (+-unique id-comm-sym id-comm-sym)))) ○ sym (distributeˡ⁻¹-natural i₁ id id))) (pullʳ (((refl⟩∘⟨ (⁂-cong₂ refl (sym (+-unique id-comm-sym id-comm-sym)))) ○ sym (distributeˡ⁻¹-natural i₂ id id)))) ⟩
[ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ ((i₁ ⁂ id) +₁ (i₁ ⁂ id)) ∘ distributeˡ⁻¹ , (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ ((i₂ ⁂ id) +₁ (i₂ ⁂ id)) ∘ distributeˡ⁻¹ ] ≈⟨ []-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ distributeʳ⁻¹-i₁ distributeʳ⁻¹-i₁)) (pullˡ (+₁∘+₁ ○ +₁-cong₂ distributeʳ⁻¹-i₂ distributeʳ⁻¹-i₂)) ⟩
[ (i₁ +₁ i₁) ∘ distributeˡ⁻¹ , (i₂ +₁ i₂) ∘ distributeˡ⁻¹ ] ≈˘⟨ []∘+₁ ⟩
([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹)) ≈˘⟨ pullʳ (cancelʳ (IsIso.isoˡ isIsoʳ)) ⟩
(([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ distributeʳ) ∎)
commutativeMaybe : Commutative braided maybeStrong
commutativeMaybe .commutes {X} {Y} = begin
[ id , i₂ ] ∘ ((swap +₁ id) ∘ ((id +₁ !) ∘ distributeˡ⁻¹) ∘ swap +₁ id) ∘ (id +₁ !) ∘ distributeˡ⁻¹ ≈⟨ refl⟩∘⟨ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ identityˡ)) ⟩
[ id , i₂ ] ∘ ((swap +₁ id) ∘ ((id +₁ !) ∘ distributeˡ⁻¹) ∘ swap +₁ !) ∘ distributeˡ⁻¹ ≈⟨ pullˡ ([]∘+₁ ○ []-cong₂ identityˡ refl) ⟩
[ (swap +₁ id) ∘ ((id +₁ !) ∘ distributeˡ⁻¹) ∘ swap , i₂ ∘ ! ] ∘ distributeˡ⁻¹ ≈⟨ ([]-cong₂ (refl⟩∘⟨ (pullʳ distributeˡ⁻¹∘swap)) (refl⟩∘⟨ !-unique (! ∘ distributeʳ⁻¹))) ⟩∘⟨refl ⟩
[ (swap +₁ id) ∘ (id +₁ !) ∘ (swap +₁ swap) ∘ distributeʳ⁻¹ , i₂ ∘ ! ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ≈˘⟨ pullˡ ([]∘+₁ ○ []-cong₂ assoc²' assoc) ⟩
[ (swap +₁ id) ∘ (id +₁ !) ∘ (swap +₁ swap) , i₂ ∘ ! ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ≈⟨ refl⟩∘⟨ distribute₄ ⟩
[ (swap +₁ id) ∘ (id +₁ !) ∘ (swap +₁ swap) , i₂ ∘ ! ] ∘ [ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ≈⟨ pullˡ ∘[] ⟩
[ [ (swap +₁ id) ∘ (id +₁ !) ∘ (swap +₁ swap) , i₂ ∘ ! ] ∘ (i₁ +₁ i₁) , [ (swap +₁ id) ∘ (id +₁ !) ∘ (swap +₁ swap) , i₂ ∘ ! ] ∘ (i₂ +₁ i₂) ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ≈⟨ ([]-cong₂ []∘+₁ []∘+₁) ⟩∘⟨refl ⟩
[ [ ((swap +₁ id) ∘ (id +₁ !) ∘ (swap +₁ swap)) ∘ i₁ , (i₂ ∘ !) ∘ i₁ ] , [ ((swap +₁ id) ∘ (id +₁ !) ∘ (swap +₁ swap)) ∘ i₂ , (i₂ ∘ !) ∘ i₂ ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ≈⟨ ([]-cong₂ ([]-cong₂ (pullʳ (pullʳ inject₁)) (pullʳ (sym (!-unique (! ∘ i₁))))) ([]-cong₂ (pullʳ (pullʳ inject₂)) (pullʳ (sym (!-unique (! ∘ i₂)))))) ⟩∘⟨refl ⟩
[ [ (swap +₁ id) ∘ (id +₁ !) ∘ i₁ ∘ swap , i₂ ∘ ! ] , [ (swap +₁ id) ∘ (id +₁ !) ∘ i₂ ∘ swap , i₂ ∘ ! ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ≈⟨ ([]-cong₂ ([]-cong₂ (refl⟩∘⟨ (pullˡ (inject₁ ○ identityʳ))) refl) ([]-cong₂ (refl⟩∘⟨ (pullˡ inject₂)) refl)) ⟩∘⟨refl ⟩
[ [ (swap +₁ id) ∘ i₁ ∘ swap , i₂ ∘ ! ] , [ (swap +₁ id) ∘ (i₂ ∘ !) ∘ swap , i₂ ∘ ! ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ≈⟨ ([]-cong₂ ([]-cong₂ (pullˡ inject₁) refl) ([]-cong₂ (pullˡ (pullˡ (inject₂ ○ identityʳ))) refl)) ⟩∘⟨refl ⟩
[ [ (i₁ ∘ swap) ∘ swap , i₂ ∘ ! ] , [ (i₂ ∘ !) ∘ swap , i₂ ∘ ! ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ≈⟨ ([]-cong₂ ([]-cong₂ (pullʳ swap∘swap) refl) ([]-cong₂ (pullʳ (sym (!-unique (! ∘ swap)))) refl)) ⟩∘⟨refl ⟩
[ id +₁ ! , [ i₂ ∘ ! , i₂ ∘ ! ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ≈⟨ pullˡ []∘+₁ ⟩
[ (id +₁ !) ∘ distributeˡ⁻¹ , [ i₂ ∘ ! , i₂ ∘ ! ] ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ≈⟨ ([]-cong₂ refl ((sym ∘[]) ⟩∘⟨refl)) ⟩∘⟨refl ⟩
[ (id +₁ !) ∘ distributeˡ⁻¹ , (i₂ ∘ [ ! , ! ]) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ≈⟨ ([]-cong₂ refl (pullʳ (sym (!-unique ([ ! , ! ] ∘ distributeˡ⁻¹))))) ⟩∘⟨refl ⟩
[ (id +₁ !) ∘ distributeˡ⁻¹ , i₂ ∘ ! ] ∘ distributeʳ⁻¹ ≈˘⟨ ([]-cong₂ (cancelʳ swap∘swap) (pullʳ (sym (!-unique (! ∘ swap))))) ⟩∘⟨refl ⟩
[ (((id +₁ !) ∘ distributeˡ⁻¹) ∘ swap) ∘ swap , (i₂ ∘ !) ∘ swap ] ∘ distributeʳ⁻¹ ≈˘⟨ pullˡ []∘+₁ ⟩
[ ((id +₁ !) ∘ distributeˡ⁻¹) ∘ swap , i₂ ∘ ! ] ∘ (swap +₁ swap) ∘ distributeʳ⁻¹ ≈˘⟨ pullʳ distributeˡ⁻¹∘swap ⟩
([ ((id +₁ !) ∘ distributeˡ⁻¹) ∘ swap , i₂ ∘ ! ] ∘ distributeˡ⁻¹) ∘ swap ≈˘⟨ pullˡ (pullˡ ([]∘+₁ ○ []-cong₂ identityˡ (refl⟩∘⟨ identityˡ))) ⟩
[ id , i₂ ] ∘ (((((id +₁ !) ∘ distributeˡ⁻¹) ∘ swap) +₁ id ∘ !) ∘ distributeˡ⁻¹) ∘ swap ≈˘⟨ refl⟩∘⟨ (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²) ○ pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ refl))) ⟩
[ id , i₂ ] ∘ ((id +₁ !) ∘ distributeˡ⁻¹ +₁ id) ∘ (swap +₁ id) ∘ ((id +₁ !) ∘ distributeˡ⁻¹) ∘ swap ∎
```

61
agda/src/Monad/Instance/Maybe/EquationalLifting.lagda.md Normal file
View file

@ -0,0 +1,61 @@
<!--
```agda
open import Level
open import Categories.Category.Core
open import Categories.Category.Cocartesian
open import Categories.Category.Cartesian
open import Categories.Category.BinaryProducts
open import Categories.Category.Cartesian.Monoidal
open import Categories.Category.Cartesian.SymmetricMonoidal
open import Categories.Category.Distributive
open import Categories.Functor hiding (id)
open import Categories.Object.Terminal
open import Categories.Monad
open import Categories.Monad.Strong
open import Categories.Monad.Commutative
open import Categories.NaturalTransformation hiding (id)
import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR
import Categories.Morphism.Properties as MP
```
-->
# The maybe monad
```agda
module Monad.Instance.Maybe.EquationalLifting {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) where
open Category C
open M C
open MR C
open MP C
open HomReasoning
open Equiv
open Distributive distributive
open import Categories.Category.Distributive.Properties distributive
open Cocartesian cocartesian
open Cartesian cartesian using (terminal; products)
open BinaryProducts products renaming (unique to ⟨⟩-unique)
open Terminal terminal
open CartesianMonoidal cartesian using (monoidal)
equationalLifting : ∀ {X} → ((id +₁ !) ∘ distributeˡ⁻¹) ∘ Δ {X + ⊤} ≈ ⟨ i₁ , id ⟩ +₁ id
equationalLifting = sym (+-unique inj₁ inj₂)
where
inj₁ : (((id +₁ !) ∘ distributeˡ⁻¹) ∘ Δ) ∘ i₁ ≈ i₁ ∘ ⟨ i₁ , id ⟩
inj₁ = begin
(((id +₁ !) ∘ distributeˡ⁻¹) ∘ Δ) ∘ i₁ ≈⟨ pullʳ Δ∘ ⟩
((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ i₁ , i₁ ⟩ ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ) ⟩
((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ i₁) ∘ ⟨ i₁ , id ⟩ ≈⟨ pullʳ (pullˡ distributeˡ⁻¹-i₁) ⟩
(id +₁ !) ∘ i₁ ∘ ⟨ i₁ , id ⟩ ≈⟨ pullˡ (inject₁ ○ identityʳ) ⟩
i₁ ∘ ⟨ i₁ , id ⟩ ∎
inj₂ : (((id +₁ !) ∘ distributeˡ⁻¹) ∘ Δ) ∘ i₂ ≈ i₂ ∘ id
inj₂ = begin
(((id +₁ !) ∘ distributeˡ⁻¹) ∘ Δ) ∘ i₂ ≈⟨ pullʳ Δ∘ ⟩
((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ i₂ , i₂ ⟩ ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ) ⟩
((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ i₂) ∘ ⟨ i₂ , id ⟩ ≈⟨ pullʳ (pullˡ distributeˡ⁻¹-i₂) ⟩
(id +₁ !) ∘ i₂ ∘ ⟨ i₂ , id ⟩ ≈⟨ pullˡ inject₂ ⟩
(i₂ ∘ !) ∘ ⟨ i₂ , id ⟩ ≈⟨ pullʳ (sym (!-unique (! ∘ ⟨ i₂ , id ⟩))) ⟩
i₂ ∘ ! ≈⟨ refl⟩∘⟨ (!-unique id) ⟩
i₂ ∘ id ∎
```

102
agda/src/Monad/Instance/Maybe/Strong.lagda.md Normal file
View file

@ -0,0 +1,102 @@
<!--
```agda
open import Level
open import Categories.Category.Core
open import Categories.Category.Cocartesian
open import Categories.Category.Cartesian
open import Categories.Category.BinaryProducts
open import Categories.Category.Cartesian.Monoidal
open import Categories.Category.Distributive
open import Categories.Functor hiding (id)
open import Categories.Object.Terminal
open import Categories.Monad
open import Categories.Monad.Strong
open import Categories.NaturalTransformation hiding (id)
open import Data.Product using (_,_)
import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR
import Categories.Morphism.Properties as MP
```
-->
# The maybe monad
```agda
module Monad.Instance.Maybe.Strong {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) where
open Category C
open M C
open MR C
open MP C
open HomReasoning
open Equiv
open Distributive distributive
open import Categories.Category.Distributive.Properties distributive
open Cocartesian cocartesian
open Cartesian cartesian using (terminal; products)
open BinaryProducts products renaming (unique to ⟨⟩-unique)
open Terminal terminal
open CartesianMonoidal cartesian using (monoidal)
open import Monad.Instance.Maybe distributive
open StrongMonad using (M; strength)
open Strength renaming (identityˡ to s-identityˡ)
maybeStrong : StrongMonad monoidal
maybeStrong .M = maybeMonad
maybeStrong .strength .strengthen = ntHelper (record { η = λ X → (id +₁ !) ∘ distributeˡ⁻¹ ; commute = λ {X} {Y} (f , g) → begin
((id +₁ !) ∘ distributeˡ⁻¹) ∘ (f ⁂ (g +₁ id)) ≈⟨ pullʳ (sym (distributeˡ⁻¹-natural f g id)) ⟩
(id +₁ !) ∘ (f ⁂ g +₁ f ⁂ id) ∘ distributeˡ⁻¹ ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ (sym (!-unique (! ∘ (f ⁂ id))))) ⟩
(f ⁂ g +₁ !) ∘ distributeˡ⁻¹ ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ identityˡ) ⟩
(f ⁂ g +₁ id) ∘ (id +₁ !) ∘ distributeˡ⁻¹ ∎ })
maybeStrong .strength .s-identityˡ = begin
(π₂ +₁ id) ∘ (id +₁ !) ∘ distributeˡ⁻¹ ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ (identityˡ ○ !-unique π₂)) ⟩
(π₂ +₁ π₂) ∘ distributeˡ⁻¹ ≈⟨ distributeˡ⁻¹-π₂ ⟩
π₂ ∎
maybeStrong .strength .η-comm = begin
((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ i₁) ≈⟨ pullʳ distributeˡ⁻¹-i₁ ⟩
(id +₁ !) ∘ i₁ ≈⟨ inject₁ ○ identityʳ ⟩
i₁ ∎
maybeStrong .strength .μ-η-comm = begin
[ id , i₂ ] ∘ (((id +₁ !) ∘ distributeˡ⁻¹) +₁ id) ∘ (id +₁ !) ∘ distributeˡ⁻¹ ≈⟨ pullˡ ([]∘+₁ ○ []-cong₂ identityˡ identityʳ) ○ pullˡ ([]∘+₁ ○ []-cong₂ identityʳ refl) ⟩
[ (id +₁ !) ∘ distributeˡ⁻¹ , i₂ ∘ ! ] ∘ distributeˡ⁻¹ ≈⟨ Iso⇒Epi (IsIso.iso isIsoˡ) ([ (id +₁ !) ∘ distributeˡ⁻¹ , i₂ ∘ ! ] ∘ distributeˡ⁻¹) (((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ [ id , i₂ ])) (begin
([ (id +₁ !) ∘ distributeˡ⁻¹ , i₂ ∘ ! ] ∘ distributeˡ⁻¹) ∘ distributeˡ ≈⟨ cancelʳ (IsIso.isoˡ isIsoˡ) ⟩
[ (id +₁ !) ∘ distributeˡ⁻¹ , i₂ ∘ ! ] ≈˘⟨ []-cong₂ refl inject₂ ⟩
[ (id +₁ !) ∘ distributeˡ⁻¹ , (id +₁ !) ∘ i₂ ] ≈˘⟨ []-cong₂ refl (pullʳ distributeˡ⁻¹-i₂) ⟩
[ (id +₁ !) ∘ distributeˡ⁻¹ , ((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ i₂) ] ≈˘⟨ []-cong₂ (cancelʳ (⁂∘⁂ ○ ⁂-cong₂ identity² inject₁ ○ ⟨⟩-unique id-comm id-comm)) (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² inject₂)) ⟩
[ (((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ [ id , i₂ ])) ∘ (id ⁂ i₁) , (((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ [ id , i₂ ])) ∘ (id ⁂ i₂) ] ≈˘⟨ ∘[] ⟩
(((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ [ id , i₂ ])) ∘ distributeˡ ∎) ⟩
((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ [ id , i₂ ]) ∎
maybeStrong .strength .strength-assoc = Iso⇒Epi (IsIso.iso isIsoˡ) _ _ (begin
((⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ id) ∘ (id +₁ !) ∘ distributeˡ⁻¹) ∘ distributeˡ ≈⟨ pullʳ (cancelʳ (IsIso.isoˡ isIsoˡ)) ⟩
(⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ id) ∘ (id +₁ !) ≈⟨ +₁∘+₁ ○ +₁-cong₂ identityʳ identityˡ ⟩
⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ! ≈⟨ []-cong₂ (sym lhs) (sym rhs) ⟩
[ (((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ (id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ (π₁ ∘ π₁) ∘ (id ⁂ i₁) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (id ⁂ i₁) ⟩) , (((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ (id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ (π₁ ∘ π₁) ∘ (id ⁂ i₂) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (id ⁂ i₂) ⟩) ] ≈˘⟨ []-cong₂ (pullʳ (pullʳ ⟨⟩∘)) (pullʳ (pullʳ ⟨⟩∘)) ⟩
[ (((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ (id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (id ⁂ i₁) , (((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ (id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (id ⁂ i₂) ] ≈˘⟨ ∘[] ⟩
(((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ (id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ ∎)
where
lhs : ((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ (id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ (π₁ ∘ π₁) ∘ (id ⁂ i₁) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (id ⁂ i₁) ⟩ ≈ i₁ ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩
lhs = begin
((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ (id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ (π₁ ∘ π₁) ∘ (id ⁂ i₁) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (id ⁂ i₁) ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ (pullʳ (project₁ ○ identityˡ)) (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ (project₁ ○ identityˡ)) project₂) ⟩
((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ (id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , i₁ ∘ π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl) ⟩
((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₂ ∘ π₁ , i₁ ∘ π₂ ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl))) ⟩
((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ i₁) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (pullˡ (pullʳ distributeˡ⁻¹-i₁))) ⟩
((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ((id +₁ !) ∘ i₁) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl ((inject₁ ○ identityʳ) ⟩∘⟨refl)) ⟩
((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , i₁ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl) ⟩
((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ i₁) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ pullˡ (pullʳ distributeˡ⁻¹-i₁) ⟩
((id +₁ !) ∘ i₁) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ (inject₁ ○ identityʳ) ⟩∘⟨refl ⟩
i₁ ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∎
rhs : (((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ (id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ (π₁ ∘ π₁) ∘ (id ⁂ i₂) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (id ⁂ i₂) ⟩) ≈ i₂ ∘ !
rhs = begin
(((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ (id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ (π₁ ∘ π₁) ∘ (id ⁂ i₂) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (id ⁂ i₂) ⟩) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ (pullʳ (project₁ ○ identityˡ)) (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ (project₁ ○ identityˡ)) project₂) ⟩
((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ (id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , i₂ ∘ π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl) ⟩
((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₂ ∘ π₁ , i₂ ∘ π₂ ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl))) ⟩
((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ i₂) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (pullˡ (pullʳ distributeˡ⁻¹-i₂))) ⟩
((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ((id +₁ !) ∘ i₂) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (inject₂ ⟩∘⟨refl)) ⟩
((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , (i₂ ∘ !) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (pullʳ (sym (!-unique (! ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩))))) ⟩
((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , i₂ ∘ ! ⟩ ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl) ⟩
((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ i₂) ∘ ⟨ π₁ ∘ π₁ , ! ⟩ ≈⟨ pullˡ (pullʳ distributeˡ⁻¹-i₂) ⟩
((id +₁ !) ∘ i₂) ∘ ⟨ π₁ ∘ π₁ , ! ⟩ ≈⟨ inject₂ ⟩∘⟨refl ⟩
(i₂ ∘ !) ∘ ⟨ π₁ ∘ π₁ , ! ⟩ ≈⟨ pullʳ (sym (!-unique (! ∘ ⟨ π₁ ∘ π₁ , ! ⟩))) ⟩
i₂ ∘ ! ∎
```