Higher homotopies of morphisms of arrows

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-02-06.
Last modified on 2024-03-13.

module foundation.higher-homotopies-morphisms-arrows where
Imports
open import foundation.action-on-identifications-functions
open import foundation.commuting-squares-of-homotopies
open import foundation.commuting-squares-of-identifications
open import foundation.dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies-morphisms-arrows
open import foundation.homotopy-induction
open import foundation.morphisms-arrows
open import foundation.path-algebra
open import foundation.structure-identity-principle
open import foundation.torsorial-type-families
open import foundation.universe-levels
open import foundation.whiskering-higher-homotopies-composition
open import foundation.whiskering-homotopies-concatenation
open import foundation.whiskering-identifications-concatenation

open import foundation-core.equivalences
open import foundation-core.homotopies
open import foundation-core.identity-types

Idea

Consider two morphisms of arrows α := (i , j , H) and α' := (i' , j' , H') and two homotopies of morphisms of arrows β := (I , J , K) and β' : (I' , J' , K') between them. A 2-homotopy of morphisms of arrows is a triple (γ₀, γ₁ , γ₂) consisting of homotopies

  γ₀ : I ~ I'
  γ₁ : J ~ J'

and a homotopy witnessing that the square of homotopies

                 left-whisker-concat-htpy H (g · γ₀)
  H ∙ (g ·l I) ---------------------------------------> H ∙ (g · I')
       |                                                     |
     K |                                                     | K'
       ∨                                                     ∨
  (J · f) ∙ H' ---------------------------------------> (J' · f) ∙ H'
                right-whisker-concat-htpy (γ₁ · f) H'

commutes.

Definitions

Homotopies of homotopies of arrows

