# Morphisms of pointed arrows

Content created by Egbert Rijke.

Created on 2024-03-13.

module structured-types.morphisms-pointed-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.commuting-triangles-of-identifications
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.functoriality-dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopy-induction
open import foundation.morphisms-arrows
open import foundation.path-algebra
open import foundation.structure-identity-principle
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.commuting-squares-of-maps
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.torsorial-type-families

open import structured-types.commuting-squares-of-pointed-homotopies
open import structured-types.commuting-squares-of-pointed-maps
open import structured-types.pointed-2-homotopies
open import structured-types.pointed-homotopies
open import structured-types.pointed-maps
open import structured-types.pointed-types
open import structured-types.whiskering-pointed-2-homotopies-concatenation
open import structured-types.whiskering-pointed-homotopies-composition


## Idea

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

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


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

## Definitions

### Morphisms of pointed arrows

module _
{l1 l2 l3 l4 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2}
{X : Pointed-Type l3} {Y : Pointed-Type l4}
(f : A →∗ B) (g : X →∗ Y)
where

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

hom-pointed-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
hom-pointed-arrow =
Σ (A →∗ X) (λ i → Σ (B →∗ Y) (coherence-hom-pointed-arrow i))

pointed-map-domain-hom-pointed-arrow :
hom-pointed-arrow → A →∗ X
pointed-map-domain-hom-pointed-arrow = pr1

map-domain-hom-pointed-arrow :
hom-pointed-arrow → type-Pointed-Type A → type-Pointed-Type X
map-domain-hom-pointed-arrow h =
map-pointed-map (pointed-map-domain-hom-pointed-arrow h)

preserves-point-map-domain-hom-pointed-arrow :
(h : hom-pointed-arrow) →
map-domain-hom-pointed-arrow h (point-Pointed-Type A) ＝
point-Pointed-Type X
preserves-point-map-domain-hom-pointed-arrow h =
preserves-point-pointed-map (pointed-map-domain-hom-pointed-arrow h)

pointed-map-codomain-hom-pointed-arrow :
hom-pointed-arrow → B →∗ Y
pointed-map-codomain-hom-pointed-arrow = pr1 ∘ pr2

map-codomain-hom-pointed-arrow :
hom-pointed-arrow → type-Pointed-Type B → type-Pointed-Type Y
map-codomain-hom-pointed-arrow h =
map-pointed-map (pointed-map-codomain-hom-pointed-arrow h)

preserves-point-map-codomain-hom-pointed-arrow :
(h : hom-pointed-arrow) →
map-codomain-hom-pointed-arrow h (point-Pointed-Type B) ＝
point-Pointed-Type Y
preserves-point-map-codomain-hom-pointed-arrow h =
preserves-point-pointed-map (pointed-map-codomain-hom-pointed-arrow h)

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

htpy-coh-hom-pointed-arrow :
(h : hom-pointed-arrow) →
coherence-hom-arrow
( map-pointed-map f)
( map-pointed-map g)
( map-domain-hom-pointed-arrow h)
( map-codomain-hom-pointed-arrow h)
htpy-coh-hom-pointed-arrow h =
htpy-pointed-htpy
( coh-hom-pointed-arrow h)


### Transposing morphisms of pointed arrows

The transposition of a morphism of pointed arrows

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


is the morphism of pointed arrows

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

module _
{l1 l2 l3 l4 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2}
{X : Pointed-Type l3} {Y : Pointed-Type l4}
(f : A →∗ B) (g : X →∗ Y) (α : hom-pointed-arrow f g)
where

pointed-map-domain-transpose-hom-pointed-arrow : A →∗ B
pointed-map-domain-transpose-hom-pointed-arrow = f

pointed-map-codomain-transpose-hom-pointed-arrow : X →∗ Y
pointed-map-codomain-transpose-hom-pointed-arrow = g

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

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


### The identity morphism of pointed arrows

The identity morphism of pointed arrows is defined as

        id
A -----> A
|        |
f |        | f
V        V
B -----> B
id


where the pointed homotopy id ∘∗ f ~∗ f ∘∗ id is the concatenation of the left unit law pointed homotopy and the inverse pointed homotopy of the right unit law pointed homotopy.

module _
{l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} {f : A →∗ B}
where

id-hom-pointed-arrow : hom-pointed-arrow f f
pr1 id-hom-pointed-arrow = id-pointed-map
pr1 (pr2 id-hom-pointed-arrow) = id-pointed-map
pr2 (pr2 id-hom-pointed-arrow) =
concat-pointed-htpy
( left-unit-law-comp-pointed-map f)
( inv-pointed-htpy (right-unit-law-comp-pointed-map f))


### Composition of morphisms of pointed 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 pointed maps. The composition of β : g → h with α : f → g is therefore defined to be

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

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

pointed-map-domain-comp-hom-pointed-arrow : A →∗ U
pointed-map-domain-comp-hom-pointed-arrow =
pointed-map-domain-hom-pointed-arrow g h b ∘∗
pointed-map-domain-hom-pointed-arrow f g a

