Morphisms of arrows

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

Created on 2023-11-09.
Last modified on 2024-04-25.

module foundation.morphisms-arrows where
Imports
open import foundation.cones-over-cospan-diagrams
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.commuting-squares-of-maps
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.postcomposition-functions
open import foundation-core.precomposition-functions

Idea

A morphism of arrows from a function f : A → B to a function g : X → Y is a triple (i , j , H) consisting of maps i : A → X and j : B → Y and a homotopy H : j ∘ f ~ g ∘ i witnessing that the square

        i
    A -----> X
    |        |
  f |        | g
    ∨        ∨
    B -----> Y
        j

commutes. Morphisms of arrows can be composed horizontally or vertically by pasting of squares.

Definitions

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)
  where

  coherence-hom-arrow : (A  X)  (B  Y)  UU (l1  l4)
  coherence-hom-arrow i = coherence-square-maps i f g

  hom-arrow : UU (l1  l2  l3  l4)
  hom-arrow = Σ (A  X)  i  Σ (B  Y) (coherence-hom-arrow i))

  map-domain-hom-arrow : hom-arrow  A  X
  map-domain-hom-arrow = pr1

  map-codomain-hom-arrow : hom-arrow  B  Y
  map-codomain-hom-arrow = pr1  pr2

  coh-hom-arrow :
    (h : hom-arrow) 
    coherence-hom-arrow (map-domain-hom-arrow h) (map-codomain-hom-arrow h)
  coh-hom-arrow = pr2  pr2

Operations

The identity morphism of arrows

The identity morphism of arrows is defined as

        id
    A -----> A
    |        |
  f |        | f
    ∨        ∨
    B -----> B
        id

where the homotopy id ∘ f ~ f ∘ id is the reflexivity homotopy.

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

  id-hom-arrow : hom-arrow f f
  pr1 id-hom-arrow = id
  pr1 (pr2 id-hom-arrow) = id
  pr2 (pr2 id-hom-arrow) = refl-htpy

Composition of morphisms of arrows

Consider a commuting diagram of the form

        α₀       β₀
    A -----> X -----> U
    |        |        |
  f |   α  g |   β    | h
    ∨        ∨        ∨
    B -----> Y -----> V.
        α₁       β₁

Then the outer rectangle commutes by horizontal pasting of commuting squares of maps. The composition of β : g → h with α : f → g is therefore defined to be

        β₀ ∘ α₀
    A ----------> U
    |             |
  f |    α □ β    | h
    ∨             ∨
    B ----------> V.
        β₁ ∘ α₁

Note. Associativity and the unit laws for composition of morphisms of arrows are proven in Homotopies of morphisms of arrows.

module _
  {l1 l2 l3 l4 l5 l6 : Level}
  {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {U : UU l5} {V : UU l6}
  (f : A  B) (g : X  Y) (h : U  V) (b : hom-arrow g h) (a : hom-arrow f g)
  where

  map-domain-comp-hom-arrow : A  U
  map-domain-comp-hom-arrow =
    map-domain-hom-arrow g h b  map-domain-hom-arrow f g a

  map-codomain-comp-hom-arrow : B  V
  map-codomain-comp-hom-arrow =
    map-codomain-hom-arrow g h b  map-codomain-hom-arrow f g a

  coh-comp-hom-arrow :
    coherence-hom-arrow f h
      ( map-domain-comp-hom-arrow)
      ( map-codomain-comp-hom-arrow)
  coh-comp-hom-arrow =
    pasting-horizontal-coherence-square-maps
      ( map-domain-hom-arrow f g a)
      ( map-domain-hom-arrow g h b)
      ( f)
      ( g)
      ( h)
      ( map-codomain-hom-arrow f g a)
      ( map-codomain-hom-arrow g h b)
      ( coh-hom-arrow f g a)
      ( coh-hom-arrow g h b)

  comp-hom-arrow : hom-arrow f h
  pr1 comp-hom-arrow =
    map-domain-comp-hom-arrow
  pr1 (pr2 comp-hom-arrow) =
    map-codomain-comp-hom-arrow
  pr2 (pr2 comp-hom-arrow) =
    coh-comp-hom-arrow

Transposing morphisms of arrows

The transposition of a morphism of arrows

        i
    A -----> X
    |        |
  f |        | g
    ∨        ∨
    B -----> Y
        j

is the morphism of arrows

        f
    A -----> B
    |        |
  i |        | j
    ∨        ∨
    X -----> Y.
        g
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)
  where

  map-domain-transpose-hom-arrow : A  B
  map-domain-transpose-hom-arrow = f

  map-codomain-transpose-hom-arrow : X  Y
  map-codomain-transpose-hom-arrow = g

  coh-transpose-hom-arrow :
    coherence-hom-arrow
      ( map-domain-hom-arrow f g α)
      ( map-codomain-hom-arrow f g α)
      ( map-domain-transpose-hom-arrow)
      ( map-codomain-transpose-hom-arrow)
  coh-transpose-hom-arrow =
    inv-htpy (coh-hom-arrow f g α)

  transpose-hom-arrow :
    hom-arrow (map-domain-hom-arrow f g α) (map-codomain-hom-arrow f g α)
  pr1 transpose-hom-arrow = map-domain-transpose-hom-arrow
  pr1 (pr2 transpose-hom-arrow) = map-codomain-transpose-hom-arrow
  pr2 (pr2 transpose-hom-arrow) = coh-transpose-hom-arrow

