Equivalences of span diagrams on families of types

Content created by Egbert Rijke.

Created on 2024-01-28.
Last modified on 2024-04-25.

module foundation.equivalences-span-diagrams-families-of-types where
Imports 
open import foundation.commuting-squares-of-maps
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.equivalences-spans-families-of-types
open import foundation.homotopies
open import foundation.operations-spans-families-of-types
open import foundation.span-diagrams-families-of-types
open import foundation.universe-levels

Idea

An equivalence of span diagrams on families of types from a span (A , s) of families of types indexed by a type I to a span (B , t) indexed by I consists of a family of equivalences h : Aᵢ ≃ Bᵢ, and an equivalence e : S ≃ T equipped with a family of homotopies witnessing that the square

         e
     S -----> T
     |        |
  fᵢ |        | gᵢ
     ∨        ∨
     Aᵢ ----> Bᵢ
         h

commutes for each i : I.

Definitions

Equivalences of span diagrams on families of types

module _
  {l1 l2 l3 l4 l5 : Level} {I : UU l1}
  (S : span-diagram-type-family l2 l3 I)
  (T : span-diagram-type-family l4 l5 I)
  where

  equiv-span-diagram-type-family : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
  equiv-span-diagram-type-family =
    Σ ( (i : I) →
        family-span-diagram-type-family S i ≃
        family-span-diagram-type-family T i)
      ( λ e →
        equiv-span-type-family
          ( concat-span-hom-family-of-types
            ( span-span-diagram-type-family S)
            ( λ i → map-equiv (e i)))
          ( span-span-diagram-type-family T))

  module _
    (e : equiv-span-diagram-type-family)
    where

    equiv-family-equiv-span-diagram-type-family :
      (i : I) →
      family-span-diagram-type-family S i ≃
      family-span-diagram-type-family T i
    equiv-family-equiv-span-diagram-type-family = pr1 e

    map-family-equiv-span-diagram-type-family :
      (i : I) →
      family-span-diagram-type-family S i →
      family-span-diagram-type-family T i
    map-family-equiv-span-diagram-type-family i =
      map-equiv (equiv-family-equiv-span-diagram-type-family i)

    equiv-span-equiv-span-diagram-type-family :
      equiv-span-type-family
        ( concat-span-hom-family-of-types
          ( span-span-diagram-type-family S)
          ( map-family-equiv-span-diagram-type-family))
        ( span-span-diagram-type-family T)
    equiv-span-equiv-span-diagram-type-family = pr2 e

    spanning-equiv-equiv-span-diagram-type-family :
      spanning-type-span-diagram-type-family S ≃
      spanning-type-span-diagram-type-family T
    spanning-equiv-equiv-span-diagram-type-family =
      equiv-equiv-span-type-family
        ( concat-span-hom-family-of-types
          ( span-span-diagram-type-family S)
          ( map-family-equiv-span-diagram-type-family))
        ( span-span-diagram-type-family T)
        ( equiv-span-equiv-span-diagram-type-family)

    spanning-map-equiv-span-diagram-type-family :
      spanning-type-span-diagram-type-family S →
      spanning-type-span-diagram-type-family T
    spanning-map-equiv-span-diagram-type-family =
      map-equiv spanning-equiv-equiv-span-diagram-type-family

    coherence-square-equiv-span-diagram-type-family :
      (i : I) →
      coherence-square-maps
        ( spanning-map-equiv-span-diagram-type-family)
        ( map-span-diagram-type-family S i)
        ( map-span-diagram-type-family T i)
        ( map-family-equiv-span-diagram-type-family i)
    coherence-square-equiv-span-diagram-type-family =
      triangle-equiv-span-type-family
        ( concat-span-hom-family-of-types
          ( span-span-diagram-type-family S)
          ( map-family-equiv-span-diagram-type-family))
        ( span-span-diagram-type-family T)
        ( equiv-span-equiv-span-diagram-type-family)

Identity equivalences of spans diagrams on families of types

module _
  {l1 l2 l3 : Level} {I : UU l1} {𝒮 : span-diagram-type-family l2 l3 I}
  where

  id-equiv-span-diagram-type-family :
    equiv-span-diagram-type-family 𝒮 𝒮
  pr1 id-equiv-span-diagram-type-family i = id-equiv
  pr1 (pr2 id-equiv-span-diagram-type-family) = id-equiv
  pr2 (pr2 id-equiv-span-diagram-type-family) i = refl-htpy

See also

Recent changes