# Commuting triangles of identifications

Content created by Fredrik Bakke, Egbert Rijke and Vojtěch Štěpančík.

Created on 2023-11-24.

module foundation.commuting-triangles-of-identifications where

Imports
open import foundation.action-on-identifications-functions
open import foundation.binary-equivalences
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels
open import foundation.whiskering-identifications-concatenation

open import foundation-core.commuting-squares-of-identifications
open import foundation-core.equivalences


## Idea

A triangle of identifications

        top
x ----> y
\     /
left \   / right
∨ ∨
z


is said to commute if there is an identification p ＝ q ∙ r.

## Definitions

### Commuting triangles of identifications

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

coherence-triangle-identifications :
(left : x ＝ z) (right : y ＝ z) (top : x ＝ y) → UU l
coherence-triangle-identifications left right top = left ＝ top ∙ right

coherence-triangle-identifications' :
(left : x ＝ z) (right : y ＝ z) (top : x ＝ y) → UU l
coherence-triangle-identifications' left right top = top ∙ right ＝ left


### The horizontally constant triangle of identifications

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

horizontal-refl-coherence-triangle-identifications :
(p : x ＝ y) → coherence-triangle-identifications p p refl
horizontal-refl-coherence-triangle-identifications p = refl


## Properties

### Whiskering of triangles of identifications

Given a commuting triangle of identifications

        top
x ----> y
\     /
left \   / right
∨ ∨
z,


we may consider three ways of attaching new identifications to it:

1. Prepending p : u ＝ x to the left gives us a commuting triangle

          p ∙ top
u ----> y
\     /
p ∙ left \   / right
∨ ∨
z.


In other words, we have a map

  (left ＝ top ∙ right) → (p ∙ left ＝ (p ∙ top) ∙ right).

2. Appending an identification p : z ＝ u to the right gives a commuting triangle of identifications

            top
x ----> y
\     /
left ∙ p \   / right ∙ p
∨ ∨
u.


In other words, we have a map

  (left ＝ top ∙ right) → (left ∙ p ＝ top ∙ (right ∙ p)).


3. Splicing an identification p : y ＝ u and its inverse into the middle gives a commuting triangle of identifications

      top ∙ p
x ----> u
\     /
left \   / p⁻¹ ∙ right
∨ ∨
z.


In other words, we have a map

  (left ＝ top ∙ right) → left ＝ (top ∙ p) ∙ (p⁻¹ ∙ right).


Similarly, we have a map

  (left ＝ top ∙ right) → left ＝ (top ∙ p⁻¹) ∙ (p ∙ right).


Because concatenation of identifications is an equivalence, it follows that all of these transformations are equivalences.

These operations are useful in proofs involving path algebra, because taking equiv-right-whisker-triangle-identifications as an example, it provides us with two maps: the forward direction states (p ＝ q ∙ r) → (p ∙ s ＝ q ∙ (r ∙ s)), which allows one to append an identification without needing to reassociate on the right, and the backwards direction conversely allows one to cancel out an identification in parentheses.

#### Left whiskering commuting squares of identifications

There is an equivalence of commuting squares

        top                        p ∙ top
x ----> y                    u ----> y
\     /                      \     /
left \   / right    ≃    p ∙ left \   / right
∨ ∨                          ∨ ∨
z                            z


for any identification p : u ＝ x.

module _
{l : Level} {A : UU l} {x y z u : A}
(p : u ＝ x) (left : x ＝ z) (right : y ＝ z) (top : x ＝ y)
where