Morphisms of arrows obtained from cones over cospans

module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
  (f : A  X) (g : B  X) (c : cone f g C)
  where

  hom-arrow-cone : hom-arrow (vertical-map-cone f g c) g
  pr1 hom-arrow-cone = horizontal-map-cone f g c
  pr1 (pr2 hom-arrow-cone) = f
  pr2 (pr2 hom-arrow-cone) = coherence-square-cone f g c

  hom-arrow-cone' : hom-arrow (horizontal-map-cone f g c) f
  hom-arrow-cone' =
    transpose-hom-arrow (vertical-map-cone f g c) g hom-arrow-cone

Cones over cospans obtained from 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) (h : hom-arrow f g)
  where

  cone-hom-arrow : cone (map-codomain-hom-arrow f g h) g A
  pr1 cone-hom-arrow = f
  pr1 (pr2 cone-hom-arrow) = map-domain-hom-arrow f g h
  pr2 (pr2 cone-hom-arrow) = coh-hom-arrow f g h

Morphisms of arrows are preserved under homotopies

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

  hom-arrow-htpy-source :
    {f f' : A  B} (F' : f' ~ f) (g : X  Y) 
    hom-arrow f g  hom-arrow f' g
  hom-arrow-htpy-source F' g (i , j , H) = (i , j , (j ·l F') ∙h H)

  hom-arrow-htpy-target :
    (f : A  B) {g g' : X  Y} (G : g ~ g') 
    hom-arrow f g  hom-arrow f g'
  hom-arrow-htpy-target f G (i , j , H) = (i , j , H ∙h (G ·r i))

  hom-arrow-htpy :
    {f f' : A  B} (F' : f' ~ f) {g g' : X  Y} (G : g ~ g') 
    hom-arrow f g  hom-arrow f' g'
  hom-arrow-htpy F' G (i , j , H) = (i , j , (j ·l F') ∙h H ∙h (G ·r i))

Dependent products of morphisms of arrows

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

  Π-hom-arrow : hom-arrow (map-Π f) (map-Π g)
  pr1 Π-hom-arrow =
    map-Π  i  map-domain-hom-arrow (f i) (g i) (α i))
  pr1 (pr2 Π-hom-arrow) =
    map-Π  i  map-codomain-hom-arrow (f i) (g i) (α i))
  pr2 (pr2 Π-hom-arrow) =
    htpy-map-Π  i  coh-hom-arrow (f i) (g i) (α i))

Morphisms of arrows give morphisms of precomposition arrows

A morphism of arrows α : f → g gives a morphism of precomposition arrows (-)^α : (–)^g → (–)^f.

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)
  where

  precomp-hom-arrow :
    {l : Level} (S : UU l)  hom-arrow (precomp g S) (precomp f S)
  pr1 (precomp-hom-arrow S) =
    precomp (map-codomain-hom-arrow f g α) S
  pr1 (pr2 (precomp-hom-arrow S)) =
    precomp (map-domain-hom-arrow f g α) S
  pr2 (pr2 (precomp-hom-arrow S)) h =
    inv (eq-htpy (h ·l coh-hom-arrow f g α))

Morphisms of arrows give morphisms of postcomposition arrows

A morphism of arrows α : f → g gives a morphism of postcomposition arrows α^(-) : f^(-) → g^(-).

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)
  where

  postcomp-hom-arrow :
    {l : Level} (S : UU l)  hom-arrow (postcomp S f) (postcomp S g)
  pr1 (postcomp-hom-arrow S) =
    postcomp S (map-domain-hom-arrow f g α)
  pr1 (pr2 (postcomp-hom-arrow S)) =
    postcomp S (map-codomain-hom-arrow f g α)
  pr2 (pr2 (postcomp-hom-arrow S)) h =
    eq-htpy (coh-hom-arrow f g α ·r h)

See also

Recent changes