module _
  {l1 l2 l3 l4 : Level}
  {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
  (f : A  B) (g : X  Y) (α α' : hom-arrow f g)
  (β β' : htpy-hom-arrow f g α α')
  where

  coherence-htpy-htpy-hom-arrow :
    htpy-domain-htpy-hom-arrow f g α α' β ~
    htpy-domain-htpy-hom-arrow f g α α' β' 
    htpy-codomain-htpy-hom-arrow f g α α' β ~
    htpy-codomain-htpy-hom-arrow f g α α' β'  UU (l1  l4)
  coherence-htpy-htpy-hom-arrow γ₀ γ₁ =
    coherence-square-homotopies
      ( left-whisker-concat-htpy
        ( coh-hom-arrow f g α)
        ( left-whisker-comp² g γ₀))
      ( coh-htpy-hom-arrow f g α α' β)
      ( coh-htpy-hom-arrow f g α α' β')
      ( right-whisker-concat-htpy
        ( right-whisker-comp² γ₁ f)
        ( coh-hom-arrow f g α'))

  htpy-htpy-hom-arrow : UU (l1  l2  l3  l4)
  htpy-htpy-hom-arrow =
    Σ ( htpy-domain-htpy-hom-arrow f g α α' β ~
        htpy-domain-htpy-hom-arrow f g α α' β')
      ( λ γ₀ 
        Σ ( htpy-codomain-htpy-hom-arrow f g α α' β ~
            htpy-codomain-htpy-hom-arrow f g α α' β')
          ( coherence-htpy-htpy-hom-arrow γ₀))

  module _
    (γ : htpy-htpy-hom-arrow)
    where

    htpy-domain-htpy-htpy-hom-arrow :
      htpy-domain-htpy-hom-arrow f g α α' β ~
      htpy-domain-htpy-hom-arrow f g α α' β'
    htpy-domain-htpy-htpy-hom-arrow = pr1 γ

    htpy-codomain-htpy-htpy-hom-arrow :
      htpy-codomain-htpy-hom-arrow f g α α' β ~
      htpy-codomain-htpy-hom-arrow f g α α' β'
    htpy-codomain-htpy-htpy-hom-arrow = pr1 (pr2 γ)

    coh-htpy-htpy-hom-arrow :
      coherence-htpy-htpy-hom-arrow
        ( htpy-domain-htpy-htpy-hom-arrow)
        ( htpy-codomain-htpy-htpy-hom-arrow)
    coh-htpy-htpy-hom-arrow = pr2 (pr2 γ)

The reflexivity homotopy of homotopies of morphisms of arrows

module _
  {l1 l2 l3 l4 : Level}
  {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
  (f : A  B) (g : X  Y) (α α' : hom-arrow f g)
  (β : htpy-hom-arrow f g α α')
  where

  htpy-domain-refl-htpy-htpy-hom-arrow :
    htpy-domain-htpy-hom-arrow f g α α' β ~
    htpy-domain-htpy-hom-arrow f g α α' β
  htpy-domain-refl-htpy-htpy-hom-arrow = refl-htpy

  htpy-codomain-refl-htpy-htpy-hom-arrow :
    htpy-codomain-htpy-hom-arrow f g α α' β ~
    htpy-codomain-htpy-hom-arrow f g α α' β
  htpy-codomain-refl-htpy-htpy-hom-arrow = refl-htpy

  coh-refl-htpy-htpy-hom-arrow :
    coherence-htpy-htpy-hom-arrow f g α α' β β
      ( htpy-domain-refl-htpy-htpy-hom-arrow)
      ( htpy-codomain-refl-htpy-htpy-hom-arrow)
  coh-refl-htpy-htpy-hom-arrow = right-unit-htpy

  refl-htpy-htpy-hom-arrow : htpy-htpy-hom-arrow f g α α' β β
  pr1 refl-htpy-htpy-hom-arrow = htpy-domain-refl-htpy-htpy-hom-arrow
  pr1 (pr2 refl-htpy-htpy-hom-arrow) = htpy-codomain-refl-htpy-htpy-hom-arrow
  pr2 (pr2 refl-htpy-htpy-hom-arrow) = coh-refl-htpy-htpy-hom-arrow

Properties

Homotopies of homotopies of morphisms of arrows characterize equality of homotopies of morphisms of arrows

module _
  {l1 l2 l3 l4 : Level}
  {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
  (f : A  B) (g : X  Y) (α α' : hom-arrow f g)
  (β : htpy-hom-arrow f g α α')
  where

  htpy-eq-htpy-hom-arrow :
    (β' : htpy-hom-arrow f g α α')  β  β'  htpy-htpy-hom-arrow f g α α' β β'
  htpy-eq-htpy-hom-arrow .β refl = refl-htpy-htpy-hom-arrow f g α α' β

  is-torsorial-htpy-htpy-hom-arrow :
    is-torsorial (htpy-htpy-hom-arrow f g α α' β)
  is-torsorial-htpy-htpy-hom-arrow =
    is-torsorial-Eq-structure
      ( is-torsorial-htpy _)
      ( htpy-domain-htpy-hom-arrow f g α α' β , refl-htpy)
      ( is-torsorial-Eq-structure
        ( is-torsorial-htpy _)
        ( htpy-codomain-htpy-hom-arrow f g α α' β , refl-htpy)
        ( is-torsorial-htpy _))

  is-equiv-htpy-eq-htpy-hom-arrow :
    (β' : htpy-hom-arrow f g α α')  is-equiv (htpy-eq-htpy-hom-arrow β')
  is-equiv-htpy-eq-htpy-hom-arrow =
    fundamental-theorem-id
      ( is-torsorial-htpy-htpy-hom-arrow)
      ( htpy-eq-htpy-hom-arrow)

  extensionality-htpy-hom-arrow :
    (β' : htpy-hom-arrow f g α α') 
    (β  β')  htpy-htpy-hom-arrow f g α α' β β'
  pr1 (extensionality-htpy-hom-arrow β') = htpy-eq-htpy-hom-arrow β'
  pr2 (extensionality-htpy-hom-arrow β') = is-equiv-htpy-eq-htpy-hom-arrow β'

  eq-htpy-htpy-hom-arrow :
    (β' : htpy-hom-arrow f g α α') 
    htpy-htpy-hom-arrow f g α α' β β'  β  β'
  eq-htpy-htpy-hom-arrow β' = map-inv-equiv (extensionality-htpy-hom-arrow β')

The left unit law for concatenation of homotopies of morphisms of arrows

module _
  {l1 l2 l3 l4 : Level}
  {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
  (f : A  B) (g : X  Y) (α α' : hom-arrow f g)
  (β : htpy-hom-arrow f g α α')
  where

  htpy-domain-left-unit-law-concat-htpy-hom-arrow :
    htpy-domain-concat-htpy-hom-arrow f g α α α' (refl-htpy-hom-arrow f g α) β ~
    htpy-domain-htpy-hom-arrow f g α α' β
  htpy-domain-left-unit-law-concat-htpy-hom-arrow = refl-htpy

  htpy-codomain-left-unit-law-concat-htpy-hom-arrow :
    htpy-codomain-concat-htpy-hom-arrow f g α α α'
      ( refl-htpy-hom-arrow f g α)
      ( β) ~
    htpy-codomain-htpy-hom-arrow f g α α' β
  htpy-codomain-left-unit-law-concat-htpy-hom-arrow = refl-htpy

  coh-left-unit-law-concat-htpy-hom-arrow :
    coherence-htpy-htpy-hom-arrow f g α α'
      ( concat-htpy-hom-arrow f g α α α' (refl-htpy-hom-arrow f g α) β)
      ( β)
      ( htpy-domain-left-unit-law-concat-htpy-hom-arrow)
      ( htpy-codomain-left-unit-law-concat-htpy-hom-arrow)
  coh-left-unit-law-concat-htpy-hom-arrow a =
    ( right-unit) 
    ( right-whisker-concat
      ( right-whisker-concat-horizontal-refl-coherence-square-identifications
        ( coh-hom-arrow f g α a)
        ( ap g (htpy-domain-htpy-hom-arrow f g α α' β a)))
      ( coh-htpy-hom-arrow f g α α' β a))

  left-unit-law-concat-htpy-hom-arrow :
    htpy-htpy-hom-arrow f g α α'
      ( concat-htpy-hom-arrow f g α α α' (refl-htpy-hom-arrow f g α) β)
      ( β)
  pr1 left-unit-law-concat-htpy-hom-arrow =
    htpy-domain-left-unit-law-concat-htpy-hom-arrow
  pr1 (pr2 left-unit-law-concat-htpy-hom-arrow) =
    htpy-codomain-left-unit-law-concat-htpy-hom-arrow
  pr2 (pr2 left-unit-law-concat-htpy-hom-arrow) =
    coh-left-unit-law-concat-htpy-hom-arrow

The right unit law for concatenation of morphisms of arrows

module _
  {l1 l2 l3 l4 : Level}
  {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
  (f : A  B) (g : X  Y) (α α' : hom-arrow f g)
  (β : htpy-hom-arrow f g α α')
  where

  htpy-domain-right-unit-law-concat-htpy-hom-arrow :
    htpy-domain-concat-htpy-hom-arrow f g α α' α' β
      ( refl-htpy-hom-arrow f g α') ~
    htpy-domain-htpy-hom-arrow f g α α' β
  htpy-domain-right-unit-law-concat-htpy-hom-arrow = right-unit-htpy

  htpy-codomain-right-unit-law-concat-htpy-hom-arrow :
    htpy-codomain-concat-htpy-hom-arrow f g α α' α' β
      ( refl-htpy-hom-arrow f g α') ~
    htpy-codomain-htpy-hom-arrow f g α α' β
  htpy-codomain-right-unit-law-concat-htpy-hom-arrow = right-unit-htpy

  coh-right-unit-law-concat-htpy-hom-arrow :
    coherence-htpy-htpy-hom-arrow f g α α'
      ( concat-htpy-hom-arrow f g α α' α' β (refl-htpy-hom-arrow f g α'))
      ( β)
      ( htpy-domain-right-unit-law-concat-htpy-hom-arrow)
      ( htpy-codomain-right-unit-law-concat-htpy-hom-arrow)
  coh-right-unit-law-concat-htpy-hom-arrow a =
    ( assoc
      ( left-whisker-concat (coh-hom-arrow f g α a) (ap-concat g _ refl))
      ( _)
      ( right-whisker-concat right-unit (coh-hom-arrow f g α' a))) 
    ( horizontal-concat-Id²
      ( ( ap
          ( left-whisker-concat (coh-hom-arrow f g α a))
          ( compute-right-refl-ap-concat g
            ( htpy-domain-htpy-hom-arrow f g α α' β a))) 
        ( distributive-left-whisker-concat-concat
          ( coh-hom-arrow f g α a)
          ( ap (ap g) right-unit)
          ( inv right-unit)))
      ( right-unit-law-horizontal-pasting-coherence-square-identifications
        ( htpy-codomain-htpy-hom-arrow f g α α' β (f a))
        ( coh-hom-arrow f g α a)
        ( coh-hom-arrow f g α' a)
        ( ap g (htpy-domain-htpy-hom-arrow f g α α' β a))
        ( coh-htpy-hom-arrow f g α α' β a)) 
      ( unsplice-concat'
        ( left-whisker-concat (coh-hom-arrow f g α a) (ap (ap g) right-unit))
        ( compute-inv-left-whisker-concat (coh-hom-arrow f g α a) right-unit)
        ( coh-htpy-hom-arrow f g α α' β a)))

  right-unit-law-concat-htpy-hom-arrow :
    htpy-htpy-hom-arrow f g α α'
      ( concat-htpy-hom-arrow f g α α' α' β (refl-htpy-hom-arrow f g α'))
      ( β)
  pr1 right-unit-law-concat-htpy-hom-arrow =
    htpy-domain-right-unit-law-concat-htpy-hom-arrow
  pr1 (pr2 right-unit-law-concat-htpy-hom-arrow) =
    htpy-codomain-right-unit-law-concat-htpy-hom-arrow
  pr2 (pr2 right-unit-law-concat-htpy-hom-arrow) =
    coh-right-unit-law-concat-htpy-hom-arrow

Recent changes