Equivalences of pointed arrows

Content created by Egbert Rijke.

Created on 2024-03-13.

module structured-types.equivalences-pointed-arrows where

Imports
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.equivalences-arrows
open import foundation.function-types
open import foundation.identity-types
open import foundation.universe-levels

open import structured-types.commuting-squares-of-pointed-maps
open import structured-types.pointed-equivalences
open import structured-types.pointed-homotopies
open import structured-types.pointed-maps
open import structured-types.pointed-types


Idea

An equivalence 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 equivalences 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
∨        ∨
B -----> Y
j


Definitions

Equivalences 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-equiv-pointed-arrow :
(A ≃∗ X) → (B ≃∗ Y) → UU (l1 ⊔ l4)
coherence-equiv-pointed-arrow i j =
coherence-square-pointed-maps
( pointed-map-pointed-equiv i)
( f)
( g)
( pointed-map-pointed-equiv j)

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

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} (e : equiv-pointed-arrow f g)
where

pointed-equiv-domain-equiv-pointed-arrow : A ≃∗ X
pointed-equiv-domain-equiv-pointed-arrow = pr1 e

equiv-domain-equiv-pointed-arrow : type-Pointed-Type A ≃ type-Pointed-Type X
equiv-domain-equiv-pointed-arrow =
equiv-pointed-equiv pointed-equiv-domain-equiv-pointed-arrow

pointed-map-domain-equiv-pointed-arrow : A →∗ X
pointed-map-domain-equiv-pointed-arrow =
pointed-map-pointed-equiv pointed-equiv-domain-equiv-pointed-arrow

map-domain-equiv-pointed-arrow : type-Pointed-Type A → type-Pointed-Type X
map-domain-equiv-pointed-arrow =
map-pointed-equiv pointed-equiv-domain-equiv-pointed-arrow

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

pointed-equiv-codomain-equiv-pointed-arrow : B ≃∗ Y
pointed-equiv-codomain-equiv-pointed-arrow = pr1 (pr2 e)

equiv-codomain-equiv-pointed-arrow : type-Pointed-Type B ≃ type-Pointed-Type Y
equiv-codomain-equiv-pointed-arrow =
equiv-pointed-equiv pointed-equiv-codomain-equiv-pointed-arrow

map-codomain-equiv-pointed-arrow : type-Pointed-Type B → type-Pointed-Type Y
map-codomain-equiv-pointed-arrow =
map-pointed-equiv pointed-equiv-codomain-equiv-pointed-arrow

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

coh-equiv-pointed-arrow :
coherence-equiv-pointed-arrow
( f)
( g)
( pointed-equiv-domain-equiv-pointed-arrow)
( pointed-equiv-codomain-equiv-pointed-arrow)
coh-equiv-pointed-arrow = pr2 (pr2 e)

htpy-coh-equiv-pointed-arrow :
coherence-equiv-arrow
( map-pointed-map f)
( map-pointed-map g)
( equiv-domain-equiv-pointed-arrow)
( equiv-codomain-equiv-pointed-arrow)
htpy-coh-equiv-pointed-arrow = htpy-pointed-htpy coh-equiv-pointed-arrow