map-domain-comp-hom-pointed-arrow :
type-Pointed-Type A → type-Pointed-Type U
map-domain-comp-hom-pointed-arrow =
map-pointed-map pointed-map-domain-comp-hom-pointed-arrow

preserves-point-map-domain-comp-hom-pointed-arrow :
map-domain-comp-hom-pointed-arrow (point-Pointed-Type A) ＝
point-Pointed-Type U
preserves-point-map-domain-comp-hom-pointed-arrow =
preserves-point-pointed-map pointed-map-domain-comp-hom-pointed-arrow

pointed-map-codomain-comp-hom-pointed-arrow : B →∗ V
pointed-map-codomain-comp-hom-pointed-arrow =
pointed-map-codomain-hom-pointed-arrow g h b ∘∗
pointed-map-codomain-hom-pointed-arrow f g a

map-codomain-comp-hom-pointed-arrow :
type-Pointed-Type B → type-Pointed-Type V
map-codomain-comp-hom-pointed-arrow =
map-pointed-map pointed-map-codomain-comp-hom-pointed-arrow

preserves-point-map-codomain-comp-hom-pointed-arrow :
map-codomain-comp-hom-pointed-arrow (point-Pointed-Type B) ＝
point-Pointed-Type V
preserves-point-map-codomain-comp-hom-pointed-arrow =
preserves-point-pointed-map pointed-map-codomain-comp-hom-pointed-arrow

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

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


### Homotopies of morphisms of pointed arrows

