diff options
Diffstat (limited to 'Data/WiringDiagram/FinRel.agda')
| -rw-r--r-- | Data/WiringDiagram/FinRel.agda | 657 |
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 + } |