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-10-27.
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 id-hom-arrow = (id , id , 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
- Equivalences of arrows
- Morphisms of twisted arrows.
- Fibered maps for the same concept under a different name.
- The pullback-hom is an operation that returns a morphism of arrows from a diagonal map.
- Homotopies of morphisms of arrows
Recent changes
- 2024-10-27. Fredrik Bakke. Functoriality of morphisms of arrows (#1130).
- 2024-04-25. Fredrik Bakke. chore: Fix arrowheads in character diagrams (#1124).
- 2024-03-22. Fredrik Bakke. Additions to cartesian morphisms (#1087).
- 2024-02-06. Egbert Rijke and Fredrik Bakke. Refactor files about identity types and homotopies (#1014).
- 2024-01-28. Egbert Rijke. Span diagrams (#1007).