Morphisms of spans on families of types

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-01-28.
Last modified on 2024-02-06.

module foundation.morphisms-spans-families-of-types where
Imports 
open import foundation.commuting-triangles-of-homotopies
open import foundation.dependent-pair-types
open import foundation.equality-dependent-function-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopy-induction
open import foundation.spans-families-of-types
open import foundation.structure-identity-principle
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

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

Idea

Consider two spans 𝒮 := (S , f) and 𝒯 := (T , g) on a family of types A : I → 𝒰. A morphism from 𝒮 to 𝒯 consists of a map h : S → T and a homotopy witnessing that the triangle

        h
    S ----> T
     \     /
  f i \   / g i
       ∨ ∨
       A i

commutes for every i : I.

Definitions

Morphisms of spans on families of types

module _
  {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2}
  (𝒮 : span-type-family l3 A) (𝒯 : span-type-family l4 A)
  where

  hom-span-type-family : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  hom-span-type-family =
    Σ ( spanning-type-span-type-family 𝒮 →
        spanning-type-span-type-family 𝒯)
      ( λ h →
        (i : I) →
        coherence-triangle-maps
          ( map-span-type-family 𝒮 i)
          ( map-span-type-family 𝒯 i)
          ( h))

module _
  {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2}
  (𝒮 : span-type-family l3 A) (𝒯 : span-type-family l4 A)
  (h : hom-span-type-family 𝒮 𝒯)
  where

  map-hom-span-type-family :
    spanning-type-span-type-family 𝒮 →
    spanning-type-span-type-family 𝒯
  map-hom-span-type-family = pr1 h

  coherence-triangle-hom-span-type-family :
    (i : I) →
    coherence-triangle-maps
      ( map-span-type-family 𝒮 i)
      ( map-span-type-family 𝒯 i)
      ( map-hom-span-type-family)
  coherence-triangle-hom-span-type-family =
    pr2 h

Homotopies of morphisms of spans on families of types

Consider two spans 𝒮 := (S , f) and 𝒯 := (T , g) on a family of types A : I → 𝒰, and consider two morphisms (h , H) and (k , K) between them. A homotopy is a pair (α , β) consisting of a homotopy

  α : h ~ k

and a family β of homotopies witnessing that the triangle

              f i
             /   \
        H i / β i \ K i
           ∨       ∨
  (g i ∘ h) ------> (g i ∘ k)
            g i · α

commutes for each i : I.

module _
  {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2}
  (𝒮 : span-type-family l3 A) (𝒯 : span-type-family l4 A)
  (h k : hom-span-type-family 𝒮 𝒯)
  where

  coherence-htpy-hom-span-type-family :
    map-hom-span-type-family 𝒮 𝒯 h ~ map-hom-span-type-family 𝒮 𝒯 k →
    UU (l1 ⊔ l2 ⊔ l3)
  coherence-htpy-hom-span-type-family α =
    (i : I) →
    coherence-triangle-homotopies'
      ( coherence-triangle-hom-span-type-family 𝒮 𝒯 k i)
      ( map-span-type-family 𝒯 i ·l α)
      ( coherence-triangle-hom-span-type-family 𝒮 𝒯 h i)

  htpy-hom-span-type-family : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  htpy-hom-span-type-family =
    Σ ( map-hom-span-type-family 𝒮 𝒯 h ~ map-hom-span-type-family 𝒮 𝒯 k)
      ( coherence-htpy-hom-span-type-family)

  module _
    (α : htpy-hom-span-type-family)
    where

    htpy-htpy-hom-span-type-family :
      map-hom-span-type-family 𝒮 𝒯 h ~ map-hom-span-type-family 𝒮 𝒯 k
    htpy-htpy-hom-span-type-family = pr1 α

    coh-htpy-hom-span-type-family :
      coherence-htpy-hom-span-type-family htpy-htpy-hom-span-type-family
    coh-htpy-hom-span-type-family = pr2 α

The reflexivity homotopy on a morphism of spans on families of types

module _
  {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2}
  (𝒮 : span-type-family l3 A) (𝒯 : span-type-family l4 A)
  (h : hom-span-type-family 𝒮 𝒯)
  where

  refl-htpy-hom-span-type-family :
    htpy-hom-span-type-family 𝒮 𝒯 h h
  pr1 refl-htpy-hom-span-type-family = refl-htpy
  pr2 refl-htpy-hom-span-type-family i = right-unit-htpy

Properties

Characterization of identifications of morphisms of spans on families of types

module _
  {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2}
  (𝒮 : span-type-family l3 A) (𝒯 : span-type-family l4 A)
  (h : hom-span-type-family 𝒮 𝒯)
  where

  htpy-eq-hom-span-type-family :
    (k : hom-span-type-family 𝒮 𝒯) →
    h ＝ k → htpy-hom-span-type-family 𝒮 𝒯 h k
  htpy-eq-hom-span-type-family .h refl =
    refl-htpy-hom-span-type-family 𝒮 𝒯 h

  is-torsorial-htpy-hom-span-type-family :
    is-torsorial (htpy-hom-span-type-family 𝒮 𝒯 h)
  is-torsorial-htpy-hom-span-type-family =
    is-torsorial-Eq-structure
      ( is-torsorial-htpy _)
      ( map-hom-span-type-family 𝒮 𝒯 h , refl-htpy)
      ( is-torsorial-Eq-Π (λ i → is-torsorial-htpy _))

  is-equiv-htpy-eq-hom-span-type-family :
    (k : hom-span-type-family 𝒮 𝒯) →
    is-equiv (htpy-eq-hom-span-type-family k)
  is-equiv-htpy-eq-hom-span-type-family =
    fundamental-theorem-id
      ( is-torsorial-htpy-hom-span-type-family)
      ( htpy-eq-hom-span-type-family)

  extensionality-hom-span-type-family :
    (k : hom-span-type-family 𝒮 𝒯) →
    (h ＝ k) ≃ htpy-hom-span-type-family 𝒮 𝒯 h k
  pr1 (extensionality-hom-span-type-family k) =
    htpy-eq-hom-span-type-family k
  pr2 (extensionality-hom-span-type-family k) =
    is-equiv-htpy-eq-hom-span-type-family k

  eq-htpy-hom-span-type-family :
    (k : hom-span-type-family 𝒮 𝒯) →
    htpy-hom-span-type-family 𝒮 𝒯 h k → h ＝ k
  eq-htpy-hom-span-type-family k =
    map-inv-equiv (extensionality-hom-span-type-family k)

Recent changes