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-02-06.

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.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
    V        V
    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

Transposing morphisms of arrows

The transposition of a morphism of arrows

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

is the morphism of arrows

        f
    A -----> B
    |        |
  i |        | j
    V        V
    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

The identity morphism of arrows

The identity morphism of arrows is defined as

        id
    A -----> A
    |        |
  f |        | f
    V        V
    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
    V        V        V
    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
    V             V
    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

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

  hom-arrow-precomp-hom-arrow :
    {l : Level} (S : UU l)  hom-arrow (precomp g S) (precomp f S)
  pr1 (hom-arrow-precomp-hom-arrow S) =
    precomp (map-codomain-hom-arrow f g α) S
  pr1 (pr2 (hom-arrow-precomp-hom-arrow S)) =
    precomp (map-domain-hom-arrow f g α) S
  pr2 (pr2 (hom-arrow-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

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

See also

Recent changes