Commuting triangles of identifications
Content created by Fredrik Bakke, Egbert Rijke and Vojtěch Štěpančík.
Created on 2023-11-24.
Last modified on 2024-04-17.
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:
-
Prepending
p : u ＝ xto the left gives us a commuting trianglep ∙ top u ----> y \ / p ∙ left \ / right ∨ ∨ z.In other words, we have a map
(left ＝ top ∙ right) → (p ∙ left ＝ (p ∙ top) ∙ right). -
Appending an identification
p : z ＝ uto the right gives a commuting triangle of identificationstop x ----> y \ / left ∙ p \ / right ∙ p ∨ ∨ u.In other words, we have a map
(left ＝ top ∙ right) → (left ∙ p ＝ top ∙ (right ∙ p)). -
Splicing an identification
p : y ＝ uand its inverse into the middle gives a commuting triangle of identificationstop ∙ 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))
without further ado.
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
Recent changes
- 2024-04-17. Fredrik Bakke. Splitting idempotents (#1105).
- 2024-04-16. Vojtěch Štěpančík. Descent data for sequential colimits and its version of the flattening lemma (#1109).
- 2024-03-13. Egbert Rijke. Refactoring pointed types (#1056).
- 2024-02-19. Fredrik Bakke. Additions for coherently invertible maps (#1024).
- 2024-02-06. Egbert Rijke and Fredrik Bakke. Refactor files about identity types and homotopies (#1014).