Commuting triangles of maps

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

Created on 2023-02-18.
Last modified on 2024-04-25.

module foundation-core.commuting-triangles-of-maps where
Imports 
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.retractions
open import foundation-core.sections

Idea

A triangle of maps

        top
     A ----> B
      \     /
  left \   / right
        ∨ ∨
         X

is said to commute if there is a homotopy between the map on the left and the composite of the top and right maps:

  left ~ right ∘ top.

Definitions

Commuting triangles of maps

module _
  {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3}
  where

  coherence-triangle-maps :
    (left : A → X) (right : B → X) (top : A → B) → UU (l1 ⊔ l2)
  coherence-triangle-maps left right top = left ~ right ∘ top

  coherence-triangle-maps' :
    (left : A → X) (right : B → X) (top : A → B) → UU (l1 ⊔ l2)
  coherence-triangle-maps' left right top = right ∘ top ~ left

Concatenation of commuting triangles of maps

module _
  {l1 l2 l3 l4 : Level} {X : UU l1} {A : UU l2} {B : UU l3} {C : UU l4}
  (f : A → X) (g : B → X) (h : C → X) (i : A → B) (j : B → C)
  where

  concat-coherence-triangle-maps :
    coherence-triangle-maps f g i →
    coherence-triangle-maps g h j →
    coherence-triangle-maps f h (j ∘ i)
  concat-coherence-triangle-maps H K =
    H ∙h (K ·r i)

Properties

If the top map has a section, then the reversed triangle with the section on top commutes

If t : B → A is a section of the top map h, then the triangle

       t
  B ------> A
   \       /
   g\     /f
     \   /
      ∨ ∨
       X

commutes.

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  (f : A → X) (g : B → X) (h : A → B) (H : coherence-triangle-maps f g h)
  (t : section h)
  where

  inv-triangle-section : coherence-triangle-maps' g f (map-section h t)
  inv-triangle-section =
    (H ·r map-section h t) ∙h (g ·l is-section-map-section h t)

  triangle-section : coherence-triangle-maps g f (map-section h t)
  triangle-section = inv-htpy inv-triangle-section

If the right map has a retraction, then the reversed triangle with the retraction on the right commutes

If r : X → B is a retraction of the right map g in a triangle f ~ g ∘ h, then the triangle

       f
  A ------> X
   \       /
   h\     /r
     \   /
      ∨ ∨
       B

commutes.

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  (f : A → X) (g : B → X) (h : A → B) (H : coherence-triangle-maps f g h)
  (r : retraction g)
  where

  inv-triangle-retraction : coherence-triangle-maps' h (map-retraction g r) f
  inv-triangle-retraction =
    (map-retraction g r ·l H) ∙h (is-retraction-map-retraction g r ·r h)

  triangle-retraction : coherence-triangle-maps h (map-retraction g r) f
  triangle-retraction = inv-htpy inv-triangle-retraction

Recent changes