A homotopy of morphisms of pointed arrows from (i , j , H) to (i' , j' , H') is a triple (I , J , K) consisting of pointed homotopies I : i ~∗ i' and J : j ~∗ j' and a pointed 2-homotopy K witnessing that the square of pointed homotopies

            J ·r f
(j ∘∗ f) --------> (j' ∘∗ f)
|                   |
H |                   | H'
∨                   ∨
(g ∘∗ i) ---------> (g ∘∗ i')
g ·l I


commutes.

module _
{l1 l2 l3 l4 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2}
{X : Pointed-Type l3} {Y : Pointed-Type l4}
(f : A →∗ B) (g : X →∗ Y) (α : hom-pointed-arrow f g)
where

coherence-htpy-hom-pointed-arrow :
(β : hom-pointed-arrow f g)
(I :
pointed-map-domain-hom-pointed-arrow f g α ~∗
pointed-map-domain-hom-pointed-arrow f g β)
(J :
pointed-map-codomain-hom-pointed-arrow f g α ~∗
pointed-map-codomain-hom-pointed-arrow f g β) →
UU (l1 ⊔ l4)
coherence-htpy-hom-pointed-arrow β I J =
coherence-square-pointed-homotopies
( right-whisker-comp-pointed-htpy _ _ J f)
( coh-hom-pointed-arrow f g α)
( coh-hom-pointed-arrow f g β)
( left-whisker-comp-pointed-htpy g _ _ I)

htpy-hom-pointed-arrow :
(β : hom-pointed-arrow f g) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
htpy-hom-pointed-arrow β =
Σ ( pointed-map-domain-hom-pointed-arrow f g α ~∗
pointed-map-domain-hom-pointed-arrow f g β)
( λ I →
Σ ( pointed-map-codomain-hom-pointed-arrow f g α ~∗
pointed-map-codomain-hom-pointed-arrow f g β)
( coherence-htpy-hom-pointed-arrow β I))

module _
(β : hom-pointed-arrow f g) (η : htpy-hom-pointed-arrow β)
where

pointed-htpy-domain-htpy-hom-pointed-arrow :
pointed-map-domain-hom-pointed-arrow f g α ~∗
pointed-map-domain-hom-pointed-arrow f g β
pointed-htpy-domain-htpy-hom-pointed-arrow = pr1 η

pointed-htpy-codomain-htpy-hom-pointed-arrow :
pointed-map-codomain-hom-pointed-arrow f g α ~∗
pointed-map-codomain-hom-pointed-arrow f g β
pointed-htpy-codomain-htpy-hom-pointed-arrow = pr1 (pr2 η)

coh-htpy-hom-pointed-arrow :
coherence-htpy-hom-pointed-arrow β
( pointed-htpy-domain-htpy-hom-pointed-arrow)
( pointed-htpy-codomain-htpy-hom-pointed-arrow)
coh-htpy-hom-pointed-arrow = pr2 (pr2 η)


### The reflexive homotopy of pointed arrows

Consider a morphism of pointed arrows

                α₀
A -----> X
|        |
(f₀ , f₁) |   α₂   | (g₀ , g₁)
∨        ∨
B -----> Y
α₁


from f : A →∗ B to g : X →∗ Y. The reflexive homotopy of morphisms of arrows r := (r₀ , r₁ , r₂) on α := (α₀ , α₁ , α₂) is given by

  r₀ := refl-pointed-htpy : α₀ ~∗ α₀
r₁ := refl-pointed-htpy : α₁ ~∗ α₁


and a pointed 2-homotopy r₂ witnessing that the square of pointed homotopies

            r₁ ·r f
(α₁ ∘ f) --------> (α₁ ∘ f)
|                  |
α₂ |                  | α₂
V                  V
(g ∘ α₀) --------> (g ∘ α₀)
g ·l r₀


commutes. Note that r₁ ·r f ~∗ refl-pointed-htpy and g ·l r₀ ≐ refl-pointed-htpy. By whiskering of pointed 2-homotopies with respect to concatenation it follows that

  (r₁ ·r f) ∙h α₂ ~∗ refl-pointed-htpy ∙h α₂ ~∗ α₂.

module _
{l1 l2 l3 l4 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2}
{X : Pointed-Type l3} {Y : Pointed-Type l4}
(f : A →∗ B) (g : X →∗ Y) (α : hom-pointed-arrow f g)
where

pointed-htpy-domain-refl-htpy-hom-pointed-arrow :
pointed-map-domain-hom-pointed-arrow f g α ~∗
pointed-map-domain-hom-pointed-arrow f g α
pointed-htpy-domain-refl-htpy-hom-pointed-arrow = refl-pointed-htpy _

pointed-htpy-codomain-refl-htpy-hom-pointed-arrow :
pointed-map-codomain-hom-pointed-arrow f g α ~∗
pointed-map-codomain-hom-pointed-arrow f g α
pointed-htpy-codomain-refl-htpy-hom-pointed-arrow = refl-pointed-htpy _

coh-refl-htpy-hom-pointed-arrow :
coherence-htpy-hom-pointed-arrow f g α α
( pointed-htpy-domain-refl-htpy-hom-pointed-arrow)
( pointed-htpy-codomain-refl-htpy-hom-pointed-arrow)
coh-refl-htpy-hom-pointed-arrow =
concat-pointed-2-htpy
( right-unit-law-concat-pointed-htpy (coh-hom-pointed-arrow f g α))
( inv-pointed-2-htpy
( concat-pointed-2-htpy
( right-whisker-concat-pointed-2-htpy
( right-whisker-comp-pointed-htpy
( pointed-map-codomain-hom-pointed-arrow f g α)
( pointed-map-codomain-hom-pointed-arrow f g α)
( pointed-htpy-codomain-refl-htpy-hom-pointed-arrow)
( f))
( refl-pointed-htpy _)
( compute-refl-right-whisker-comp-pointed-htpy
( pointed-map-codomain-hom-pointed-arrow f g α)
( f))
( coh-hom-pointed-arrow f g α))
( left-unit-law-concat-pointed-htpy (coh-hom-pointed-arrow f g α))))

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


### Characterization of the identity types of morphisms of pointed arrows

module _
{l1 l2 l3 l4 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2}
{X : Pointed-Type l3} {Y : Pointed-Type l4}
(f : A →∗ B) (g : X →∗ Y) (α : hom-pointed-arrow f g)
where

is-torsorial-htpy-hom-pointed-arrow :
is-torsorial (htpy-hom-pointed-arrow f g α)
is-torsorial-htpy-hom-pointed-arrow =
is-torsorial-Eq-structure
( is-torsorial-pointed-htpy _)
( pointed-map-domain-hom-pointed-arrow f g α , refl-pointed-htpy _)
( is-torsorial-Eq-structure
( is-torsorial-pointed-htpy _)
( pointed-map-codomain-hom-pointed-arrow f g α , refl-pointed-htpy _)
( is-contr-equiv' _
( equiv-tot
( λ H →
equiv-concat-pointed-2-htpy'
( inv-pointed-2-htpy
( concat-pointed-2-htpy
( right-whisker-concat-pointed-2-htpy _ _
( compute-refl-right-whisker-comp-pointed-htpy
( pointed-map-codomain-hom-pointed-arrow f g α)
( f))
( H))
( left-unit-law-concat-pointed-htpy H)))))
( is-torsorial-pointed-2-htpy
( concat-pointed-htpy
( coh-hom-pointed-arrow f g α)
( refl-pointed-htpy _)))))

htpy-eq-hom-pointed-arrow :
(β : hom-pointed-arrow f g) → α ＝ β → htpy-hom-pointed-arrow f g α β
htpy-eq-hom-pointed-arrow β refl = refl-htpy-hom-pointed-arrow f g α

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

extensionality-hom-pointed-arrow :
(β : hom-pointed-arrow f g) → (α ＝ β) ≃ htpy-hom-pointed-arrow f g α β
pr1 (extensionality-hom-pointed-arrow β) =
htpy-eq-hom-pointed-arrow β
pr2 (extensionality-hom-pointed-arrow β) =
is-equiv-htpy-eq-hom-pointed-arrow β

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