Morphisms of twisted pointed arrows

Content created by Egbert Rijke.

Created on 2024-03-13.
Last modified on 2024-04-25.

module structured-types.morphisms-twisted-pointed-arrows where
Imports 
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.identity-types
open import foundation.morphisms-twisted-arrows
open import foundation.universe-levels

open import structured-types.pointed-homotopies
open import structured-types.pointed-maps
open import structured-types.pointed-types

A morphism of twisted 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 : X →∗ A and j : B →∗ Y and a pointed homotopy H : j ∘∗ f ~∗ g ∘∗ i witnessing that the diagram

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

commutes.

Definitions

Morphisms of twisted 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-twisted-pointed-arrow :
    (X →∗ A) → (B →∗ Y) → UU (l3 ⊔ l4)
  coherence-hom-twisted-pointed-arrow i j = ((j ∘∗ f) ∘∗ i) ~∗ g

  hom-twisted-pointed-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  hom-twisted-pointed-arrow =
    Σ (X →∗ A) (λ i → Σ (B →∗ Y) (coherence-hom-twisted-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} (h : hom-twisted-pointed-arrow f g)
  where

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

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

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

  pointed-map-codomain-hom-twisted-pointed-arrow : B →∗ Y
  pointed-map-codomain-hom-twisted-pointed-arrow = pr1 (pr2 h)

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

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

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

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

Recent changes