equiv-left-whisker-concat-coherence-triangle-identifications :
coherence-triangle-identifications left right top ≃
coherence-triangle-identifications (p ∙ left) right (p ∙ top)
equiv-left-whisker-concat-coherence-triangle-identifications =
( equiv-inv-concat' _ (assoc p top right)) ∘e
( equiv-left-whisker-concat p)

left-whisker-concat-coherence-triangle-identifications :
coherence-triangle-identifications left right top →
coherence-triangle-identifications (p ∙ left) right (p ∙ top)
left-whisker-concat-coherence-triangle-identifications =
map-equiv equiv-left-whisker-concat-coherence-triangle-identifications

left-unwhisker-concat-coherence-triangle-identifications :
coherence-triangle-identifications (p ∙ left) right (p ∙ top) →
coherence-triangle-identifications left right top
left-unwhisker-concat-coherence-triangle-identifications =
map-inv-equiv equiv-left-whisker-concat-coherence-triangle-identifications

is-equiv-left-whisker-concat-coherence-triangle-identifications :
is-equiv
( left-whisker-concat-coherence-triangle-identifications)
is-equiv-left-whisker-concat-coherence-triangle-identifications =
is-equiv-map-equiv
equiv-left-whisker-concat-coherence-triangle-identifications

equiv-left-whisker-concat-coherence-triangle-identifications' :
coherence-triangle-identifications' left right top ≃
coherence-triangle-identifications' (p ∙ left) right (p ∙ top)
equiv-left-whisker-concat-coherence-triangle-identifications' =
( equiv-concat (assoc p top right) _) ∘e
( equiv-left-whisker-concat p)

left-whisker-concat-coherence-triangle-identifications' :
coherence-triangle-identifications' left right top →
coherence-triangle-identifications' (p ∙ left) right (p ∙ top)
left-whisker-concat-coherence-triangle-identifications' =
map-equiv equiv-left-whisker-concat-coherence-triangle-identifications'

left-unwhisker-concat-coherence-triangle-identifications' :
coherence-triangle-identifications' (p ∙ left) right (p ∙ top) →
coherence-triangle-identifications' left right top
left-unwhisker-concat-coherence-triangle-identifications' =
map-inv-equiv equiv-left-whisker-concat-coherence-triangle-identifications'

is-equiv-left-whisker-concat-coherence-triangle-identifications' :
is-equiv left-whisker-concat-coherence-triangle-identifications'
is-equiv-left-whisker-concat-coherence-triangle-identifications' =
is-equiv-map-equiv
equiv-left-whisker-concat-coherence-triangle-identifications'


#### Right whiskering commuting squares of identifications

There is an equivalence of commuting triangles of identifications

        top                            top
x ----> y                      x ----> y
\     /                        \     /
left \   / right     ≃     left ∙ p \   / right ∙ p
∨ ∨                            ∨ ∨
z                              u


for any identification p : z ＝ u.

module _
{l : Level} {A : UU l} {x y z u : A}
(left : x ＝ z) (right : y ＝ z) (top : x ＝ y) (p : z ＝ u)
where

equiv-right-whisker-concat-coherence-triangle-identifications :
coherence-triangle-identifications left right top ≃
coherence-triangle-identifications (left ∙ p) (right ∙ p) top
equiv-right-whisker-concat-coherence-triangle-identifications =
( equiv-concat-assoc' (left ∙ p) top right p) ∘e
( equiv-right-whisker-concat p)

right-whisker-concat-coherence-triangle-identifications :
coherence-triangle-identifications left right top →
coherence-triangle-identifications (left ∙ p) (right ∙ p) top
right-whisker-concat-coherence-triangle-identifications =
map-equiv equiv-right-whisker-concat-coherence-triangle-identifications

right-unwhisker-concat-coherence-triangle-identifications :
coherence-triangle-identifications (left ∙ p) (right ∙ p) top →
coherence-triangle-identifications left right top
right-unwhisker-concat-coherence-triangle-identifications =
map-inv-equiv equiv-right-whisker-concat-coherence-triangle-identifications

is-equiv-right-whisker-concat-coherence-triangle-identifications :
is-equiv right-whisker-concat-coherence-triangle-identifications
is-equiv-right-whisker-concat-coherence-triangle-identifications =
is-equiv-map-equiv
equiv-right-whisker-concat-coherence-triangle-identifications

equiv-right-whisker-concat-coherence-triangle-identifications' :
coherence-triangle-identifications' left right top ≃
coherence-triangle-identifications' (left ∙ p) (right ∙ p) top
equiv-right-whisker-concat-coherence-triangle-identifications' =
( equiv-concat-assoc top right p (left ∙ p)) ∘e
( equiv-right-whisker-concat p)

right-whisker-concat-coherence-triangle-identifications' :
coherence-triangle-identifications' left right top →
coherence-triangle-identifications' (left ∙ p) (right ∙ p) top
right-whisker-concat-coherence-triangle-identifications' =
map-equiv equiv-right-whisker-concat-coherence-triangle-identifications'

right-unwhisker-concat-coherence-triangle-identifications' :
coherence-triangle-identifications' (left ∙ p) (right ∙ p) top →
coherence-triangle-identifications' left right top
right-unwhisker-concat-coherence-triangle-identifications' =
map-inv-equiv equiv-right-whisker-concat-coherence-triangle-identifications'

is-equiv-right-whisker-concat-coherence-triangle-identifications' :
is-equiv right-whisker-concat-coherence-triangle-identifications'
is-equiv-right-whisker-concat-coherence-triangle-identifications' =
is-equiv-map-equiv
equiv-right-whisker-concat-coherence-triangle-identifications'


#### Splicing a pair of mutual inverse identifications in a commuting triangle of identifications

Consider two identifications p : y ＝ u and q : u ＝ y equipped with an identification α : inv p ＝ q. Then we have an equivalence of commuting triangles of identifications

        top                       top ∙ p
x ----> y                   x ----> u
\     /                     \     /
left \   / right     ≃     left  \   / q ∙ right
∨ ∨                         ∨ ∨
z                           z.


Note that we have formulated the equivalence in such a way that it gives us both equivalences

  (left ＝ top ∙ right) ≃ (left ＝ (top ∙ p) ∙ (p⁻¹ ∙ right)),


and

  (left ＝ top ∙ right) ≃ (left ＝ (top ∙ p⁻¹) ∙ (p ∙ right))


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

equiv-splice-coherence-triangle-identifications :
(p : y ＝ u) (q : u ＝ y) (α : inv p ＝ q) →
(left : x ＝ z) (right : y ＝ z) (top : x ＝ y) →
coherence-triangle-identifications left right top ≃
coherence-triangle-identifications left (q ∙ right) (top ∙ p)
equiv-splice-coherence-triangle-identifications refl .refl refl
left right top =
equiv-concat' left (right-whisker-concat (inv right-unit) right)

splice-coherence-triangle-identifications :
(p : y ＝ u) (q : u ＝ y) (α : inv p ＝ q) →
(left : x ＝ z) (right : y ＝ z) (top : x ＝ y) →
coherence-triangle-identifications left right top →
coherence-triangle-identifications left (q ∙ right) (top ∙ p)
splice-coherence-triangle-identifications refl .refl refl
left right top t =
t ∙ inv (right-whisker-concat right-unit right)

unsplice-coherence-triangle-identifications :
(p : y ＝ u) (q : u ＝ y) (α : inv p ＝ q) →
(left : x ＝ z) (right : y ＝ z) (top : x ＝ y) →
coherence-triangle-identifications left (q ∙ right) (top ∙ p) →
coherence-triangle-identifications left right top
unsplice-coherence-triangle-identifications refl .refl refl
left right top t =
t ∙ right-whisker-concat right-unit right

equiv-splice-coherence-triangle-identifications' :
(p : y ＝ u) (q : u ＝ y) (α : inv p ＝ q) →
(left : x ＝ z) (right : y ＝ z) (top : x ＝ y) →
coherence-triangle-identifications' left right top ≃
coherence-triangle-identifications' left (q ∙ right) (top ∙ p)
equiv-splice-coherence-triangle-identifications' refl .refl refl
left right top =
equiv-concat (right-whisker-concat right-unit right) left

splice-coherence-triangle-identifications' :
(p : y ＝ u) (q : u ＝ y) (α : inv p ＝ q) →
(left : x ＝ z) (right : y ＝ z) (top : x ＝ y) →
coherence-triangle-identifications' left right top →
coherence-triangle-identifications' left (q ∙ right) (top ∙ p)
splice-coherence-triangle-identifications' refl .refl refl
left right top t =
right-whisker-concat right-unit right ∙ t

unsplice-coherence-triangle-identifications' :
(p : y ＝ u) (q : u ＝ y) (α : inv p ＝ q) →
(left : x ＝ z) (right : y ＝ z) (top : x ＝ y) →
coherence-triangle-identifications' left (q ∙ right) (top ∙ p) →
coherence-triangle-identifications' left right top
unsplice-coherence-triangle-identifications' refl .refl refl
left right top t =
inv (right-whisker-concat right-unit right) ∙ t


### The action of functions on commuting triangles of identifications

Consider a commuting triangle of identifications

        top
x ----> y
\     /
left \   / right
∨ ∨
z


in a type A and consider a map f : A → B. Then we obtain a commuting triangle of identifications

          ap f top
f x ----> f y
\     /
ap f left \   / ap f right
∨ ∨
f z


Furthermore, in the case where the identification right is refl we obtain an identification

  inv right-unit ＝
map-coherence-triangle-identifications p refl p (inv right-unit)


and in the case where the identification top is refl we obtain

  refl ＝ map-coherence-triangle-identifications p p refl refl.

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
where

map-coherence-triangle-identifications :
{x y z : A} (left : x ＝ z) (right : y ＝ z) (top : x ＝ y) →
coherence-triangle-identifications left right top →
coherence-triangle-identifications (ap f left) (ap f right) (ap f top)
map-coherence-triangle-identifications .(top ∙ right) right top refl =
ap-concat f top right

compute-refl-right-map-coherence-triangle-identifications :
{x y : A} (p : x ＝ y) →
inv right-unit ＝
map-coherence-triangle-identifications p refl p (inv right-unit)
compute-refl-right-map-coherence-triangle-identifications refl = refl

compute-refl-top-map-coherence-triangle-identifications :
{x y : A} (p : x ＝ y) →
refl ＝ map-coherence-triangle-identifications p p refl refl
compute-refl-top-map-coherence-triangle-identifications p = refl


### Inverting one side of a commuting triangle of identifications

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

transpose-top-coherence-triangle-identifications :
{a b c : A} (left : a ＝ c) (right : b ＝ c) (top : b ＝ a)
{top' : a ＝ b} (α : inv top ＝ top') →
coherence-triangle-identifications right left top →
coherence-triangle-identifications left right top'
transpose-top-coherence-triangle-identifications left right top refl t =
left-transpose-eq-concat _ _ _ (inv t)

equiv-transpose-top-coherence-triangle-identifications :
{a b c : A} (left : a ＝ c) (right : b ＝ c) (top : b ＝ a) →
coherence-triangle-identifications right left top ≃
coherence-triangle-identifications left right (inv top)
equiv-transpose-top-coherence-triangle-identifications left right top =
equiv-left-transpose-eq-concat _ _ _ ∘e equiv-inv _ _

equiv-higher-transpose-top-coherence-triangle-identifications :
{a b c : A} (left : a ＝ c) (right : b ＝ c) (top : b ＝ a)
{left' : a ＝ c} (p : left ＝ left')
{top' : a ＝ b} (α : inv top ＝ top') →
(s : coherence-triangle-identifications right left top) →
(t : coherence-triangle-identifications right left' top) →
coherence-triangle-identifications t (left-whisker-concat top p) s ≃
coherence-triangle-identifications
( transpose-top-coherence-triangle-identifications left right top α s)
( transpose-top-coherence-triangle-identifications left' right top α t)
( p)
equiv-higher-transpose-top-coherence-triangle-identifications
left right top refl refl s t =
( equiv-ap
( equiv-transpose-top-coherence-triangle-identifications left right top)
( _)
( _)) ∘e
( equiv-inv _ _) ∘e
( equiv-concat' _ right-unit)

higher-transpose-top-coherence-triangle-identifications :
{a b c : A} (left : a ＝ c) (right : b ＝ c) (top : b ＝ a) →
{left' : a ＝ c} (p : left ＝ left')
{top' : a ＝ b} (q : inv top ＝ top') →
(s : coherence-triangle-identifications right left top) →
(t : coherence-triangle-identifications right left' top) →
coherence-triangle-identifications t (left-whisker-concat top p) s →
coherence-triangle-identifications
( transpose-top-coherence-triangle-identifications left right top q s)
( transpose-top-coherence-triangle-identifications left' right top q t)
( p)
higher-transpose-top-coherence-triangle-identifications
left right top p q s t =
map-equiv
( equiv-higher-transpose-top-coherence-triangle-identifications
left right top p q s t)

transpose-right-coherence-triangle-identifications :
{a b c : A} (left : a ＝ c) (right : c ＝ b) (top : a ＝ b)
{right' : b ＝ c} (p : inv right ＝ right') →
coherence-triangle-identifications top right left →
coherence-triangle-identifications left right' top
transpose-right-coherence-triangle-identifications left right top refl t =
right-transpose-eq-concat _ _ _ (inv t)

equiv-transpose-right-coherence-triangle-identifications :
{a b c : A} (left : a ＝ c) (right : c ＝ b) (top : a ＝ b) →
coherence-triangle-identifications top right left ≃
coherence-triangle-identifications left (inv right) top
equiv-transpose-right-coherence-triangle-identifications left right top =
equiv-right-transpose-eq-concat _ _ _ ∘e equiv-inv _ _

equiv-higher-transpose-right-coherence-triangle-identifications :
{a b c : A} (left : a ＝ c) (right : c ＝ b) (top : a ＝ b) →
{left' : a ＝ c} (p : left ＝ left')
{right' : b ＝ c} (q : inv right ＝ right') →
(s : coherence-triangle-identifications top right left) →
(t : coherence-triangle-identifications top right left') →
coherence-triangle-identifications t (right-whisker-concat p right) s ≃
coherence-triangle-identifications
( transpose-right-coherence-triangle-identifications left right top q s)
( transpose-right-coherence-triangle-identifications left' right top q t)
( p)
equiv-higher-transpose-right-coherence-triangle-identifications
left right top refl refl s t =
( equiv-ap
( equiv-transpose-right-coherence-triangle-identifications left right top)
( _)
( _)) ∘e
( equiv-inv _ _) ∘e
( equiv-concat' t right-unit)

higher-transpose-right-coherence-triangle-identifications :
{a b c : A} (left : a ＝ c) (right : c ＝ b) (top : a ＝ b) →
{left' : a ＝ c} (p : left ＝ left')
{right' : b ＝ c} (q : inv right ＝ right') →
(s : coherence-triangle-identifications top right left) →
(t : coherence-triangle-identifications top right left') →
coherence-triangle-identifications t (right-whisker-concat p right) s →
coherence-triangle-identifications
( transpose-right-coherence-triangle-identifications left right top q s)
( transpose-right-coherence-triangle-identifications left' right top q t)
( p)
higher-transpose-right-coherence-triangle-identifications
left right top p q s t =
map-equiv
( equiv-higher-transpose-right-coherence-triangle-identifications
( left)
( right)
( top)
( p)
( q)
( s)
( t))


### Inverting all sides of a commuting triangle of identifications

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

inv-coherence-triangle-identifications :
(left : x ＝ z) (right : y ＝ z) (top : x ＝ y) →
coherence-triangle-identifications left right top →
coherence-triangle-identifications (inv left) (inv top) (inv right)
inv-coherence-triangle-identifications .(top ∙ right) right top refl =
distributive-inv-concat top right


### Concatenating identifications on edges with coherences of commuting triangles of identifications

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

equiv-concat-top-coherence-triangle-identifications :
{a b c : A} (left : a ＝ c) (right : b ＝ c) (top : a ＝ b)
{top' : a ＝ b} (p : top' ＝ top) →
coherence-triangle-identifications left right top' ≃
coherence-triangle-identifications left right top
equiv-concat-top-coherence-triangle-identifications left right top p =
equiv-concat' left (right-whisker-concat p right)

concat-top-coherence-triangle-identifications :
{a b c : A} (left : a ＝ c) (right : b ＝ c) (top : a ＝ b)
{top' : a ＝ b} (p : top' ＝ top) →
coherence-triangle-identifications left right top' →
coherence-triangle-identifications left right top
concat-top-coherence-triangle-identifications left right top p =
map-equiv
( equiv-concat-top-coherence-triangle-identifications left right top p)

equiv-concat-right-coherence-triangle-identifications :
{a b c : A} (left : a ＝ c) (right : b ＝ c) (top : a ＝ b)
{right' : b ＝ c} (p : right' ＝ right) →
coherence-triangle-identifications left right' top ≃
coherence-triangle-identifications left right top
equiv-concat-right-coherence-triangle-identifications left right top p =
equiv-concat' left (left-whisker-concat top p)

concat-right-coherence-triangle-identifications :
{a b c : A} (left : a ＝ c) (right : b ＝ c) (top : a ＝ b)
{right' : b ＝ c} (p : right' ＝ right) →
coherence-triangle-identifications left right' top →
coherence-triangle-identifications left right top
concat-right-coherence-triangle-identifications left right top p =
map-equiv
( equiv-concat-right-coherence-triangle-identifications left right top p)

equiv-concat-left-coherence-triangle-identifications :
{a b c : A} (left : a ＝ c) (right : b ＝ c) (top : a ＝ b)
{left' : a ＝ c} (p : left ＝ left') →
coherence-triangle-identifications left' right top ≃
coherence-triangle-identifications left right top
equiv-concat-left-coherence-triangle-identifications left right top p =
equiv-concat p (top ∙ right)

concat-left-coherence-triangle-identifications :
{a b c : A} (left : a ＝ c) (right : b ＝ c) (top : a ＝ b)
{left' : a ＝ c} (p : left ＝ left') →
coherence-triangle-identifications left' right top →
coherence-triangle-identifications left right top
concat-left-coherence-triangle-identifications left right top p =
map-equiv
( equiv-concat-left-coherence-triangle-identifications left right top p)


### Horizontal pasting of commuting triangles of identifications

Consider a commuting diagram of identifications of the form

  top-left   top-right
a ---> b ---> c
\    |    /
left \   |m  / right
\  |  /
∨ ∨ ∨
d


Then the outer triangle commutes too. Indeed, an identification left ＝ top-left ∙ middle is given. Then, an identification

  top-left ∙ middle ＝ (top-left ∙ top-right) ∙ right


is obtained immediately by left whiskering the right triangle with the identification top-left. Note that this direct construction of the coherence of the outer commuting triangle of identifications avoids any use of associativity.

module _
{l : Level} {A : UU l}
{a b c d : A} (left : a ＝ d) (middle : b ＝ d) (right : c ＝ d)
(top-left : a ＝ b) (top-right : b ＝ c)
where

horizontal-pasting-coherence-triangle-identifications :
coherence-triangle-identifications left middle top-left →
coherence-triangle-identifications middle right top-right →
coherence-triangle-identifications left right (top-left ∙ top-right)
horizontal-pasting-coherence-triangle-identifications s t =
( s) ∙
( left-whisker-concat-coherence-triangle-identifications
( top-left)
( middle)
( right)
( top-right)
( t))


### Horizontal pasting of commuting triangles of identifications is a binary equivalence

module _
{l : Level} {A : UU l}
{a b c d : A} (left : a ＝ d) (middle : b ＝ d) (right : c ＝ d)
(top-left : a ＝ b) (top-right : b ＝ c)
where

abstract
is-equiv-horizontal-pasting-coherence-triangle-identifications :
(s : coherence-triangle-identifications left middle top-left) →
is-equiv
( horizontal-pasting-coherence-triangle-identifications
( left)
( middle)
( right)
( top-left)
( top-right)
( s))
is-equiv-horizontal-pasting-coherence-triangle-identifications s =
is-equiv-comp _ _
( is-equiv-left-whisker-concat-coherence-triangle-identifications
( top-left)
( middle)
( right)
( top-right))
( is-equiv-concat s _)

equiv-horizontal-pasting-coherence-triangle-identifications :
(s : coherence-triangle-identifications left middle top-left) →
coherence-triangle-identifications middle right top-right ≃
coherence-triangle-identifications left right (top-left ∙ top-right)
pr1 (equiv-horizontal-pasting-coherence-triangle-identifications s) =
horizontal-pasting-coherence-triangle-identifications _ _ _ _ _ s
pr2 (equiv-horizontal-pasting-coherence-triangle-identifications s) =
is-equiv-horizontal-pasting-coherence-triangle-identifications s

abstract
is-equiv-horizontal-pasting-coherence-triangle-identifications' :
(t : coherence-triangle-identifications middle right top-right) →
is-equiv
( λ s →
horizontal-pasting-coherence-triangle-identifications
( left)
( middle)
( right)
( top-left)
( top-right)
( s)
( t))
is-equiv-horizontal-pasting-coherence-triangle-identifications' t =
is-equiv-concat' _
( left-whisker-concat-coherence-triangle-identifications
( top-left)
( middle)
( right)
( top-right)
( t))

equiv-horizontal-pasting-coherence-triangle-identifications' :
(t : coherence-triangle-identifications middle right top-right) →
coherence-triangle-identifications left middle top-left ≃
coherence-triangle-identifications left right (top-left ∙ top-right)
pr1 (equiv-horizontal-pasting-coherence-triangle-identifications' t) s =
horizontal-pasting-coherence-triangle-identifications
( left)
( middle)
( right)
( top-left)
( top-right)
( s)
( t)
pr2 (equiv-horizontal-pasting-coherence-triangle-identifications' t) =
is-equiv-horizontal-pasting-coherence-triangle-identifications' t

is-binary-equiv-horizontal-pasting-coherence-triangle-identifications :
is-binary-equiv
( horizontal-pasting-coherence-triangle-identifications
( left)
( middle)
( right)
( top-left)
( top-right))
pr1 is-binary-equiv-horizontal-pasting-coherence-triangle-identifications =
is-equiv-horizontal-pasting-coherence-triangle-identifications'
pr2 is-binary-equiv-horizontal-pasting-coherence-triangle-identifications =
is-equiv-horizontal-pasting-coherence-triangle-identifications


### The left unit law for horizontal pastinf of commuting triangles of identifications

Consider a commuting triangle of identifications

         top
a ------> b
\       /
left \     / right
\   /
∨ ∨
c


with t : left ＝ top ∙ right. Then we have an identification

  horizontal-pasting left left right refl top refl t ＝ t

module _
{l : Level} {A : UU l} {a b c : A}
where

left-unit-law-horizontal-pasting-coherence-triangle-identifications :
(left : a ＝ c) (right : b ＝ c) (top : a ＝ b) →
(t : coherence-triangle-identifications left right top) →
horizontal-pasting-coherence-triangle-identifications
( left)
( left)
( right)
( refl)
( top)
( refl)
( t) ＝
t
left-unit-law-horizontal-pasting-coherence-triangle-identifications
._ right top refl =
refl


### The left unit law for horizontal pastinf of commuting triangles of identifications

Consider a commuting triangle of identifications

         top
a ------> b
\       /
left \     / right
\   /
∨ ∨
c


with t : left ＝ top ∙ right. Then we have a commuting triangle of identifications

      horizontal-pasting t refl
left ----------------------> (top ∙ refl) ∙ right
\                     /
\                   /
t \                 / right-whisker right-unit right
\               /
\             /
∨           ∨
top ∙ right

module _
{l : Level} {A : UU l} {a b c : A}
where

right-unit-law-horizontal-pasting-coherence-triangle-identifications :
(left : a ＝ c) (right : b ＝ c) (top : a ＝ b) →
(t : coherence-triangle-identifications left right top) →
coherence-triangle-identifications
( t)
( right-whisker-concat right-unit right)
( horizontal-pasting-coherence-triangle-identifications
( left)
( right)
( right)
( top)
( refl)
( t)
( refl))
right-unit-law-horizontal-pasting-coherence-triangle-identifications
._ right refl refl = refl


### Associativity of horizontal pasting of coherences of commuting triangles of identifications

module _
{l : Level} {A : UU l} {a b c d e : A}
where

associative-horizontal-pasting-coherence-triangle-identifications :
(left : a ＝ e) (mid-left : b ＝ e) (mid-right : c ＝ e) (right : d ＝ e)
(top-left : a ＝ b) (top-middle : b ＝ c) (top-right : c ＝ d)
(r : coherence-triangle-identifications left mid-left top-left) →
(s : coherence-triangle-identifications mid-left mid-right top-middle) →
(t : coherence-triangle-identifications mid-right right top-right) →
coherence-triangle-identifications
( horizontal-pasting-coherence-triangle-identifications
( left)
( mid-left)
( right)
( top-left)
( top-middle ∙ top-right)
( r)
( horizontal-pasting-coherence-triangle-identifications
( mid-left)
( mid-right)
( right)
( top-middle)
( top-right)
( s)
( t)))
( right-whisker-concat (assoc top-left top-middle top-right) right)
( horizontal-pasting-coherence-triangle-identifications
( left)
( mid-right)
( right)
( top-left ∙ top-middle)
( top-right)
( horizontal-pasting-coherence-triangle-identifications
( left)
( mid-left)
( mid-right)
( top-left)
( top-middle)
( r)
( s))
( t))
associative-horizontal-pasting-coherence-triangle-identifications
refl .refl .refl .refl refl refl refl refl refl refl =
refl


### Left whiskering of horizontal pasting of commuting triangles of identifications

Consider two commuting triangles of identifications as in the diagram

      s       t
a ----> b ----> c
\     |     /
\  L |  R /
l \   |m  / r
\  |  /
∨ ∨ ∨
d,


and consider furthermore a commuting triangle of identifications

             t'
b ----> c
|     /
| R' /
m |   / r
|  /
∨ ∨
d


where the identifications m : b ＝ d and r : c ＝ d are the same as in the previous diagram. Finally, consider an identification p : t ＝ t' and an identification q witnessing that the triangle

        R
m ------> t ∙ r
\       /
R' \     / right-whisker p r
\   /
∨ ∨
t' ∙ r


commutes. Then the triangle

                      horizontal-pasting L R
l ----------------> (s ∙ t) ∙ r
\               /
\             /
horizontal-pasting L R' \           / right-whisker (left-whisker s p) r
\         /
∨       ∨
(s ∙ t') ∙ r


commutes.

module _
{l : Level} {A : UU l} {a b c d : A}
where

left-whisker-horizontal-pasting-coherence-triangle-identifications :
(left : a ＝ d) (middle : b ＝ d) (right : c ＝ d)
(top-left : a ＝ b) (top-right top-right' : b ＝ c) →
(L : coherence-triangle-identifications left middle top-left)
(R : coherence-triangle-identifications middle right top-right)
(R' : coherence-triangle-identifications middle right top-right')
(p : top-right ＝ top-right') →
coherence-triangle-identifications R' (right-whisker-concat p right) R →
coherence-triangle-identifications
( horizontal-pasting-coherence-triangle-identifications
( left)
( middle)
( right)
( top-left)
( top-right')
( L)
( R'))
( right-whisker-concat (left-whisker-concat top-left p) right)
( horizontal-pasting-coherence-triangle-identifications
( left)
( middle)
( right)
( top-left)
( top-right)
( L)
( R))
left-whisker-horizontal-pasting-coherence-triangle-identifications
._ ._ refl refl refl .refl refl refl ._ refl refl =
refl


### Right whiskering of horizontal pasting of commuting triangles of identifications

Consider two commuting triangles of identifications as in the diagram

     s      t
a ----> b ----> c
\     |     /
\  L |  R /
l \   |m  / r
\  |  /
∨ ∨ ∨
d,


and consider furthermore a commuting triangle of identifications

      s'
a ----> b
\     |
\ L' |
l \   |m
\  |
∨ ∨
d,


where the identifications m : b ＝ d and l : a ＝ d are the same as in the previous diagram. Finally, consider an identification p : s ＝ s' and an identification q witnessing that the triangle

        L
l ------> s ∙ m
\       /
L' \     / right-whisker p m
\   /
∨ ∨
s' ∙ r


commutes. Then the triangle

                      horizontal-pasting L R
l ----------------> (s ∙ t) ∙ r
\               /
\             /
horizontal-pasting L R' \           / right-whisker (right-whisker p t) r
\         /
∨       ∨
(s' ∙ t) ∙ r


commutes.

module _
{l : Level} {A : UU l} {a b c d : A}
where

right-whisker-horizontal-pasting-coherence-triangle-identifications :
(left : a ＝ d) (middle : b ＝ d) (right : c ＝ d)
(top-left top-left' : a ＝ b) (top-right : b ＝ c) →
(L : coherence-triangle-identifications left middle top-left)
(L' : coherence-triangle-identifications left middle top-left')
(R : coherence-triangle-identifications middle right top-right)
(p : top-left ＝ top-left') →
coherence-triangle-identifications L' (right-whisker-concat p middle) L →
coherence-triangle-identifications
( horizontal-pasting-coherence-triangle-identifications
( left)
( middle)
( right)
( top-left')
( top-right)
( L')
( R))
( right-whisker-concat (right-whisker-concat p top-right) right)
( horizontal-pasting-coherence-triangle-identifications
( left)
( middle)
( right)
( top-left)
( top-right)
( L)
( R))
right-whisker-horizontal-pasting-coherence-triangle-identifications
refl .refl .refl refl .refl refl refl ._ refl refl refl =
refl


### Right pasting of commuting triangles of identifications

Consider a commuting diagram of identifications of the form

          top
a ------------> b
\ ⎻⎽          /
\  ⎺⎽ mid   / top-right
\   ⎺⎽    ∨
left \    ⎺> c
\     /
\   / bottom-right
∨ ∨
d


Then the outer triangle commutes too. Indeed, an identification left ＝ mid ∙ bottom-right is given. Then, an identification

  mid ∙ bottom-right ＝ top ∙ (top-right ∙ bottom-right)


is obtained immediately by right whiskering the upper triangle with the identification bottom-right. Note that this direct construction of the coherence of the outer commuting triangle of identifications avoids any use of associativity.

module _
{l : Level} {A : UU l} {a b c d : A}
(left : a ＝ d) (top-right : b ＝ c) (bottom-right : c ＝ d)
(middle : a ＝ c) (top : a ＝ b)
where

right-pasting-coherence-triangle-identifications :
(s : coherence-triangle-identifications left bottom-right middle) →
(t : coherence-triangle-identifications middle top-right top) →
coherence-triangle-identifications left (top-right ∙ bottom-right) top
right-pasting-coherence-triangle-identifications s t =
( s) ∙
( right-whisker-concat-coherence-triangle-identifications
( middle)
( top-right)
( top)
( bottom-right)
( t))


### Right pasting commuting triangles of identifications is a binary equivalence

module _
{l : Level} {A : UU l} {a b c d : A}
(left : a ＝ d) (top-right : b ＝ c) (bottom-right : c ＝ d)
(middle : a ＝ c) (top : a ＝ b)
where

abstract
is-equiv-right-pasting-coherence-triangle-identifications :
(s : coherence-triangle-identifications left bottom-right middle) →
is-equiv
( right-pasting-coherence-triangle-identifications
( left)
( top-right)
( bottom-right)
( middle)
( top)
( s))
is-equiv-right-pasting-coherence-triangle-identifications s =
is-equiv-comp _ _
( is-equiv-right-whisker-concat-coherence-triangle-identifications
( middle)
( top-right)
( top)
( bottom-right))
( is-equiv-concat s _)

equiv-right-pasting-coherence-triangle-identifications :
(s : coherence-triangle-identifications left bottom-right middle) →
coherence-triangle-identifications middle top-right top ≃
coherence-triangle-identifications left (top-right ∙ bottom-right) top
pr1 (equiv-right-pasting-coherence-triangle-identifications s) =
right-pasting-coherence-triangle-identifications
( left)
( top-right)
( bottom-right)
( middle)
( top)
( s)
pr2 (equiv-right-pasting-coherence-triangle-identifications s) =
is-equiv-right-pasting-coherence-triangle-identifications s

abstract
is-equiv-right-pasting-coherence-triangle-identifications' :
(t : coherence-triangle-identifications middle top-right top) →
is-equiv
( λ (s : coherence-triangle-identifications left bottom-right middle) →
right-pasting-coherence-triangle-identifications
( left)
( top-right)
( bottom-right)
( middle)
( top)
( s)
( t))
is-equiv-right-pasting-coherence-triangle-identifications' t =
is-equiv-concat' _
( right-whisker-concat-coherence-triangle-identifications
( middle)
( top-right)
( top)
( bottom-right)
( t))

equiv-right-pasting-coherence-triangle-identifications' :
(t : coherence-triangle-identifications middle top-right top) →
coherence-triangle-identifications left bottom-right middle ≃
coherence-triangle-identifications left (top-right ∙ bottom-right) top
pr1 (equiv-right-pasting-coherence-triangle-identifications' t) s =
right-pasting-coherence-triangle-identifications
( left)
( top-right)
( bottom-right)
( middle)
( top)
( s)
( t)
pr2 (equiv-right-pasting-coherence-triangle-identifications' t) =
is-equiv-right-pasting-coherence-triangle-identifications' t

is-binary-equiv-right-pasting-coherence-triangle-identifications :
is-binary-equiv
( right-pasting-coherence-triangle-identifications
( left)
( top-right)
( bottom-right)
( middle)
( top))
pr1 is-binary-equiv-right-pasting-coherence-triangle-identifications =
is-equiv-right-pasting-coherence-triangle-identifications'
pr2 is-binary-equiv-right-pasting-coherence-triangle-identifications =
is-equiv-right-pasting-coherence-triangle-identifications


### Left pasting of commuting triangles of identifications

Note. For left pasting there are two potential constructions. One takes a commuting diagram of identifications of the form

                top
a ------------> b
\          ⎽⎻ /
top-left \     m ⎽⎺  /
∨    ⎽⎺   /
c <⎺    / right
\     /
bottom-left \   /
∨ ∨
d


and returns an identification witnessing that the outer triangle commutes. In this case the top triangle is an ordinary commuting triangle of identifications, and the bottom triangle is inverted along the top edge m.

The other left pasting of commuting triangles of identifications takes a commuting diagram of identifications of the form

                top
a ------------> b
\         ⎽-> /
top-left \    m ⎽⎺   /
∨   ⎽⎺    /
c ⎺     / right
\     /
bottom-left \   /
∨ ∨
d


and returns an identification witnessing that the outer rectangle commutes. In this case the bottom triangle of identifications is an ordinary commuting triangle of identifications, and the top triangle is inverted along the right edge m.

Both constructions have yet to be formalized.

### Vertically pasting commuting squares and commuting triangles of identifications

Consider a diagram of the form

                top
a ------------> b
\             /
top-left \           / top-right
∨   mid   ∨
c ----> d
\     /
bottom-left \   / bottom-right
∨ ∨
e


with s : top-left ∙ mid ＝ top ∙ top-right witnessing that the square commutes, and with t : bottom-left ＝ mid ∙ bottom-right witnessing that the triangle commutes. Then the outer triangle commutes.

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

vertical-pasting-coherence-square-coherence-triangle-identifications :
{a b c d e : A}
(top : a ＝ b) (top-left : a ＝ c) (top-right : b ＝ d) (mid : c ＝ d)
(bottom-left : c ＝ e) (bottom-right : d ＝ e) →
coherence-square-identifications top top-left top-right mid →
coherence-triangle-identifications bottom-left bottom-right mid →
coherence-triangle-identifications
( top-left ∙ bottom-left)
( top-right ∙ bottom-right)
( top)
vertical-pasting-coherence-square-coherence-triangle-identifications
top top-left top-right mid bottom-left bottom-right s t =
( left-whisker-concat top-left t) ∙
( right-whisker-concat-coherence-square-identifications
( top)
( top-left)
( top-right)
( mid)
( s)
( bottom-right))


### Vertical pasting of horizontally constant commuting squares of identifications and commuting triangles of identifications

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

vertical-pasting-coherence-horizontally-constant-square-coherence-triangle-identifications :
{a c e : A} (p : a ＝ c)
(bottom-left : c ＝ e) (bottom-right : c ＝ e) →
(t : coherence-triangle-identifications bottom-left bottom-right refl) →
( vertical-pasting-coherence-square-coherence-triangle-identifications
( refl)
( p)
( p)
( refl)
( bottom-left)
( bottom-right)
( horizontal-refl-coherence-square-identifications p)
( t)) ＝
( left-whisker-concat p t)
vertical-pasting-coherence-horizontally-constant-square-coherence-triangle-identifications
refl refl .refl refl =
refl


### Vertical pasting of verticaly constant commuting squares of identifications and commuting triangles of identifications

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

vertical-pasting-coherence-vertically-constant-square-coherence-triangle-identifications :
{a b c : A} (left : a ＝ c) (right : b ＝ c) (top : a ＝ b) →
(t : coherence-triangle-identifications left right top) →
( vertical-pasting-coherence-square-coherence-triangle-identifications
( top)
( refl)
( refl)
( top)
( left)
( right)
( vertical-refl-coherence-square-identifications top)
( t)) ＝
t
vertical-pasting-coherence-vertically-constant-square-coherence-triangle-identifications
._ refl refl refl = refl