Add monoidal category of finite relations

1 files changed, 657 insertions, 0 deletions

diff --git a/Data/WiringDiagram/FinRel.agda b/Data/WiringDiagram/FinRel.agda
new file mode 100644
index 0000000..0a60528
--- /dev/null
+++ b/Data/WiringDiagram/FinRel.agda
@@ -0,0 +1,657 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.WiringDiagram.FinRel where
+
+open import Categories.Category using (Category)
+open import Categories.Category.Helper using (categoryHelper)
+open import Data.Fin using (Fin; splitAt; _↑ˡ_; _↑ʳ_; cast)
+open import Data.Fin.Properties using (splitAt⁻¹-↑ˡ; splitAt⁻¹-↑ʳ; splitAt-↑ˡ; splitAt-↑ʳ; ↑ˡ-injective; cast-is-id; cast-involutive; cast-trans)
+open import Data.Nat using (ℕ)
+open import Data.Nat.Properties using (+-assoc)
+open import Data.Product using (_,_; swap)
+open import Function using (flip; id; _∘_)
+open import Level using (0ℓ; suc)
+open import Relation.Binary using (REL; _⇒_; _⇔_)
+open import Relation.Binary.Construct.Composition using (_;_)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning)
+
+FinRel : Category 0ℓ (suc 0ℓ) 0ℓ
+FinRel = categoryHelper record
+    { Obj = ℕ
+    ; _⇒_ = λ n m → REL (Fin n) (Fin m) 0ℓ
+    ; _≈_ = _⇔_
+    ; id = _≡_
+    ; _∘_ = flip _;_
+    ; assoc = (λ (a , b , c , d , e) → c , (a , b , d) , e) , λ (a , (b , c , d) , e) → b , c , a , d , e
+    ; identityˡ = (λ { (_ , f[x,y] , ≡.refl) → f[x,y] }) , λ {x y} f[x,y] → y , f[x,y] , ≡.refl
+    ; identityʳ = (λ { (_ , ≡.refl , f[x,y]) → f[x,y] }) , λ {x y} f[x,y] → x , ≡.refl , f[x,y]
+    ; equiv = record
+        { refl = id , id
+        ; sym = swap
+        ; trans = λ (x , y) (x′ , y′) → x′ ∘ x , y ∘ y′
+        }
+    ; ∘-resp-≈ = λ (f⇒h , h⇒i) (g⇒i , i⇒g) → (λ (z , g-x-z , f-z-y) → z , g⇒i g-x-z , f⇒h f-z-y) , λ (z , i-x-z , h-z-y) → z , i⇒g i-x-z , h⇒i h-z-y
+    }
+
+open import Categories.Category.Monoidal using (Monoidal)
+open import Categories.Functor.Bifunctor using (Bifunctor)
+open import Data.Nat using (_+_)
+open import Data.Product using (_×_; Σ; Σ-syntax)
+open import Data.Sum using (_⊎_)
+open import Data.Sum.Properties using (inj₁-injective; inj₂-injective)
+open import Data.Empty using (⊥)
+open _⊎_
+
+opaque
+  _+₁_
+      : {A B C D : ℕ}
+      → REL (Fin A) (Fin B) 0ℓ
+      → REL (Fin C) (Fin D) 0ℓ
+      → REL (Fin (A + C)) (Fin (B + D)) 0ℓ
+  _+₁_ {A} {B} {C} {D} R S x y with splitAt A x | splitAt B y
+  ... | inj₁ x | inj₁ y = R x y
+  ... | inj₁ x | inj₂ y = ⊥
+  ... | inj₂ x | inj₁ y = ⊥
+  ... | inj₂ x | inj₂ y = S x y
+
+infixr 7 _+₁_
+
+opaque
+  unfolding _+₁_
+  +₁-⊎
+      : {A B C D : ℕ}
+        {R : REL (Fin A) (Fin B) 0ℓ}
+        {S : REL (Fin C) (Fin D) 0ℓ}
+        {x : Fin (A + C)}
+        {y : Fin (B + D)}
+      → (R +₁ S) x y
+      → Σ[ x′ ∈ Fin A ] Σ[ y′ ∈ Fin B ] (R x′ y′ × x ≡ x′ ↑ˡ C × y ≡ y′ ↑ˡ D)
+      ⊎ Σ[ x′ ∈ Fin C ] Σ[ y′ ∈ Fin D ] (S x′ y′ × x ≡ A ↑ʳ x′ × y ≡ B ↑ʳ y′)
+  +₁-⊎ {A} {B} {x = x} {y} RS with splitAt A x in eq₁ | splitAt B y in eq₂
+  ... | inj₁ x₁ | inj₁ x₂ = inj₁ (x₁ , x₂ , RS , ≡.sym (splitAt⁻¹-↑ˡ eq₁) , ≡.sym (splitAt⁻¹-↑ˡ eq₂))
+  ... | inj₂ y₁ | inj₂ y₂ = inj₂ (y₁ , y₂ , RS , ≡.sym (splitAt⁻¹-↑ʳ eq₁) , ≡.sym (splitAt⁻¹-↑ʳ eq₂))
+
+opaque
+
+  unfolding _+₁_
+
+  ↑ˡ-REL
+      : {X Y X′ Y′ : ℕ}
+        {x : Fin X}
+        {y : Fin Y}
+        {f : REL (Fin X) (Fin Y) 0ℓ}
+        {f′ : REL (Fin X′) (Fin Y′) 0ℓ}
+      → f x y
+      → (f +₁ f′) (x ↑ˡ X′) (y ↑ˡ Y′)
+  ↑ˡ-REL {X} {Y} {X′} {Y′} {x} {y} f-x-y
+    rewrite splitAt-↑ˡ X x X′
+    rewrite splitAt-↑ˡ Y y Y′ = f-x-y
+
+  ↑ʳ-REL
+      : {X Y X′ Y′ : ℕ}
+        {x′ : Fin X′}
+        {y′ : Fin Y′}
+        {f : REL (Fin X) (Fin Y) 0ℓ}
+        {f′ : REL (Fin X′) (Fin Y′) 0ℓ}
+      → f′ x′ y′
+      → (f +₁ f′) (X ↑ʳ x′) (Y ↑ʳ y′)
+  ↑ʳ-REL {X} {Y} {X′} {Y′} {x′} {y′} f′-x′-y′
+    rewrite splitAt-↑ʳ X X′ x′
+    rewrite splitAt-↑ʳ Y Y′ y′ = f′-x′-y′
+
+opaque
+  unfolding _+₁_
+  +₁-≡ : {A B : ℕ} {x y : Fin (A + B)} → ((_≡_ {A = Fin A}) +₁ _≡_) x y → x ≡ y
+  +₁-≡ {A} {B} {x} {y} x≡y₁₂ with splitAt A x in eq₁ | splitAt A y in eq₂
+  ... | inj₁ x₁ | inj₁ y₁ = ≡.trans (≡.sym (splitAt⁻¹-↑ˡ eq₁)) (≡.trans (≡.cong (_↑ˡ B) x≡y₁₂) (splitAt⁻¹-↑ˡ eq₂))
+  ... | inj₂ x₂ | inj₂ y₂ = ≡.trans (≡.sym (splitAt⁻¹-↑ʳ eq₁)) (≡.trans (≡.cong (A ↑ʳ_) x≡y₁₂) (splitAt⁻¹-↑ʳ eq₂))
+
+opaque
+  unfolding _+₁_
+  ≡-+₁ : {A B : ℕ} {x y : Fin (A + B)} → x ≡ y → ((_≡_ {A = Fin A}) +₁ _≡_) x y
+  ≡-+₁ {A} {B} {x} {y} x≡y with splitAt A x in eq₁ | splitAt A y in eq₂
+  ... | inj₁ x′ | inj₁ y′ = inj₁-injective (≡.trans (≡.sym eq₁) (≡.trans (≡.cong (splitAt A) x≡y) eq₂))
+  ... | inj₁ x′ | inj₂ y′ with () ← ≡.trans (≡.sym eq₁) (≡.trans (≡.cong (splitAt A) x≡y) eq₂)
+  ... | inj₂ x′ | inj₁ y′ with () ← ≡.trans (≡.sym eq₁) (≡.trans (≡.cong (splitAt A) x≡y) eq₂)
+  ... | inj₂ x′ | inj₂ y′ = inj₂-injective (≡.trans (≡.sym eq₁) (≡.trans (≡.cong (splitAt A) x≡y) eq₂))
+
+;-+₁
+    : {X X′ Y Y′ Z Z′ : ℕ}
+      (f : REL (Fin X) (Fin Y) 0ℓ)
+      (f′ : REL (Fin X′) (Fin Y′) 0ℓ)
+      (g : REL (Fin Y) (Fin Z) 0ℓ)
+      (g′ : REL (Fin Y′) (Fin Z′) 0ℓ)
+      (x : Fin (X + X′))
+      (y : Fin (Z + Z′))
+    → (f ; g +₁ f′ ; g′) x y
+    → ((f +₁ f′) ; (g +₁ g′)) x y
+;-+₁ {X} {X′} {Y} {Y′} {Z} {Z′} f f′ g g′ x y BER with +₁-⊎ BER
+... | inj₁ (x′ , z′ , (y , f-x′-y , g-y-z) , eq , eq₂)
+        rewrite eq
+        rewrite eq₂ = y ↑ˡ Y′ , ↑ˡ-REL f-x′-y , ↑ˡ-REL g-y-z
+... | inj₂ (x′ , y′ , (z , f′-x′-z′ , g′-z-y′) , eq₁ , eq₂)
+        rewrite eq₁
+        rewrite eq₂ = Y ↑ʳ z  , ↑ʳ-REL f′-x′-z′ , ↑ʳ-REL g′-z-y′
+
+opaque
+  unfolding _+₁_
+  +₁-;
+      : {X X′ Y Y′ Z Z′ : ℕ}
+        (f : REL (Fin X) (Fin Y) 0ℓ)
+        (f′ : REL (Fin X′) (Fin Y′) 0ℓ)
+        (g : REL (Fin Y) (Fin Z) 0ℓ)
+        (g′ : REL (Fin Y′) (Fin Z′) 0ℓ)
+        (x : Fin (X + X′))
+        (y : Fin (Z + Z′))
+      → ((f +₁ f′) ; (g +₁ g′)) x y
+      → (f ; g +₁ f′ ; g′) x y
+  +₁-; {X} {X′} {Y} {Y′} {Z} {Z′} f f′ g g′ x z (y , fxygyz)
+    with splitAt X x | splitAt Y y | splitAt Z z
+  ... | inj₁ x′ | inj₁ y′ | inj₁ z′ = y′ , fxygyz
+  ... | inj₂ x′ | inj₂ y′ | inj₂ z′ = y′ , fxygyz
+
+module _ {A A′ B B′ : ℕ} {f g : REL (Fin A) (Fin B) 0ℓ} {f′ g′ : REL (Fin A′) (Fin B′) 0ℓ} where
+
+  +₁-resp-⇒ : f ⇒ g → f′ ⇒ g′ → f +₁ f′ ⇒ g +₁ g′
+  +₁-resp-⇒ f⇒g f′⇒g′ f+f′-a-b with +₁-⊎ f+f′-a-b
+  ... | inj₁ (a , b , f-a-b , ≡a↑ˡA′ , ≡b↑ˡB′) rewrite ≡a↑ˡA′ rewrite ≡b↑ˡB′ = ↑ˡ-REL (f⇒g f-a-b)
+  ... | inj₂ (a , b , f′-a-b , ≡A↑ʳa , ≡B↑ʳb) rewrite ≡A↑ʳa rewrite ≡B↑ʳb = ↑ʳ-REL (f′⇒g′ f′-a-b)
+
+⊗ : Bifunctor FinRel FinRel FinRel
+⊗ = record
+    { F₀ = λ (n , m) → n + m
+    ; F₁ = λ (f , g) → f +₁ g
+    ; identity = λ { {A , B} → +₁-≡ {A} {B} , ≡-+₁ {A} {B} }
+    ; homomorphism = λ { {X , X′} {Y , Y′} {Z , Z′} {f , f′} {g , g′} →
+        (λ { {x} {y} → ;-+₁ f f′ g g′ x y }) , (λ { {x} {y} → +₁-; f f′ g g′ x y }) }
+    ; F-resp-≈ = λ { {A , A′} {B , B′} {f , f′} {g , g′} ((f⇒g , g⇒f) , (f′⇒g′ , g′⇒f′))
+        → +₁-resp-⇒ f⇒g f′⇒g′ , +₁-resp-⇒ g⇒f g′⇒f′ }
+    }
+
+module _ {X : ℕ} where
+
+  ρ⇒ : REL (Fin (X + 0)) (Fin X) 0ℓ
+  ρ⇒ x+0 y with inj₁ x ← splitAt X x+0 = x ≡ y
+
+  ρ⇐ : REL (Fin X) (Fin (X + 0)) 0ℓ
+  ρ⇐ x y+0 with inj₁ y ← splitAt X y+0 = x ≡ y
+
+  ρ⇒⇐-≡ : ρ⇒ ; ρ⇐ ⇒ _≡_
+  ρ⇒⇐-≡ {x+0} {y+0} (z , x≡z , z≡y) with splitAt X x+0 in eq₁ | splitAt X y+0 in eq₂
+  ... | inj₁ x | inj₁ y rewrite ≡.sym (splitAt⁻¹-↑ˡ eq₁) rewrite ≡.sym (splitAt⁻¹-↑ˡ eq₂) = ≡.cong (_↑ˡ 0) (≡.trans x≡z z≡y)
+
+  ≡-ρ⇒⇐ : _≡_ ⇒ ρ⇒ ; ρ⇐
+  ≡-ρ⇒⇐ {x+0} {y+0} x↑ˡ0≡y↑ˡ0 with splitAt X x+0 in eq₁ | splitAt X y+0 in eq₂
+  ... | inj₁ x | inj₁ y rewrite ≡.sym (splitAt⁻¹-↑ˡ eq₁) rewrite ≡.sym (splitAt⁻¹-↑ˡ eq₂) = (x , ≡.refl , ↑ˡ-injective 0 x y x↑ˡ0≡y↑ˡ0)
+
+  ρ⇐⇒-≡ : ρ⇐ ; ρ⇒ ⇒ _≡_
+  ρ⇐⇒-≡ {x} {y} (z , x≡z , z≡y) with inj₁ z ← splitAt X z = ≡.trans x≡z z≡y
+
+  ≡-ρ⇐⇒ : _≡_ ⇒ ρ⇐ ; ρ⇒
+  ≡-ρ⇐⇒ {x} {y} x≡y = x ↑ˡ 0 , lemma
+    where
+      lemma : ρ⇐ x (x ↑ˡ 0) × ρ⇒ (x ↑ˡ 0) y
+      lemma with splitAt X (x ↑ˡ 0) in eq
+      ... | inj₁ x′ = ≡.sym x′≡x , ≡.trans x′≡x x≡y
+        where
+          x′≡x : x′ ≡ x
+          x′≡x = ↑ˡ-injective 0 x′ x (splitAt⁻¹-↑ˡ eq)
+
+open import Categories.Morphism FinRel using (_≅_; module ≅)
+
+module _ {X : ℕ} where
+
+  unitorˡ : 0 + X ≅ X
+  unitorˡ = ≅.refl
+
+  unitorʳ : X + 0 ≅ X
+  unitorʳ = record
+      { from = ρ⇒
+      ; to = ρ⇐
+      ; iso = record
+          { isoˡ = ρ⇒⇐-≡ , ≡-ρ⇒⇐
+          ; isoʳ = ρ⇐⇒-≡ , ≡-ρ⇐⇒
+          }
+      }
+
+module _ {X Y Z : ℕ} where
+
+  α⇒ : REL (Fin (X + Y + Z)) (Fin (X + (Y + Z))) 0ℓ
+  α⇒ [xy]z x[yz] = cast (+-assoc X Y Z) [xy]z ≡ x[yz]
+
+  α⇐ : REL (Fin (X + (Y + Z))) (Fin ((X + Y) + Z)) 0ℓ
+  α⇐ x[yz] [xy]z = cast (≡.sym (+-assoc X Y Z)) x[yz] ≡ [xy]z
+
+  α⇒;α⇐-⇒ : α⇒ ; α⇐ ⇒ _≡_
+  α⇒;α⇐-⇒ {x} {y} (z , cast-x≡z , cast-z≡y) =
+      ≡.trans
+          (≡.sym (cast-involutive (≡.sym (+-assoc X Y Z)) (+-assoc X Y Z) x))
+          (≡.trans (≡.cong (cast _) cast-x≡z) cast-z≡y)
+
+  α⇒;α⇐-⇐ : _≡_ ⇒ α⇒ ; α⇐
+  α⇒;α⇐-⇐ {x} {y} x≡y = cast _ x , ≡.refl , ≡.trans (cast-involutive (≡.sym (+-assoc X Y Z)) (+-assoc X Y Z) x) x≡y
+
+  α⇐;α⇒-⇒ : α⇐ ; α⇒ ⇒ _≡_
+  α⇐;α⇒-⇒ {x} {y} (z , cast-x≡z , cast-z≡y) =
+      ≡.trans
+          (≡.sym (cast-involutive (+-assoc X Y Z) (≡.sym (+-assoc X Y Z)) x))
+          (≡.trans (≡.cong (cast _) cast-x≡z) cast-z≡y)
+
+  α⇐;α⇒-⇐ : _≡_ ⇒ α⇐ ; α⇒
+  α⇐;α⇒-⇐ {x} {y} x≡y = cast _ x , ≡.refl , ≡.trans (cast-involutive (+-assoc X Y Z) (≡.sym (+-assoc X Y Z)) x) x≡y
+
+  associator : (X + Y) + Z ≅ X + (Y + Z)
+  associator = record
+      { from = α⇒
+      ; to = α⇐
+      ; iso = record
+          { isoˡ = α⇒;α⇐-⇒ , α⇒;α⇐-⇐
+          ; isoʳ = α⇐;α⇒-⇒ , α⇐;α⇒-⇐
+          }
+      }
+
+module _ (X Y : ℕ) (R : REL (Fin X) (Fin Y) 0ℓ) where
+
+  left₁ : (_≡_ +₁ R) ; _≡_ ⇒ _≡_ ; R
+  left₁ (_ , e-x-y′ , ≡.refl) with +₁-⊎ e-x-y′
+  ... | inj₂ (x , y , xRy , ≡.refl , ≡.refl) = x , ≡.refl , xRy
+
+  right₁ : _≡_ ; R ⇒ (_≡_ +₁ R) ; _≡_
+  right₁ {x} {y} (x , ≡.refl , xRy) = y , ↑ʳ-REL xRy , ≡.refl
+
+  unitorˡ-commute-to : (_≡_ +₁ R) ; _≡_ ⇔ _≡_ ; R
+  unitorˡ-commute-to = left₁ , right₁
+
+  left₂ : R ; _≡_ ⇒ _≡_ ; (_≡_ +₁ R)
+  left₂ {x} {y} (y , xRy , ≡.refl) = x , ≡.refl , ↑ʳ-REL xRy
+
+  right₂ : _≡_ ; (_≡_ +₁ R) ⇒ R ; _≡_
+  right₂ (_ , ≡.refl , e-x-y) with +₁-⊎ e-x-y
+  ... | inj₂ (x , y , xRy , ≡.refl , ≡.refl) = y , xRy , ≡.refl
+
+  unitorˡ-commute-from : R ; _≡_ ⇔ _≡_ ; (_≡_ +₁ R)
+  unitorˡ-commute-from = left₂ , right₂
+
+  left₃ : (R +₁ _≡_) ; ρ⇒ ⇒ ρ⇒ ; R
+  left₃ {x+0} {y} (y+0 , e-x-y , y≡y) with +₁-⊎ e-x-y | splitAt X x+0 in eq₁ | splitAt Y y+0 in eq₂ | y≡y
+  ... | inj₁ (x″ , y″ , x″Ry″ , x+0≡x″↑ˡ0 , y+0≡y″↑ˡ0) | inj₁ x′ | inj₁ y′ | y≡y′
+    rewrite (≡.sym (↑ˡ-injective 0 x′ x″ (≡.trans (splitAt⁻¹-↑ˡ eq₁) x+0≡x″↑ˡ0)))
+    rewrite (≡.sym (↑ˡ-injective 0 y′ y″ (≡.trans (splitAt⁻¹-↑ˡ eq₂) y+0≡y″↑ˡ0)))
+    rewrite ≡.sym y≡y′ = x′ , ≡.refl , x″Ry″
+
+  right₃ : ρ⇒ ; R ⇒ (R +₁ _≡_) ; ρ⇒
+  right₃ {x+0} {y} (x , e-x-y , xRy) with splitAt X x+0 in eq₁
+  ... | inj₁ x′
+    rewrite ≡.sym (splitAt⁻¹-↑ˡ eq₁)
+    rewrite e-x-y = y ↑ˡ 0 , ↑ˡ-REL xRy , lemma
+      where
+        lemma : ρ⇒ (y ↑ˡ 0) y
+        lemma with splitAt Y (y ↑ˡ 0) in eq₂
+        ... | inj₁ y′ = ↑ˡ-injective 0 y′ y (splitAt⁻¹-↑ˡ eq₂)
+
+  unitorʳ-commute-from : (R +₁ _≡_) ; ρ⇒ ⇒ ρ⇒ ; R × ρ⇒ ; R ⇒ (R +₁ _≡_) ; ρ⇒
+  unitorʳ-commute-from = left₃ , right₃
+
+  left₄ : R ; ρ⇐ ⇒ ρ⇐ ; (R +₁ _≡_)
+  left₄ {x} {y+0} (y , xRy′ , y≡y′) with splitAt Y y+0 in eq₁
+  ... | inj₁ y′
+    rewrite ≡.sym (splitAt⁻¹-↑ˡ eq₁)
+    rewrite y≡y′
+        = x ↑ˡ 0 , lemma , ↑ˡ-REL xRy′
+    where
+      lemma : ρ⇐ x (x ↑ˡ 0)
+      lemma with splitAt X (x ↑ˡ 0) in eq₂
+      ... | inj₁ x′ = ↑ˡ-injective 0 x x′ (≡.sym (splitAt⁻¹-↑ˡ eq₂))
+
+  right₄ : ρ⇐ ; (R +₁ _≡_) ⇒ R ; ρ⇐
+  right₄ {x} {y+0} (x+0 , x≡x″ , e-x-y) with +₁-⊎ e-x-y | splitAt X x+0 in eq₁
+  ... | inj₁ (x′ , y′ , x′Ry′ , x+0≡x′↑ˡ0 , y+0≡y′↑ˡ0) | inj₁ x″
+    rewrite x≡x″
+    rewrite (↑ˡ-injective 0 x″ x′ (≡.trans (splitAt⁻¹-↑ˡ eq₁) x+0≡x′↑ˡ0))
+        = y′ , x′Ry′ , lemma
+      where
+        lemma : ρ⇐ y′ y+0
+        lemma with splitAt Y y+0 in eq₂
+        ... | inj₁ y″ = ↑ˡ-injective 0 y′ y″ (≡.sym (≡.trans (splitAt⁻¹-↑ˡ eq₂) y+0≡y′↑ˡ0))
+
+  unitorʳ-commute-to : R ; ρ⇐ ⇔ ρ⇐ ; (R +₁ _≡_)
+  unitorʳ-commute-to = left₄ , right₄
+
++-↑ʳ : (A B : ℕ) {C : ℕ} (c : Fin C) → cast (+-assoc A B C) (A + B ↑ʳ c) ≡ A ↑ʳ (B ↑ʳ c)
++-↑ʳ ℕ.zero B c = cast-is-id ≡.refl (B ↑ʳ c)
++-↑ʳ (ℕ.suc A) B c = ≡.cong Fin.suc (+-↑ʳ A B c)
+
+↑ˡ-+ : {A : ℕ} (a : Fin A) (B C : ℕ) → cast (+-assoc A B C) (a ↑ˡ B ↑ˡ C) ≡ a ↑ˡ (B + C)
+↑ˡ-+ Fin.zero B C = ≡.refl
+↑ˡ-+ (Fin.suc a) B C = ≡.cong Fin.suc (↑ˡ-+ a B C)
+
+↑ʳ-↑ˡ : (A : ℕ) {B : ℕ} (b : Fin B) (C : ℕ) → cast (+-assoc A B C) ((A ↑ʳ b) ↑ˡ C) ≡ A ↑ʳ (b ↑ˡ C)
+↑ʳ-↑ˡ ℕ.zero b C = cast-is-id ≡.refl (b ↑ˡ C)
+↑ʳ-↑ˡ (ℕ.suc A) b C = ≡.cong Fin.suc (↑ʳ-↑ˡ A b C)
+
+cast-↑ˡ : {A B : ℕ} (A≡B : A ≡ B) (x : Fin A) (C : ℕ) → cast A≡B x ↑ˡ C ≡ cast (≡.cong (_+ C) A≡B) (x ↑ˡ C)
+cast-↑ˡ ≡.refl x C
+  rewrite cast-is-id ≡.refl x
+  rewrite cast-is-id ≡.refl (x ↑ˡ C) = ≡.refl
+
+cast-↑ʳ : {B C : ℕ} (B≡C : B ≡ C) (A : ℕ) (x : Fin B) → A ↑ʳ cast B≡C x ≡ cast (≡.cong (A +_) B≡C) (A ↑ʳ x)
+cast-↑ʳ ≡.refl A x
+  rewrite cast-is-id ≡.refl x
+  rewrite cast-is-id ≡.refl (A ↑ʳ x) = ≡.refl
+
+↑ˡ-assoc : {X : ℕ} (x : Fin X) (Y Z W : ℕ) → x ↑ˡ Y + Z + W ≡ cast (≡.cong (X +_) (≡.sym (+-assoc Y Z W))) (x ↑ˡ Y + (Z + W))
+↑ˡ-assoc {X} x Y Z W = begin
+    x ↑ˡ Y + Z + W                                            ≡⟨ ↑ˡ-+ x (Y + Z) W ⟨
+    cast _ (x ↑ˡ Y + Z ↑ˡ W)                                  ≡⟨ ≡.cong (cast _ ∘ (_↑ˡ W)) (↑ˡ-+ x Y Z) ⟨
+    cast (+-assoc X (Y + Z) W) (cast _ (x ↑ˡ Y ↑ˡ Z) ↑ˡ W)    ≡⟨ ≡.cong (cast _) (cast-↑ˡ (+-assoc X Y Z) ((x ↑ˡ Y) ↑ˡ Z) W) ⟩
+    cast (+-assoc X (Y + Z) W) (cast _ (x ↑ˡ Y ↑ˡ Z ↑ˡ W))    ≡⟨ cast-trans _ (+-assoc X (Y + Z) W) (x ↑ˡ Y ↑ˡ Z ↑ˡ W) ⟩
+    cast _ (x ↑ˡ Y ↑ˡ Z ↑ˡ W)                                 ≡⟨ cast-trans (+-assoc (X + Y) Z W) _ (x ↑ˡ Y ↑ˡ Z ↑ˡ W) ⟨
+    cast _ (cast (+-assoc (X + Y) Z W) (x ↑ˡ Y ↑ˡ Z ↑ˡ W))    ≡⟨ ≡.cong (cast _) (↑ˡ-+ (x ↑ˡ Y) Z W)  ⟩
+    cast _ (x ↑ˡ Y ↑ˡ Z + W)                                  ≡⟨ cast-trans _ (≡.cong (X +_) (≡.sym (+-assoc Y Z W))) (x ↑ˡ Y ↑ˡ Z + W) ⟨
+    cast (≡.cong (X +_) (≡.sym (+-assoc Y Z W))) (cast  _ (x ↑ˡ Y ↑ˡ Z + W))  ≡⟨ ≡.cong (cast _) (↑ˡ-+ x Y (Z + W)) ⟩
+    cast _ (x ↑ˡ Y + (Z + W)) ∎
+  where
+    open ≡-Reasoning
+
+assoc-↑ʳ : (X Y Z : ℕ) {W : ℕ} (w : Fin W) → X + Y + Z ↑ʳ w ≡ cast (≡.cong (_+ W) (≡.sym (+-assoc X Y Z))) (X + (Y + Z) ↑ʳ w)
+assoc-↑ʳ X Y Z {W} w = begin
+    X + Y + Z ↑ʳ w                                                ≡⟨ cast-involutive (≡.sym (+-assoc (X + Y) Z W)) (+-assoc (X + Y) Z W) (X + Y + Z ↑ʳ w) ⟨
+    cast _ (cast (+-assoc (X + Y) Z W) (X + Y + Z ↑ʳ w))          ≡⟨ ≡.cong (cast _) (+-↑ʳ (X + Y) Z w) ⟩
+    cast _ (X + Y ↑ʳ (Z ↑ʳ w))                                    ≡⟨ cast-trans (+-assoc X Y (Z + W)) eq₂ (X + Y ↑ʳ (Z ↑ʳ w)) ⟨
+    cast _ (cast (+-assoc X Y (Z + W)) (X + Y ↑ʳ (Z ↑ʳ w)))       ≡⟨ ≡.cong (cast _) (+-↑ʳ X Y (Z ↑ʳ w)) ⟩
+    cast _ (X ↑ʳ Y ↑ʳ Z ↑ʳ w)                                     ≡⟨ cast-trans (≡.cong (_+_ X) (≡.sym (+-assoc Y Z W))) eq (X ↑ʳ Y ↑ʳ Z ↑ʳ w) ⟨
+    cast eq (cast _ (X ↑ʳ Y ↑ʳ Z ↑ʳ w))                          ≡⟨ ≡.cong (cast _) (cast-↑ʳ (≡.sym (+-assoc Y Z W)) X (Y ↑ʳ Z ↑ʳ w)) ⟨
+    cast _ (X ↑ʳ cast {Y + (Z + W)} {Y + Z + W} _ (Y ↑ʳ Z ↑ʳ w))  ≡⟨ ≡.cong (cast eq ∘ (X ↑ʳ_) ∘ cast _) (+-↑ʳ Y Z w) ⟨
+    cast _ (X ↑ʳ cast _ (cast (+-assoc Y Z W) (Y + Z ↑ʳ w)))      ≡⟨ ≡.cong (cast eq ∘ (X ↑ʳ_)) (cast-involutive (≡.sym (+-assoc Y Z W)) (+-assoc Y Z W) (Y + Z ↑ʳ w)) ⟩
+    cast eq (X ↑ʳ (Y + Z ↑ʳ w))                                  ≡⟨ ≡.cong (cast eq) (+-↑ʳ X (Y + Z) w) ⟨
+    cast eq (cast _ (X + (Y + Z) ↑ʳ w))                          ≡⟨ cast-trans (+-assoc X (Y + Z) W) eq (X + (Y + Z) ↑ʳ w) ⟩
+    cast _ (X + (Y + Z) ↑ʳ w)                                     ∎
+  where
+    open ≡-Reasoning
+    eq :  X + (Y + Z + W) ≡ X + Y + Z + W
+    eq = begin
+        X + (Y + Z + W) ≡⟨ +-assoc X (Y + Z) W ⟨
+        X + (Y + Z) + W ≡⟨ ≡.cong (_+ W) (+-assoc X Y Z) ⟨
+        X + Y + Z + W   ∎
+    eq₂ : X + (Y + (Z + W)) ≡ X + Y + Z + W
+    eq₂ = begin
+        X + (Y + (Z + W)) ≡⟨ +-assoc X Y (Z + W) ⟨
+        X + Y + (Z + W)   ≡⟨ +-assoc (X + Y) Z W ⟨
+        X + Y + Z + W     ∎
+
+module _
+    {X Y X′ Y′ X″ Y″ : ℕ}
+    {R : REL (Fin X) (Fin Y) 0ℓ}
+    {S : REL (Fin X′) (Fin Y′) 0ℓ}
+    {T : REL (Fin X″) (Fin Y″) 0ℓ}
+  where
+
+  +₁-assoc-⇒
+      : {x : Fin (X + X′ + X″)}
+        {y : Fin (Y + Y′ + Y″)}
+      → ((R +₁ S) +₁ T) x y
+      → (R +₁ (S +₁ T)) (cast (+-assoc X X′ X″) x) (cast (+-assoc Y Y′ Y″) y)
+  +₁-assoc-⇒ xxxRSTyyy with +₁-⊎ xxxRSTyyy
+  ... | inj₂ (x , y , xTy , ≡.refl , ≡.refl) rewrite +-↑ʳ X X′ x rewrite +-↑ʳ Y Y′ y
+            = ↑ʳ-REL (↑ʳ-REL xTy)
+  ... | inj₁ (xx , yy , xxRSyy , ≡.refl , ≡.refl) with +₁-⊎ xxRSyy 
+  ...   | inj₁ (x , y , xRy , ≡.refl , ≡.refl) rewrite ↑ˡ-+ x X′ X″ rewrite ↑ˡ-+ y Y′ Y″ = ↑ˡ-REL xRy
+  ...   | inj₂ (x , y , xSy , ≡.refl , ≡.refl) rewrite ↑ʳ-↑ˡ X x X″ rewrite ↑ʳ-↑ˡ Y y Y″ = ↑ʳ-REL (↑ˡ-REL xSy)
+
+  +₁-assoc-⇐
+      : {x : Fin (X + (X′ + X″))}
+        {y : Fin (Y + (Y′ + Y″))}
+      → (R +₁ (S +₁ T)) x y
+      → ((R +₁ S) +₁ T) (cast (≡.sym (+-assoc X X′ X″)) x) (cast (≡.sym (+-assoc Y Y′ Y″)) y)
+  +₁-assoc-⇐ xxxRSTyyy with +₁-⊎ xxxRSTyyy
+  ... | inj₁ (x , y , xRy , ≡.refl , ≡.refl)
+          rewrite ≡.sym (↑ˡ-+ x X′ X″)
+          rewrite ≡.sym (↑ˡ-+ y Y′ Y″)
+          rewrite cast-involutive (≡.sym (+-assoc X X′ X″)) (+-assoc X X′ X″) (x ↑ˡ X′ ↑ˡ X″)
+          rewrite cast-involutive (≡.sym ((+-assoc Y Y′ Y″))) (+-assoc Y Y′ Y″) (y ↑ˡ Y′ ↑ˡ Y″)
+        = ↑ˡ-REL (↑ˡ-REL xRy)
+  ... | inj₂ (xx , yy , xxSTyy , ≡.refl , ≡.refl) with +₁-⊎ xxSTyy
+  ...   | inj₁ (x , y , xSy , ≡.refl , ≡.refl)
+            rewrite ≡.sym (↑ʳ-↑ˡ X x X″)
+            rewrite ≡.sym (↑ʳ-↑ˡ Y y Y″)
+            rewrite cast-involutive (≡.sym (+-assoc X X′ X″)) (+-assoc X X′ X″) ((X ↑ʳ x) ↑ˡ X″)
+            rewrite cast-involutive (≡.sym (+-assoc Y Y′ Y″)) (+-assoc Y Y′ Y″) ((Y ↑ʳ y) ↑ˡ Y″)
+          = ↑ˡ-REL (↑ʳ-REL xSy)
+  ...   | inj₂ (x , y , xTy , ≡.refl , ≡.refl)
+            rewrite ≡.sym (+-↑ʳ X X′ x)
+            rewrite ≡.sym (+-↑ʳ Y Y′ y)
+            rewrite cast-involutive (≡.sym (+-assoc X X′ X″)) (+-assoc X X′ X″) (X + X′ ↑ʳ x)
+            rewrite cast-involutive (≡.sym (+-assoc Y Y′ Y″)) (+-assoc Y Y′ Y″) (Y + Y′ ↑ʳ y)
+          = ↑ʳ-REL xTy
+
+module _
+    (X Y X′ Y′ X″ Y″ : ℕ)
+    (R : REL (Fin X) (Fin Y) 0ℓ)
+    (S : REL (Fin X′) (Fin Y′) 0ℓ)
+    (T : REL (Fin X″) (Fin Y″) 0ℓ)
+  where
+
+  left₅ : ((R +₁ S) +₁ T) ; α⇒ {Y} ⇒ α⇒ {X} ; (R +₁ S +₁ T)
+  left₅ {x} {y} (y′ , RST-x-y′ , y′≡y) rewrite ≡.sym y′≡y = cast (+-assoc X X′ X″) x , ≡.refl , +₁-assoc-⇒ RST-x-y′
+
+  right₅ : α⇒ {X} ; (R +₁ S +₁ T) ⇒ ((R +₁ S) +₁ T) ; α⇒ {Y}
+  right₅ {x} {y} (x′ , x≡x′ , x′RSTy)
+    rewrite ≡.trans (≡.sym (cast-involutive _ (+-assoc X X′ X″) x)) (≡.cong (cast (≡.sym (+-assoc X X′ X″))) x≡x′)
+      = cast (≡.sym (+-assoc Y Y′ Y″)) y , +₁-assoc-⇐ x′RSTy , cast-involutive (+-assoc Y Y′ Y″) _ y
+
+  assoc-commute-from : ((R +₁ S) +₁ T) ; α⇒ {Y} ⇔ α⇒ {X} ; (R +₁ S +₁ T)
+  assoc-commute-from = left₅ , right₅
+
+  left₆ : (R +₁ S +₁ T) ; α⇐ {Y} ⇒ α⇐ {X} ; ((R +₁ S) +₁ T)
+  left₆ {xxx} {yyy} (yyy′ , xxxRSTyyy′ , ≡.refl)
+      = cast (≡.sym (+-assoc X X′ X″)) xxx , ≡.refl , +₁-assoc-⇐ xxxRSTyyy′
+
+  right₆ : α⇐ {X} ; ((R +₁ S) +₁ T) ⇒ (R +₁ S +₁ T) ; α⇐ {Y}
+  right₆ {xxx} {yyy} (xxx′ , xxx≡xxx′ , xxx′RSTyyy)
+    rewrite ≡.trans (≡.sym (cast-involutive (+-assoc X X′ X″) _ xxx)) (≡.cong (cast (+-assoc X X′ X″)) (xxx≡xxx′))
+      = cast (+-assoc Y Y′ Y″) yyy , +₁-assoc-⇒ xxx′RSTyyy , cast-involutive (≡.sym (+-assoc Y Y′ Y″)) _ yyy
+
+  assoc-commute-to : (R +₁ S +₁ T) ; α⇐ {Y} ⇔ α⇐ {X} ; ((R +₁ S) +₁ T)
+  assoc-commute-to = left₆ , right₆
+
+module _ (X Y : ℕ) where
+
+  triˡ : α⇒ {X} ; (_≡_ {A = Fin X} +₁ _≡_) ⇒ ρ⇒ +₁ _≡_ {A = Fin Y}
+  triˡ {[x0]y} {x[0y]} (x[0y]′ , ≡.refl , e-[x0]y-x[0y]) with +₁-⊎ e-[x0]y-x[0y]
+  ... | inj₁ (x , x , ≡.refl , cast[x0]y≡x↑ˡY , ≡.refl)
+          rewrite ≡.trans
+              (≡.sym (cast-involutive (≡.sym (+-assoc X 0 Y)) _ [x0]y))
+              (≡.cong (cast _) cast[x0]y≡x↑ˡY)
+          rewrite ≡.trans
+              (≡.cong (cast (≡.sym (+-assoc X 0 Y))) (≡.sym (↑ˡ-+ x 0 Y)))
+              (cast-involutive _ (+-assoc X 0 Y) (x ↑ˡ 0 ↑ˡ Y))
+            = ↑ˡ-REL aux
+        where
+          aux : ρ⇒ (x ↑ˡ 0) x
+          aux with splitAt X (x ↑ˡ 0) in eq
+          ... | inj₁ x′ = ↑ˡ-injective 0 x′ x (splitAt⁻¹-↑ˡ eq)
+  ... | inj₂ (y , y , ≡.refl , cast[x0]y≡X↑ʳy , ≡.refl)
+          rewrite ≡.trans
+              (≡.sym (cast-involutive (≡.sym (+-assoc X 0 Y)) _ [x0]y))
+              (≡.cong (cast _) cast[x0]y≡X↑ʳy)
+          rewrite ≡.trans
+              (≡.cong (cast (≡.sym (+-assoc X 0 Y))) (≡.sym (+-↑ʳ X 0 y)))
+              (cast-involutive (≡.sym (+-assoc X 0 Y)) _ (X + 0 ↑ʳ y))
+            = ↑ʳ-REL ≡.refl
+
+  triʳ : ρ⇒ +₁ _≡_ {A = Fin Y} ⇒ α⇒ {X} ; (_≡_ {A = Fin X} +₁ _≡_)
+  triʳ {[x0]y} {x[0y]} e-[x0]y-x[0y] with +₁-⊎ e-[x0]y-x[0y]
+  ... | inj₂ (y , y , ≡.refl , ≡.refl , ≡.refl) = x[0y] , +-↑ʳ X 0 y , ↑ʳ-REL ≡.refl
+  ... | inj₁ (x0 , x , x′≡x , ≡.refl , ≡.refl) with splitAt X x0 in eq
+  ... | inj₁ x′ rewrite ≡.sym (splitAt⁻¹-↑ˡ eq) rewrite x′≡x = x[0y] , ↑ˡ-+ x 0 Y , ↑ˡ-REL ≡.refl
+
+  triangle : α⇒ {X} ; (_≡_ {A = Fin X} +₁ _≡_) ⇔ ρ⇒ +₁ _≡_ {A = Fin Y}
+  triangle = triˡ , triʳ
+
+module _ (X Y Z W : ℕ) where
+
+  pentˡ
+      : ((α⇒ {X} {Y} {Z} +₁ _≡_ {A = Fin W}) ; α⇒ {X}) ; (_≡_ {A = Fin X} +₁ (α⇒ {Y}))
+      ⇒ α⇒ {X + Y} ; α⇒ {X}
+  pentˡ {xyzw} {x[y[zw]]} (x[[yz]w] , ([x[yz]]w , xyzw~[x[yz]]w , ≡.refl) , [x[yz]]w~x[y[zw]])
+    with +₁-⊎ xyzw~[x[yz]]w | +₁-⊎ [x[yz]]w~x[y[zw]]
+  ... | inj₁ ([xy]z , x[y]z , ≡.refl , ≡.refl , ≡.refl)
+      | inj₁ (x , x′ , ≡.refl , [xy]z↑ˡW≡x↑ˡY+Z+W , ≡.refl)
+            = cast (≡.sym (+-assoc X Y (Z + W))) x[y[zw]]
+            , eq
+            , cast-involutive (+-assoc X Y (Z + W)) (≡.sym (+-assoc X Y (Z + W))) x[y[zw]]
+          where
+            lemma : cast  _ [xy]z ↑ˡ W ≡ cast _ (x ↑ˡ Y + Z + W)
+            lemma = ≡.trans
+                (≡.sym (cast-involutive (≡.sym (+-assoc X (Y + Z) W)) (+-assoc X (Y + Z) W) (cast {X + Y + Z} {X + (Y + Z)} _ [xy]z ↑ˡ W)))
+                (≡.cong (cast (≡.sym (+-assoc X (Y + Z) W))) [xy]z↑ˡW≡x↑ˡY+Z+W)
+            open ≡-Reasoning
+            eq : cast {X + Y + Z + W} {X + Y + (Z + W)} _ ([xy]z ↑ˡ W)
+                ≡ cast {X + (Y + (Z + W))} {X + Y + (Z + W)} _ x[y[zw]]
+            eq = begin
+              cast (+-assoc (X + Y) Z W) ([xy]z ↑ˡ W)
+                  ≡⟨ cast-trans _ (≡.trans (≡.cong (_+ W) (≡.sym (+-assoc X Y Z))) (+-assoc (X + Y) Z W)) ([xy]z ↑ˡ W) ⟨
+              cast (≡.trans (≡.cong (_+ W) (≡.sym (+-assoc X Y Z))) (+-assoc (X + Y) Z W)) (cast _ ([xy]z ↑ˡ W))
+                  ≡⟨ ≡.cong (cast _) (cast-↑ˡ (+-assoc X Y Z) [xy]z W) ⟨
+              cast _ (cast _ [xy]z ↑ˡ W)
+                  ≡⟨ ≡.cong (cast _) lemma ⟩
+              cast (≡.trans (≡.cong (_+ W) (≡.sym (+-assoc X Y Z))) (+-assoc (X + Y) Z W))
+              (cast (≡.sym (+-assoc X (Y + Z) W)) (x ↑ˡ Y + Z + W))
+                  ≡⟨ cast-trans (≡.sym (+-assoc X (Y + Z) W)) (≡.trans (≡.cong (_+ W) (≡.sym (+-assoc X Y Z))) (+-assoc (X + Y) Z W)) (x ↑ˡ Y + Z + W) ⟩
+              cast _ (x ↑ˡ Y + Z + W)
+                  ≡⟨ ≡.cong (cast _) (↑ˡ-assoc x Y Z W) ⟩
+              cast _ (cast (≡.cong (X +_) (≡.sym (+-assoc Y Z W))) (x ↑ˡ Y + (Z + W)))
+                  ≡⟨ cast-trans (≡.cong (X +_) (≡.sym (+-assoc Y Z W))) _ (x ↑ˡ Y + (Z + W)) ⟩
+              cast _ (x ↑ˡ (Y + (Z + W)))                   ∎
+  ... | inj₁ ([xy]z , x[yz] , ≡.refl , ≡.refl , ≡.refl) | inj₂ ([yz]w , y[zw] , ≡.refl , [xy]z↑ˡW≡X↑ʳ[yz]w , ≡.refl)
+            = cast (≡.sym (+-assoc X Y (Z + W))) (x[y[zw]])
+            , eq
+            , cast-involutive (+-assoc X Y (Z + W)) _ (X ↑ʳ cast _ [yz]w)
+          where
+            open ≡-Reasoning
+            lemma₁ : X + (Y + Z + W) ≡ X + Y + Z + W
+            lemma₁ = begin
+                X + (Y + Z + W) ≡⟨ +-assoc X (Y + Z) W ⟨
+                X + (Y + Z) + W ≡⟨ ≡.cong (_+ W) (+-assoc X Y Z) ⟨
+                X + Y + Z + W   ∎
+            lemma₂ : cast {X + Y + Z + W} {X + (Y + Z) + W} _ ([xy]z ↑ˡ W) ≡ cast _ (X ↑ʳ [yz]w)
+            lemma₂ = begin
+                cast _ ([xy]z ↑ˡ W)                                     ≡⟨ cast-↑ˡ (+-assoc X Y Z) [xy]z W ⟨
+                cast _ [xy]z ↑ˡ W                                       ≡⟨ cast-involutive (≡.sym (+-assoc X (Y + Z) W)) _ (cast _ [xy]z ↑ˡ W) ⟨
+                cast _ (cast (+-assoc X (Y + Z) W) (cast _ [xy]z ↑ˡ W)) ≡⟨ ≡.cong (cast _) [xy]z↑ˡW≡X↑ʳ[yz]w ⟩
+                cast _ (X ↑ʳ [yz]w)                                     ∎
+            lemma₃ : [xy]z ↑ˡ W ≡ cast _ (X ↑ʳ [yz]w)
+            lemma₃ = begin
+                [xy]z ↑ˡ W                                                  ≡⟨ cast-involutive (≡.sym (≡.cong (_+ W) (+-assoc X Y Z))) _ ([xy]z ↑ˡ W) ⟨
+                cast _ (cast (≡.cong (_+ W) (+-assoc X Y Z)) ([xy]z ↑ˡ W))  ≡⟨ ≡.cong (cast _) lemma₂ ⟩
+                cast (≡.sym (≡.cong (_+ W) (+-assoc X Y Z))) (cast _ (X ↑ʳ [yz]w))  ≡⟨ cast-trans _ (≡.sym (≡.cong (_+ W) (+-assoc X Y Z))) (X ↑ʳ [yz]w) ⟩
+                cast _ (X ↑ʳ [yz]w) ∎
+            eq : cast (+-assoc (X + Y) Z W) ([xy]z ↑ˡ W) ≡ cast _ (X ↑ʳ cast _ [yz]w)
+            eq = begin
+                cast _ ([xy]z ↑ˡ W)                                       ≡⟨ ≡.cong (cast _) lemma₃ ⟩
+                cast (+-assoc (X + Y) Z W) (cast _ (X ↑ʳ [yz]w))          ≡⟨ cast-trans lemma₁ (+-assoc (X + Y) Z W) (X ↑ʳ [yz]w) ⟩
+                cast _ (X ↑ʳ [yz]w)                                       ≡⟨ cast-trans _ (≡.sym (+-assoc X Y (Z + W))) (X ↑ʳ [yz]w) ⟨
+                cast (≡.sym (+-assoc X Y (Z + W))) (cast _ (X ↑ʳ [yz]w))  ≡⟨ ≡.cong (cast _) (cast-↑ʳ (+-assoc Y Z W) X [yz]w) ⟨
+                cast _ (X ↑ʳ cast _ [yz]w)                                ∎
+  ... | inj₂ (w , w , ≡.refl , ≡.refl , ≡.refl) | inj₁ (x , x , ≡.refl , X+[Y+Z]↑ʳw≡x↑ˡY+Z+W , ≡.refl)
+            = cast (≡.sym (+-assoc X Y (Z + W))) x[y[zw]]
+            , eq
+            , cast-involutive (+-assoc X Y (Z + W)) _ (x ↑ˡ Y + (Z + W))
+          where
+            open ≡-Reasoning
+            lemma₁ : X + (Y + (Z + W)) ≡ X + (Y + Z + W)
+            lemma₁ = ≡.cong (X +_) (≡.sym (+-assoc Y Z W))
+            lemma₂ : X + (Y + Z + W) ≡ X + Y + (Z + W)
+            lemma₂ = ≡.trans (≡.cong (X +_) (+-assoc Y Z W)) (≡.sym (+-assoc X Y (Z + W)))
+            lemma₃ : X + (Y + Z) + W ≡ X + Y + Z + W
+            lemma₃ = ≡.cong (_+ W) (≡.sym (+-assoc X Y Z))
+            eq : cast _ (X + Y + Z ↑ʳ w) ≡ cast (≡.sym (+-assoc X Y (Z + W))) (x ↑ˡ Y + (Z + W))
+            eq = begin
+                cast _ (X + Y + Z ↑ʳ w)                                 ≡⟨ ≡.cong (cast _) (assoc-↑ʳ X Y Z w) ⟩
+                cast _ (cast lemma₃ (X + (Y + Z) ↑ʳ w))                 ≡⟨ cast-trans lemma₃ (+-assoc (X + Y) Z W) (X + (Y + Z) ↑ʳ w) ⟩
+                cast _ (X + (Y + Z) ↑ʳ w)                               ≡⟨ cast-trans (+-assoc X (Y + Z) W) _ (X + (Y + Z) ↑ʳ w) ⟨
+                cast _ (cast (+-assoc X (Y + Z) W) (X + (Y + Z) ↑ʳ w))  ≡⟨ ≡.cong (cast _) X+[Y+Z]↑ʳw≡x↑ˡY+Z+W ⟩
+                cast _ (x ↑ˡ Y + Z + W)                                 ≡⟨ ≡.cong (cast _) (↑ˡ-assoc x Y Z W) ⟩
+                cast lemma₂ (cast lemma₁ (x ↑ˡ Y + (Z + W)))            ≡⟨ cast-trans lemma₁ lemma₂ (x ↑ˡ Y + (Z + W)) ⟩
+                cast (≡.sym (+-assoc X Y (Z + W))) (x ↑ˡ Y + (Z + W))   ∎
+  ... | inj₂ (w , w , ≡.refl , ≡.refl , ≡.refl) | inj₂ ([yz]w , y[zw] , ≡.refl , X+[Y+Z]↑ʳw≡X↑ʳ[yz]w , ≡.refl)
+            = cast (≡.sym (+-assoc X Y (Z + W))) x[y[zw]]
+            , eq
+            , cast-involutive {X + Y + (Z + W)} {X + (Y + (Z + W))} (+-assoc X Y (Z + W)) _ (X ↑ʳ cast _ [yz]w)
+          where
+            open ≡-Reasoning
+            lemma : X + (Y + Z + W) ≡ X + Y + (Z + W)
+            lemma = ≡.trans (≡.cong (X +_) (+-assoc Y Z W)) (≡.sym (+-assoc X Y (Z + W)))
+            eq : cast (+-assoc (X + Y) Z W) (X + Y + Z ↑ʳ w) ≡ cast (≡.sym (+-assoc X Y (Z + W))) (X ↑ʳ cast (+-assoc Y Z W) [yz]w)
+            eq = begin
+                cast _ (X + Y + Z ↑ʳ w)                                     ≡⟨ ≡.cong (cast _) (assoc-↑ʳ X Y Z w) ⟩
+                cast (+-assoc (X + Y) Z W) (cast _ (X + (Y + Z) ↑ʳ w))      ≡⟨ cast-trans _ (+-assoc (X + Y) Z W) (X + (Y + Z) ↑ʳ w) ⟩
+                cast _ (X + (Y + Z) ↑ʳ w)                                   ≡⟨ cast-trans (+-assoc X (Y + Z) W) _ (X + (Y + Z) ↑ʳ w) ⟨
+                cast lemma (cast _ (X + (Y + Z) ↑ʳ w))                      ≡⟨ ≡.cong (cast _) X+[Y+Z]↑ʳw≡X↑ʳ[yz]w ⟩
+                cast _ (X ↑ʳ [yz]w)                                         ≡⟨ cast-trans (≡.cong (X +_) (+-assoc Y Z W)) _ (X ↑ʳ [yz]w) ⟨
+                cast _ (cast (≡.cong (X +_) (+-assoc Y Z W)) (X ↑ʳ [yz]w))  ≡⟨ ≡.cong (cast _) (cast-↑ʳ (+-assoc Y Z W) X [yz]w) ⟨
+                cast _ (X ↑ʳ cast _ [yz]w)                                  ∎
+
+  pentʳ
+      : α⇒ {X + Y} ; α⇒ {X}
+      ⇒ ((α⇒ {X} {Y} {Z} +₁ _≡_ {A = Fin W}) ; α⇒ {X}) ; (_≡_ {A = Fin X} +₁ (α⇒ {Y}))
+  pentʳ {xyzw} {x[y[zw]]} (xy[zw] , ≡.refl , ≡.refl)
+      = cast (≡.cong (X +_) (≡.sym (+-assoc Y Z W))) x[y[zw]]
+      , (cast (≡.cong (_+ W) (+-assoc X Y Z)) xyzw , eq₁ , eq₂)
+      , eq₃
+    where
+      eq₁ : ((λ [xy]z x[yz] → cast _ [xy]z ≡ x[yz]) +₁ _≡_) xyzw (cast {X + Y + Z + W} {X + (Y + Z) + W} (≡.cong (_+ W) (+-assoc X Y Z)) xyzw)
+      eq₁ with splitAt (X + Y + Z) xyzw in eq
+      ... | inj₁ xyz rewrite ≡.sym (splitAt⁻¹-↑ˡ eq) = lemma
+              where
+                lemma : ((λ [xy]z x[yz] → cast (+-assoc X Y Z) [xy]z ≡ x[yz]) +₁ _≡_) (xyz ↑ˡ W) (cast (≡.cong (_+ W) (+-assoc X Y Z)) (xyz ↑ˡ W))
+                lemma rewrite ≡.sym (cast-↑ˡ (+-assoc X Y Z) xyz W) = ↑ˡ-REL ≡.refl
+      ... | inj₂ w rewrite ≡.sym (splitAt⁻¹-↑ʳ eq) = lemma
+              where
+                open ≡-Reasoning
+                lemma′ : X + Y + Z + W ≡ X + (Y + Z) + W
+                lemma′ = ≡.cong (_+ W) (+-assoc X Y Z)
+                rw : cast lemma′ (X + Y + Z ↑ʳ w) ≡ X + (Y + Z) ↑ʳ w
+                rw = begin
+                    cast _ (X + Y + Z ↑ʳ w)                                           ≡⟨ ≡.cong (cast _) (assoc-↑ʳ X Y Z w) ⟩
+                    cast (≡.cong (_+ W) (+-assoc X Y Z)) (cast _ (X + (Y + Z) ↑ʳ w))  ≡⟨ cast-involutive (≡.cong (_+ W) (+-assoc X Y Z)) _ (X + (Y + Z) ↑ʳ w) ⟩
+                    X + (Y + Z) ↑ʳ w                                                  ∎
+                lemma : ((λ [xy]z → _≡_ (cast (+-assoc X Y Z) [xy]z)) +₁ _≡_) (X + Y + Z ↑ʳ w) (cast lemma′ (X + Y + Z ↑ʳ w))
+                lemma rewrite rw = ↑ʳ-REL ≡.refl
+      open ≡-Reasoning
+      eq₂ : cast (+-assoc X (Y + Z) W) (cast _ xyzw) ≡ cast (≡.cong (X +_) (≡.sym (+-assoc Y Z W))) (cast (+-assoc X Y (Z + W)) (cast (+-assoc (X + Y) Z W) xyzw))
+      eq₂ = begin
+          cast _ (cast (≡.cong (_+ W) (+-assoc X Y Z)) xyzw)  ≡⟨ cast-trans (≡.cong (_+ W) (+-assoc X Y Z)) (+-assoc X (Y + Z) W) xyzw ⟩
+          cast _ xyzw                   ≡⟨ cast-trans _ (≡.trans (+-assoc X Y (Z + W)) (≡.cong (X +_) (≡.sym (+-assoc Y Z W)))) xyzw ⟨
+          cast (≡.trans (+-assoc X Y (Z + W)) (≡.cong (X +_) (≡.sym (+-assoc Y Z W)))) (cast (+-assoc (X + Y) Z W) xyzw)  ≡⟨ cast-trans (+-assoc X Y (Z + W)) (≡.cong (X +_) (≡.sym (+-assoc Y Z W))) (cast (+-assoc (X + Y) Z W) xyzw) ⟨
+          cast (≡.cong (X +_) (≡.sym (+-assoc Y Z W))) (cast (+-assoc X Y (Z + W)) (cast _ xyzw)) ∎
+      arg₁ : Fin (X + (Y + Z + W))
+      arg₁ = cast (≡.cong (X +_) (≡.sym (+-assoc Y Z W))) (cast (+-assoc X Y (Z + W)) (cast (+-assoc (X + Y) Z W) xyzw))
+      arg₂ : Fin (X + (Y + (Z + W)))
+      arg₂ = cast (+-assoc X Y (Z + W)) (cast (+-assoc (X + Y) Z W) xyzw)
+      eq₃ : (_≡_ {A = Fin X} +₁ (λ [yz]w y[zw] → cast (+-assoc Y Z W) [yz]w ≡ y[zw])) arg₁ arg₂
+      eq₃ with splitAt X x[y[zw]] in eq
+      ... | inj₁ x rewrite ≡.sym (splitAt⁻¹-↑ˡ eq) rewrite ≡.sym (↑ˡ-assoc x Y Z W) = ↑ˡ-REL ≡.refl
+      ... | inj₂ yzw rewrite ≡.sym (splitAt⁻¹-↑ʳ eq) rewrite ≡.sym (cast-↑ʳ (≡.sym (+-assoc Y Z W)) X yzw) = ↑ʳ-REL (cast-involutive (+-assoc Y Z W) _ yzw)
+
+  pentagon
+      : ((α⇒ {X} {Y} {Z} +₁ _≡_ {A = Fin W}) ; α⇒ {X}) ; (_≡_ {A = Fin X} +₁ (α⇒ {Y}))
+      ⇔ α⇒ {X + Y} ; α⇒ {X}
+  pentagon = pentˡ , pentʳ
+
+FinRel-Monoidal : Monoidal FinRel
+FinRel-Monoidal = record
+    { ⊗ = ⊗
+    ; unit = 0
+    ; unitorˡ = unitorˡ
+    ; unitorʳ = unitorʳ
+    ; associator = λ {X Y Z} → associator {X} {Y} {Z}
+    ; unitorˡ-commute-from = λ {X} {Y} {R} → unitorˡ-commute-to X Y R
+    ; unitorˡ-commute-to = λ {X} {Y} {R} → unitorˡ-commute-from X Y R
+    ; unitorʳ-commute-from = λ {X} {Y} {R} → unitorʳ-commute-from X Y R
+    ; unitorʳ-commute-to = λ {X} {Y} {R} → unitorʳ-commute-to X Y R
+    ; assoc-commute-from = λ {X Y R X′ Y′ S X″ Y″ T} → assoc-commute-from X Y X′ Y′ X″ Y″ R S T
+    ; assoc-commute-to = λ {X Y R X′ Y′ S X″ Y″ T} → assoc-commute-to X Y X′ Y′ X″ Y″ R S T
+    ; triangle = λ {X Y} → triangle X Y
+    ; pentagon = λ {X Y Z W} → pentagon X Y Z W
+    }