# Path algebra

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Raymond Baker, Elisabeth Bonnevier and maybemabeline.

Created on 2022-03-10.

module foundation.path-algebra where

Imports
open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.binary-embeddings
open import foundation.binary-equivalences
open import foundation.commuting-squares-of-identifications
open import foundation.identity-types
open import foundation.universe-levels

open import foundation-core.constant-maps
open import foundation-core.function-types
open import foundation-core.homotopies


## Idea

As we iterate identity type (i.e., consider the type of identifications between two identifications), the identity types gain further structure.

Identity types of identity types are types of the form p ＝ q, where p q : x ＝ y and x y : A. Using the homotopy interpretation of type theory, elements of such a type are often called 2-paths and a twice iterated identity type is often called a type of 2-paths.

Since 2-paths are just identifications, they have the usual operations and coherences on paths/identifications. In the context of 2-paths, this famliar concatination operation is called vertical concatination (see vertical-concat-Id² below). However, 2-paths have novel operations and coherences derived from the operations and coherences of the boundary 1-paths (these are p and q in the example above). Since concatination of 1-paths is a functor, it has an induced action on paths. We call this operation horizontal concatination (see horizontal-concat-Id² below). It comes with the standard coherences of an action on paths function, as well as coherences induced by coherences on the boundary 1-paths.

## Properties

### The unit laws of concatenation induce homotopies

module _
{l : Level} {A : UU l} {a0 a1 : A}
where

htpy-left-unit : (λ (p : a0 ＝ a1) → refl {x = a0} ∙ p) ~ id
htpy-left-unit p = left-unit

htpy-right-unit : (λ (p : a0 ＝ a1) → p ∙ refl) ~ id
htpy-right-unit p = right-unit


### Squares

horizontal-concat-square :
{l : Level} {A : UU l} {a b c d e f : A}
(p-lleft : a ＝ b) (p-lbottom : b ＝ d) (p-rbottom : d ＝ f)
(p-middle : c ＝ d) (p-ltop : a ＝ c) (p-rtop : c ＝ e) (p-rright : e ＝ f)
(s-left : coherence-square-identifications p-lleft p-lbottom p-ltop p-middle)
(s-right :
coherence-square-identifications p-middle p-rbottom p-rtop p-rright) →
coherence-square-identifications
p-lleft (p-lbottom ∙ p-rbottom) (p-ltop ∙ p-rtop) p-rright
horizontal-concat-square {a = a} {f = f}
p-lleft p-lbottom p-rbottom p-middle p-ltop p-rtop p-rright s-left s-right =
( inv (assoc p-lleft p-lbottom p-rbottom)) ∙
( ( ap (concat' a p-rbottom) s-left) ∙
( ( assoc p-ltop p-middle p-rbottom) ∙
( ( ap (concat p-ltop f) s-right) ∙
( inv (assoc p-ltop p-rtop p-rright)))))

horizontal-unit-square :
{l : Level} {A : UU l} {a b : A} (p : a ＝ b) →
coherence-square-identifications p refl refl p
horizontal-unit-square p = right-unit

left-unit-law-horizontal-concat-square :
{l : Level} {A : UU l} {a b c d : A}
(p-left : a ＝ b) (p-bottom : b ＝ d) (p-top : a ＝ c) (p-right : c ＝ d) →
(s : coherence-square-identifications p-left p-bottom p-top p-right) →
( horizontal-concat-square
p-left refl p-bottom p-left refl p-top p-right
( horizontal-unit-square p-left)
( s)) ＝
( s)
left-unit-law-horizontal-concat-square refl p-bottom p-top p-right s =
right-unit ∙ ap-id s

vertical-concat-square :
{l : Level} {A : UU l} {a b c d e f : A}
(p-tleft : a ＝ b) (p-bleft : b ＝ c) (p-bbottom : c ＝ f)
(p-middle : b ＝ e) (p-ttop : a ＝ d) (p-tright : d ＝ e) (p-bright : e ＝ f)
(s-top : coherence-square-identifications p-tleft p-middle p-ttop p-tright)
(s-bottom :
coherence-square-identifications p-bleft p-bbottom p-middle p-bright) →
coherence-square-identifications
(p-tleft ∙ p-bleft) p-bbottom p-ttop (p-tright ∙ p-bright)
vertical-concat-square {a = a} {f = f}
p-tleft p-bleft p-bbottom p-middle p-ttop p-tright p-bright s-top s-bottom =
( assoc p-tleft p-bleft p-bbottom) ∙
( ( ap (concat p-tleft f) s-bottom) ∙
( ( inv (assoc p-tleft p-middle p-bright)) ∙
( ( ap (concat' a p-bright) s-top) ∙
( assoc p-ttop p-tright p-bright))))


### Unit laws for assoc

We give two treatments of the unit laws for the associator. One for computing with the associator, and one for coherences between the unit laws.

#### Computing assoc at a reflexivity

module _
{l : Level} {A : UU l} {x y z : A}
where

left-unit-law-assoc :
(p : x ＝ y) (q : y ＝ z) →
assoc refl p q ＝ refl
left-unit-law-assoc p q = refl

middle-unit-law-assoc :
(p : x ＝ y) (q : y ＝ z) →
assoc p refl q ＝ ap (_∙ q) (right-unit)
middle-unit-law-assoc refl q = refl

right-unit-law-assoc :
(p : x ＝ y) (q : y ＝ z) →
assoc p q refl ＝ (right-unit ∙ ap (p ∙_) (inv right-unit))
right-unit-law-assoc refl refl = refl


#### Unit laws for assoc and their coherence

We use a binary naming scheme for the (higher) unit laws of the associator. For each 3-digit binary number except when all digits are 1, there is a corresponding unit law. A 0 reflects that the unit of the operator is present in the corresponding position. More generally, there is for each n-digit binary number (except all 1s) a unit law for the n-ary coherence operator.

module _
{l : Level} {A : UU l} {x y z : A}
where

unit-law-assoc-011 :
(p : x ＝ y) (q : y ＝ z) →
assoc refl p q ＝ refl
unit-law-assoc-011 p q = refl

unit-law-assoc-101 :
(p : x ＝ y) (q : y ＝ z) →
assoc p refl q ＝ ap (_∙ q) (right-unit)
unit-law-assoc-101 refl q = refl

unit-law-assoc-101' :
(p : x ＝ y) (q : y ＝ z) →
inv (assoc p refl q) ＝ ap (_∙ q) (inv right-unit)
unit-law-assoc-101' refl q = refl

unit-law-assoc-110 :
(p : x ＝ y) (q : y ＝ z) →
(assoc p q refl ∙ ap (p ∙_) right-unit) ＝ right-unit
unit-law-assoc-110 refl refl = refl

unit-law-assoc-110' :
(p : x ＝ y) (q : y ＝ z) →
(inv right-unit ∙ assoc p q refl) ＝ ap (p ∙_) (inv right-unit)
unit-law-assoc-110' refl refl = refl


### Unit laws for ap-concat-eq

ap-concat-eq-inv-right-unit :
{l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) {x y : A}
(p : x ＝ y) → inv right-unit ＝ ap-concat-eq f p refl p (inv right-unit)
ap-concat-eq-inv-right-unit f refl = refl


### Iterated inverse laws

module _
{l : Level} {A : UU l}
where

is-section-left-concat-inv :
{x y z : A} (p : x ＝ y) (q : y ＝ z) → (inv p ∙ (p ∙ q)) ＝ q
is-section-left-concat-inv refl q = refl

is-retraction-left-concat-inv :
{x y z : A} (p : x ＝ y) (q : x ＝ z) → (p ∙ (inv p ∙ q)) ＝ q
is-retraction-left-concat-inv refl q = refl

is-section-right-concat-inv :
{x y z : A} (p : x ＝ y) (q : z ＝ y) → ((p ∙ inv q) ∙ q) ＝ p
is-section-right-concat-inv refl refl = refl

is-retraction-right-concat-inv :
{x y z : A} (p : x ＝ y) (q : y ＝ z) → ((p ∙ q) ∙ inv q) ＝ p
is-retraction-right-concat-inv refl refl = refl


## Properties of 2-paths

### Definition of vertical and horizontal concatenation in identity types of identity types (a type of 2-paths)

vertical-concat-Id² :
{l : Level} {A : UU l} {x y : A} {p q r : x ＝ y} → p ＝ q → q ＝ r → p ＝ r
vertical-concat-Id² α β = α ∙ β

horizontal-concat-Id² :
{l : Level} {A : UU l} {x y z : A} {p q : x ＝ y} {u v : y ＝ z} →
p ＝ q → u ＝ v → (p ∙ u) ＝ (q ∙ v)
horizontal-concat-Id² α β = ap-binary (λ s t → s ∙ t) α β


### Definition of identification whiskering

module _
{l : Level} {A : UU l} {x y z : A}
where

identification-left-whisk :
(p : x ＝ y) {q q' : y ＝ z} → q ＝ q' → (p ∙ q) ＝ (p ∙ q')
identification-left-whisk p β = ap (p ∙_) β

identification-right-whisk :
{p p' : x ＝ y} → p ＝ p' → (q : y ＝ z) → (p ∙ q) ＝ (p' ∙ q)
identification-right-whisk α q = ap (_∙ q) α

htpy-identification-left-whisk :
{q q' : y ＝ z} → q ＝ q' → (_∙ q) ~ (_∙ q')
htpy-identification-left-whisk β p = identification-left-whisk p β


### Both horizontal and vertical concatenation of 2-paths are binary equivalences

is-binary-equiv-vertical-concat-Id² :
{l : Level} {A : UU l} {x y : A} {p q r : x ＝ y} →
is-binary-equiv (vertical-concat-Id² {l} {A} {x} {y} {p} {q} {r})
is-binary-equiv-vertical-concat-Id² = is-binary-equiv-concat

is-binary-equiv-horizontal-concat-Id² :
{l : Level} {A : UU l} {x y z : A} {p q : x ＝ y} {u v : y ＝ z} →
is-binary-equiv (horizontal-concat-Id² {l} {A} {x} {y} {z} {p} {q} {u} {v})
is-binary-equiv-horizontal-concat-Id² =
is-binary-emb-is-binary-equiv is-binary-equiv-concat


### Unit laws for horizontal and vertical concatenation of 2-paths

left-unit-law-vertical-concat-Id² :
{l : Level} {A : UU l} {x y : A} {p q : x ＝ y} {β : p ＝ q} →
vertical-concat-Id² refl β ＝ β
left-unit-law-vertical-concat-Id² = left-unit

right-unit-law-vertical-concat-Id² :
{l : Level} {A : UU l} {x y : A} {p q : x ＝ y} {α : p ＝ q} →
vertical-concat-Id² α refl ＝ α
right-unit-law-vertical-concat-Id² = right-unit

left-unit-law-horizontal-concat-Id² :
{l : Level} {A : UU l} {x y z : A} {p : x ＝ y} {u v : y ＝ z} (γ : u ＝ v) →
horizontal-concat-Id² (refl {x = p}) γ ＝
identification-left-whisk p γ
left-unit-law-horizontal-concat-Id² γ = left-unit-ap-binary (λ s t → s ∙ t) γ

right-unit-law-horizontal-concat-Id² :
{l : Level} {A : UU l} {x y z : A} {p q : x ＝ y} (α : p ＝ q) {u : y ＝ z} →
horizontal-concat-Id² α (refl {x = u}) ＝
identification-right-whisk α u
right-unit-law-horizontal-concat-Id² α = right-unit-ap-binary (λ s t → s ∙ t) α


Horizontal concatination satisfies an additional "2-dimensional" unit law (on both the left and right) induced by the unit laws on the boundary 1-paths.

module _
{l : Level} {A : UU l} {x y : A} {p p' : x ＝ y} (α : p ＝ p')
where

nat-sq-right-unit-Id² :
coherence-square-identifications
( right-unit)
( α)
( horizontal-concat-Id² α refl)
( right-unit)
nat-sq-right-unit-Id² =
( ( horizontal-concat-Id² refl (inv (ap-id α))) ∙
( nat-htpy htpy-right-unit α)) ∙
( horizontal-concat-Id² (inv (right-unit-law-horizontal-concat-Id² α)) refl)

nat-sq-left-unit-Id² :
coherence-square-identifications
( left-unit)
( α)
( horizontal-concat-Id² (refl {x = refl}) α)
( left-unit)
nat-sq-left-unit-Id² =
( ( (inv (ap-id α) ∙ (nat-htpy htpy-left-unit α)) ∙ right-unit) ∙
( inv (left-unit-law-horizontal-concat-Id² α))) ∙ inv right-unit


### Unit laws for whiskering

module _
{l : Level} {A : UU l} {x y : A}
where

left-unit-law-identification-left-whisk :
{p p' : x ＝ y} (α : p ＝ p') →
identification-left-whisk refl α ＝ α
left-unit-law-identification-left-whisk refl = refl

right-unit-law-identification-right-whisk :
{p p' : x ＝ y} (α : p ＝ p') →
identification-right-whisk α refl ＝
right-unit ∙ α ∙ inv right-unit
right-unit-law-identification-right-whisk {p = refl} refl = refl


### The whiskering operations allow us to commute higher identifications

module _
{l : Level} {A : UU l} {x y z : A}
where

path-swap-nat-identification-left-whisk :
{q q' : y ＝ z} (β : q ＝ q') {p p' : x ＝ y} (α : p ＝ p') →
coherence-square-identifications
( identification-left-whisk p β)
( identification-right-whisk α q')
( identification-right-whisk α q)
( identification-left-whisk p' β)
path-swap-nat-identification-left-whisk β =
nat-htpy (htpy-identification-left-whisk β)


### Definition of horizontal inverse

2-paths have an induced inverse operation from the operation on boundary 1-paths

module _
{l : Level} {A : UU l} {x y : A} {p p' : x ＝ y}
where

horizontal-inv-Id² : p ＝ p' → (inv p) ＝ (inv p')
horizontal-inv-Id² α = ap inv α


This operation satisfies a left and right idenity induced by the inverse laws on 1-paths

module _
{l : Level} {A : UU l} {x y : A} {p p' : x ＝ y} (α : p ＝ p')
where

nat-sq-right-inv-Id² :
coherence-square-identifications
( right-inv p)
( refl)
( horizontal-concat-Id² α (horizontal-inv-Id² α))
( right-inv p')
nat-sq-right-inv-Id² =
( ( ( horizontal-concat-Id² refl (inv (ap-const refl α))) ∙
( nat-htpy right-inv α)) ∙
( horizontal-concat-Id²
( ap-binary-comp-diagonal (_∙_) id inv α)
( refl))) ∙
( ap
( λ t → horizontal-concat-Id² t (horizontal-inv-Id² α) ∙ right-inv p')
( ap-id α))

nat-sq-left-inv-Id² :
coherence-square-identifications
( left-inv p)
( refl)
( horizontal-concat-Id² (horizontal-inv-Id² α) α)
( left-inv p')
nat-sq-left-inv-Id² =
( ( ( horizontal-concat-Id² refl (inv (ap-const refl α))) ∙
( nat-htpy left-inv α)) ∙
( horizontal-concat-Id²
( ap-binary-comp-diagonal _∙_ inv id α)
( refl))) ∙
( ap
( λ t → (horizontal-concat-Id² (horizontal-inv-Id² α) t) ∙ left-inv p')
( ap-id α))


### Interchange laws for 2-paths

interchange-Id² :
{l : Level} {A : UU l} {x y z : A} {p q r : x ＝ y} {u v w : y ＝ z}
(α : p ＝ q) (β : q ＝ r) (γ : u ＝ v) (δ : v ＝ w) →
( horizontal-concat-Id²
( vertical-concat-Id² α β)
( vertical-concat-Id² γ δ)) ＝
( vertical-concat-Id²
( horizontal-concat-Id² α γ)
( horizontal-concat-Id² β δ))
interchange-Id² refl refl refl refl = refl

unit-law-α-interchange-Id² :
{l : Level} {A : UU l} {x y z : A} {p q : x ＝ y} (α : p ＝ q) (u : y ＝ z) →
( ( interchange-Id² α refl (refl {x = u}) refl) ∙
( right-unit ∙ right-unit-law-horizontal-concat-Id² α)) ＝
( ( right-unit-law-horizontal-concat-Id² (α ∙ refl)) ∙
( ap (ap (concat' x u)) right-unit))
unit-law-α-interchange-Id² refl u = refl

unit-law-β-interchange-Id² :
{l : Level} {A : UU l} {x y z : A} {p q : x ＝ y} (β : p ＝ q) (u : y ＝ z) →
interchange-Id² refl β (refl {x = u}) refl ＝ refl
unit-law-β-interchange-Id² refl u = refl

unit-law-γ-interchange-Id² :
{l : Level} {A : UU l} {x y z : A} (p : x ＝ y) {u v : y ＝ z} (γ : u ＝ v) →
( ( interchange-Id² (refl {x = p}) refl γ refl) ∙
( right-unit ∙ left-unit-law-horizontal-concat-Id² γ)) ＝
( ( left-unit-law-horizontal-concat-Id² (γ ∙ refl)) ∙
( ap (ap (concat p z)) right-unit))
unit-law-γ-interchange-Id² p refl = refl

unit-law-δ-interchange-Id² :
{l : Level} {A : UU l} {x y z : A} (p : x ＝ y) {u v : y ＝ z} (δ : u ＝ v) →
interchange-Id² (refl {x = p}) refl refl δ ＝ refl
unit-law-δ-interchange-Id² p refl = refl


### Action on 2-paths of functors

Functions have an induced action on 2-paths

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {x y : A}
{p p' : x ＝ y} (f : A → B) (α : p ＝ p')
where

ap² : (ap f p) ＝ (ap f p')
ap² = (ap (ap f)) α


Since this is define in terms of ap, it comes with the standard coherences. It also has induced cohereces.

Inverse law.

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {x y : A}
{p p' : x ＝ y} (f : A → B) (α : p ＝ p')
where

nat-sq-ap-inv-Id² :
coherence-square-identifications
( ap-inv f p)
( horizontal-inv-Id² (ap² f α))
( ap² f (horizontal-inv-Id² α))
( ap-inv f p')
nat-sq-ap-inv-Id² =
(inv (horizontal-concat-Id² refl (ap-comp inv (ap f) α)) ∙
(nat-htpy (ap-inv f) α)) ∙
(horizontal-concat-Id² (ap-comp (ap f) inv α) refl)


Identity law and constant law.

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {x y : A}
{p p' : x ＝ y} (α : p ＝ p')
where

nat-sq-ap-id-Id² :
coherence-square-identifications (ap-id p) α (ap² id α) (ap-id p')
nat-sq-ap-id-Id² =
((horizontal-concat-Id² refl (inv (ap-id α))) ∙ (nat-htpy ap-id α))

nat-sq-ap-const-Id² :
(b : B) →
coherence-square-identifications
( ap-const b p)
( refl)
( ap² (const A B b) α)
( ap-const b p')
nat-sq-ap-const-Id² b =
( inv (horizontal-concat-Id² refl (ap-const refl α))) ∙
( nat-htpy (ap-const b) α)


Composition law

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
{x y : A} {p p' : x ＝ y} (g : B → C) (f : A → B) (α : p ＝ p')
where

nat-sq-ap-comp-Id² :
coherence-square-identifications
( ap-comp g f p)
( (ap² g ∘ ap² f) α)
( ap² (g ∘ f) α)
( ap-comp g f p')
nat-sq-ap-comp-Id² =
(horizontal-concat-Id² refl (inv (ap-comp (ap g) (ap f) α)) ∙
(nat-htpy (ap-comp g f) α))


## Properties of 3-paths

3-paths are identifications of 2-paths. In symbols, a type of 3-paths is a type of the form α ＝ β where α β : p ＝ q and p q : x ＝ y.

### Concatination in a type of 3-paths

Like with 2-paths, 3-paths have the standard operations on equalties, plus the operations induced by the operations on 1-paths. But 3-paths also have operations induced by those on 2-paths. Thus there are three ways to concatenate in triple identity types. We name the three concatenations of triple identity types x-, y-, and z-concatenation, after the standard names for the three axis in 3-dimensional space.

The x-concatenation operation corresponds the standard concatination of equalities.

x-concat-Id³ :
{l : Level} {A : UU l} {x y : A} {p q : x ＝ y} {α β γ : p ＝ q} →
α ＝ β → β ＝ γ → α ＝ γ
x-concat-Id³ σ τ = vertical-concat-Id² σ τ


The y-concatenation operation corresponds the operation induced by the concatination on 1-paths.

y-concat-Id³ :
{l : Level} {A : UU l} {x y : A} {p q r : x ＝ y} {α β : p ＝ q}
{γ δ : q ＝ r} → α ＝ β → γ ＝ δ → (α ∙ γ) ＝ (β ∙ δ)
y-concat-Id³ σ τ = horizontal-concat-Id² σ τ


The z-concatenation operation corresponds the concatination induced by the horizontal concatination on 2-paths.

z-concat-Id³ :
{l : Level} {A : UU l} {x y z : A} {p q : x ＝ y} {u v : y ＝ z}
{α β : p ＝ q} {γ δ : u ＝ v} →
α ＝ β → γ ＝ δ → horizontal-concat-Id² α γ ＝ horizontal-concat-Id² β δ
z-concat-Id³ σ τ = ap-binary (λ s t → horizontal-concat-Id² s t) σ τ


### Unit laws for the concatenation operations on 3-paths

left-unit-law-x-concat-Id³ :
{l : Level} {A : UU l} {x y : A} {p q : x ＝ y} {α β : p ＝ q} {σ : α ＝ β} →
x-concat-Id³ refl σ ＝ σ
left-unit-law-x-concat-Id³ = left-unit-law-vertical-concat-Id²

right-unit-law-x-concat-Id³ :
{l : Level} {A : UU l} {x y : A} {p q : x ＝ y} {α β : p ＝ q} {τ : α ＝ β} →
x-concat-Id³ τ refl ＝ τ
right-unit-law-x-concat-Id³ = right-unit-law-vertical-concat-Id²

left-unit-law-y-concat-Id³ :
{l : Level} {A : UU l} {x y : A} {p q r : x ＝ y} {α : p ＝ q} {γ δ : q ＝ r}
{τ : γ ＝ δ} → y-concat-Id³ (refl {x = α}) τ ＝ ap (concat α r) τ
left-unit-law-y-concat-Id³ {τ = τ} = left-unit-law-horizontal-concat-Id² τ

right-unit-law-y-concat-Id³ :
{l : Level} {A : UU l} {x y : A} {p q r : x ＝ y} {α β : p ＝ q} {γ : q ＝ r}
{σ : α ＝ β} → y-concat-Id³ σ (refl {x = γ}) ＝ ap (concat' p γ) σ
right-unit-law-y-concat-Id³ {σ = σ} = right-unit-law-horizontal-concat-Id² σ

left-unit-law-z-concat-Id³ :
{l : Level} {A : UU l} {x y z : A} {p q : x ＝ y} {u v : y ＝ z}
{α : p ＝ q} {γ δ : u ＝ v} (τ : γ ＝ δ) →
z-concat-Id³ (refl {x = α}) τ ＝ ap (horizontal-concat-Id² α) τ
left-unit-law-z-concat-Id³ τ =
left-unit-ap-binary (λ s t → horizontal-concat-Id² s t) τ

right-unit-law-z-concat-Id³ :
{l : Level} {A : UU l} {x y z : A} {p q : x ＝ y} {u v : y ＝ z}
{α β : p ＝ q} {γ : u ＝ v} (σ : α ＝ β) →
z-concat-Id³ σ (refl {x = γ}) ＝ ap (λ ω → horizontal-concat-Id² ω γ) σ
right-unit-law-z-concat-Id³ σ =
right-unit-ap-binary (λ s t → horizontal-concat-Id² s t) σ


### Interchange laws for 3-paths for the concatenation operations on 3-paths

interchange-x-y-concat-Id³ :
{l : Level} {A : UU l} {x y : A} {p q r : x ＝ y} {α β γ : p ＝ q}
{δ ε ζ : q ＝ r} (σ : α ＝ β) (τ : β ＝ γ) (υ : δ ＝ ε) (ϕ : ε ＝ ζ) →
( y-concat-Id³ (x-concat-Id³ σ τ) (x-concat-Id³ υ ϕ)) ＝
( x-concat-Id³ (y-concat-Id³ σ υ) (y-concat-Id³ τ ϕ))
interchange-x-y-concat-Id³ = interchange-Id²

interchange-x-z-concat-Id³ :
{l : Level} {A : UU l} {x y z : A} {p q : x ＝ y} {u v : y ＝ z}
{α β γ : p ＝ q} {δ ε ζ : u ＝ v} (σ : α ＝ β) (τ : β ＝ γ) (υ : δ ＝ ε)
(ϕ : ε ＝ ζ) →
( z-concat-Id³ (x-concat-Id³ σ τ) (x-concat-Id³ υ ϕ)) ＝
( x-concat-Id³ (z-concat-Id³ σ υ) (z-concat-Id³ τ ϕ))
interchange-x-z-concat-Id³ refl τ refl ϕ = refl

interchange-y-z-concat-Id³ :
{l : Level} {A : UU l} {x y z : A} {p q r : x ＝ y} {u v w : y ＝ z}
{α β : p ＝ q} {γ δ : q ＝ r} {ε ζ : u ＝ v} {η θ : v ＝ w}
(σ : α ＝ β) (τ : γ ＝ δ) (υ : ε ＝ ζ) (ϕ : η ＝ θ) →
( ( z-concat-Id³ (y-concat-Id³ σ τ) (y-concat-Id³ υ ϕ)) ∙
( interchange-Id² β δ ζ θ)) ＝
( ( interchange-Id² α γ ε η) ∙
( y-concat-Id³ (z-concat-Id³ σ υ) (z-concat-Id³ τ ϕ)))
interchange-y-z-concat-Id³ refl refl refl refl = inv right-unit


## Properties of 4-paths

The pattern for concatenation of 1, 2, and 3-paths continues. There are four ways to concatenate in quadruple identity types. We name the three non-standard concatenations in quadruple identity types i-, j-, and k-concatenation, after the standard names for the quaternions i, j, and k.

### Concatenation of four paths

#### The standard concatination

concat-Id⁴ :
{l : Level} {A : UU l} {x y : A} {p q : x ＝ y} {α β : p ＝ q}
{r s t : α ＝ β} → r ＝ s → s ＝ t → r ＝ t
concat-Id⁴ σ τ = x-concat-Id³ σ τ


#### Concatination induced by concatination of boundary 1-paths

i-concat-Id⁴ :
{l : Level} {A : UU l} {x y : A} {p q : x ＝ y} {α β γ : p ＝ q} →
{s s' : α ＝ β} (σ : s ＝ s') {t t' : β ＝ γ} (τ : t ＝ t') →
x-concat-Id³ s t ＝ x-concat-Id³ s' t'
i-concat-Id⁴ σ τ = y-concat-Id³ σ τ


#### Concatination induced by concatination of boundary 2-paths

j-concat-Id⁴ :
{l : Level} {A : UU l} {x y : A} {p q r : x ＝ y} {α β : p ＝ q}
{γ δ : q ＝ r} {s s' : α ＝ β} (σ : s ＝ s') {t t' : γ ＝ δ} (τ : t ＝ t') →
y-concat-Id³ s t ＝ y-concat-Id³ s' t'
j-concat-Id⁴ σ τ = z-concat-Id³ σ τ


#### Concatination induced by concatination of boundary 3-paths

k-concat-Id⁴ :
{l : Level} {A : UU l} {x y z : A} {p q : x ＝ y} {u v : y ＝ z}
{α β : p ＝ q} {γ δ : u ＝ v} {s s' : α ＝ β} (σ : s ＝ s') {t t' : γ ＝ δ}
(τ : t ＝ t') → z-concat-Id³ s t ＝ z-concat-Id³ s' t'
k-concat-Id⁴ σ τ = ap-binary (λ m n → z-concat-Id³ m n) σ τ


### Commuting cubes

module _
{l : Level} {A : UU l} {x000 x001 x010 x100 x011 x101 x110 x111 : A}
where

cube :
(p000̂ : x000 ＝ x001) (p00̂0 : x000 ＝ x010) (p0̂00 : x000 ＝ x100)
(p00̂1 : x001 ＝ x011) (p0̂01 : x001 ＝ x101) (p010̂ : x010 ＝ x011)
(p0̂10 : x010 ＝ x110) (p100̂ : x100 ＝ x101) (p10̂0 : x100 ＝ x110)
(p0̂11 : x011 ＝ x111) (p10̂1 : x101 ＝ x111) (p110̂ : x110 ＝ x111)
(p00̂0̂ : coherence-square-identifications p000̂ p00̂1 p00̂0 p010̂)
(p0̂00̂ : coherence-square-identifications p000̂ p0̂01 p0̂00 p100̂)
(p0̂0̂0 : coherence-square-identifications p00̂0 p0̂10 p0̂00 p10̂0)
(p0̂0̂1 : coherence-square-identifications p00̂1 p0̂11 p0̂01 p10̂1)
(p0̂10̂ : coherence-square-identifications p010̂ p0̂11 p0̂10 p110̂)
(p10̂0̂ : coherence-square-identifications p100̂ p10̂1 p10̂0 p110̂) → UU l
cube
p000̂ p00̂0 p0̂00 p00̂1 p0̂01 p010̂ p0̂10 p100̂ p10̂0 p0̂11 p10̂1 p110̂
p00̂0̂ p0̂00̂ p0̂0̂0 p0̂0̂1 p0̂10̂ p10̂0̂ =
Id
( ( ap (concat' x000 p0̂11) p00̂0̂) ∙
( ( assoc p00̂0 p010̂ p0̂11) ∙
( ( ap (concat p00̂0 x111) p0̂10̂) ∙
( ( inv (assoc p00̂0 p0̂10 p110̂)) ∙
( ( ap (concat' x000 p110̂) p0̂0̂0) ∙
( assoc p0̂00 p10̂0 p110̂))))))
( ( assoc p000̂ p00̂1 p0̂11) ∙
( ( ap (concat p000̂ x111) p0̂0̂1) ∙
( ( inv (assoc p000̂ p0̂01 p10̂1)) ∙
( ( ap (concat' x000 p10̂1) p0̂00̂) ∙
( ( assoc p0̂00 p100̂ p10̂1) ∙
( ( ap (concat p0̂00 x111) p10̂0̂)))))))