Equivalances of dependent sequential diagrams

Content created by Vojtěch Štěpančík.

Created on 2024-04-16.
Last modified on 2024-06-01.

module synthetic-homotopy-theory.equivalences-dependent-sequential-diagrams where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.commuting-squares-of-maps
open import foundation.dependent-pair-types
open import foundation.equality-dependent-function-types
open import foundation.equivalences
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.homotopy-induction
open import foundation.identity-types
open import foundation.structure-identity-principle
open import foundation.torsorial-type-families
open import foundation.univalence
open import foundation.universe-levels

open import synthetic-homotopy-theory.dependent-sequential-diagrams
open import synthetic-homotopy-theory.morphisms-dependent-sequential-diagrams
open import synthetic-homotopy-theory.sequential-diagrams

Idea

Consider two dependent sequential diagrams

     b₀      b₁      b₂            c₀      c₁      c₂
 B₀ ---> B₁ ---> B₂ ---> ⋯     C₀ ---> C₁ ---> C₂ ---> ⋯
 |       |       |             |       |       |
 |       |       |             |       |       |
 ↡       ↡       ↡             ↡       ↡       ↡
 A₀ ---> A₁ ---> A₂ ---> ⋯     A₀ ---> A₁ ---> A₂ ---> ⋯ .
     a₀      a₁      a₂            a₀      a₁      a₂

An equivalence of dependent sequential diagrams between them is a family of fiberwise equivalences

eₙ : (a : Aₙ) → Bₙ a ≃ Cₙ a

equipped with a family of fiberwise homotopies making the squares

                 eₙ a
     Bₙ a -----------------> Cₙ a
       |          ≃            |
  bₙ a |                       | cₙ a
       |                       |
       ∨          ≃            ∨
  Bₙ₊₁ (aₙ a) ----------> Cₙ₊₁ (aₙ a)
              eₙ₊₁ (aₙ a)

commute.

Definitions

Equivalences of dependent sequential diagrams

module _
  {l1 l2 l3 : Level} {A : sequential-diagram l1}
  (B : dependent-sequential-diagram A l2)
  (C : dependent-sequential-diagram A l3)
  where

  coherence-equiv-dependent-sequential-diagram :
    ( (n : ℕ) (a : family-sequential-diagram A n) →
      family-dependent-sequential-diagram B n a ≃
      family-dependent-sequential-diagram C n a) →
    UU (l1 ⊔ l2 ⊔ l3)
  coherence-equiv-dependent-sequential-diagram h =
    (n : ℕ) (a : family-sequential-diagram A n) →
    coherence-square-maps
      ( map-equiv (h n a))
      ( map-dependent-sequential-diagram B n a)
      ( map-dependent-sequential-diagram C n a)
      ( map-equiv (h (succ-ℕ n) (map-sequential-diagram A n a)))

  equiv-dependent-sequential-diagram : UU (l1 ⊔ l2 ⊔ l3)
  equiv-dependent-sequential-diagram =
    Σ ( (n : ℕ) (a : family-sequential-diagram A n) →
        family-dependent-sequential-diagram B n a ≃
        family-dependent-sequential-diagram C n a)
      ( coherence-equiv-dependent-sequential-diagram)

Components of an equivalence of dependent sequential diagrams

module _
  {l1 l2 l3 : Level} {A : sequential-diagram l1}
  {B : dependent-sequential-diagram A l2}
  (C : dependent-sequential-diagram A l3)
  (e : equiv-dependent-sequential-diagram B C)
  where

  equiv-equiv-dependent-sequential-diagram :
    (n : ℕ) (a : family-sequential-diagram A n) →
    family-dependent-sequential-diagram B n a ≃
    family-dependent-sequential-diagram C n a
  equiv-equiv-dependent-sequential-diagram = pr1 e

  map-equiv-dependent-sequential-diagram :
    (n : ℕ) (a : family-sequential-diagram A n) →
    family-dependent-sequential-diagram B n a →
    family-dependent-sequential-diagram C n a
  map-equiv-dependent-sequential-diagram n a =
    map-equiv (equiv-equiv-dependent-sequential-diagram n a)

  is-equiv-map-equiv-dependent-sequential-diagram :
    (n : ℕ) (a : family-sequential-diagram A n) →
    is-equiv (map-equiv-dependent-sequential-diagram n a)
  is-equiv-map-equiv-dependent-sequential-diagram n a =
    is-equiv-map-equiv (equiv-equiv-dependent-sequential-diagram n a)

  coh-equiv-dependent-sequential-diagram :
    coherence-equiv-dependent-sequential-diagram B C
      ( equiv-equiv-dependent-sequential-diagram)
  coh-equiv-dependent-sequential-diagram = pr2 e

  hom-equiv-dependent-sequential-diagram :
    hom-dependent-sequential-diagram B C
  pr1 hom-equiv-dependent-sequential-diagram =
    map-equiv-dependent-sequential-diagram
  pr2 hom-equiv-dependent-sequential-diagram =
    coh-equiv-dependent-sequential-diagram

The predicate on morphisms of dependent sequential daigrams of being an equivalence

module _
  {l1 l2 l3 : Level} {A : sequential-diagram l1}
  {B : dependent-sequential-diagram A l2}
  (C : dependent-sequential-diagram A l3)
  where

  is-equiv-hom-dependent-sequential-diagram :
    hom-dependent-sequential-diagram B C → UU (l1 ⊔ l2 ⊔ l3)
  is-equiv-hom-dependent-sequential-diagram h =
    (n : ℕ) (a : family-sequential-diagram A n) →
    is-equiv (map-hom-dependent-sequential-diagram C h n a)

  is-equiv-hom-equiv-dependent-sequential-diagram :
    (e : equiv-dependent-sequential-diagram B C) →
    is-equiv-hom-dependent-sequential-diagram
      ( hom-equiv-dependent-sequential-diagram C e)
  is-equiv-hom-equiv-dependent-sequential-diagram e =
    is-equiv-map-equiv-dependent-sequential-diagram C e

The identity equivalence of sequential diagrams

module _
  {l1 l2 : Level} {A : sequential-diagram l1}
  (B : dependent-sequential-diagram A l2)
  where

  id-equiv-dependent-sequential-diagram : equiv-dependent-sequential-diagram B B
  pr1 id-equiv-dependent-sequential-diagram n a = id-equiv
  pr2 id-equiv-dependent-sequential-diagram n a = refl-htpy

Properties

Morphisms of dependent sequential diagrams which are equivalences are equivalences of dependent sequential diagrams

To construct an equivalence of dependent sequential diagrams e : B ≃ C, it suffices to construct a morphism h : B → C and a proof that the maps hₙ are fiberwise equivalences.

module _
  {l1 l2 l3 : Level} {A : sequential-diagram l1}
  {B : dependent-sequential-diagram A l2}
  (C : dependent-sequential-diagram A l3)
  (h : hom-dependent-sequential-diagram B C)
  where

  equiv-hom-dependent-sequential-diagram :
    is-equiv-hom-dependent-sequential-diagram C h →
    equiv-dependent-sequential-diagram B C
  pr1 (equiv-hom-dependent-sequential-diagram is-equiv-map) n a =
    (map-hom-dependent-sequential-diagram C h n a , is-equiv-map n a)
  pr2 (equiv-hom-dependent-sequential-diagram is-equiv-map) =
    coh-hom-dependent-sequential-diagram C h

Characterization of identity types of dependent sequential diagrams

The type of equivalences of dependent sequential diagrams characterizes the identity type of dependent sequential diagrams.

module _
  {l1 l2 : Level} {A : sequential-diagram l1}
  (B : dependent-sequential-diagram A l2)
  where

  equiv-eq-dependent-sequential-diagram :
    (C : dependent-sequential-diagram A l2) →
    (B ＝ C) → equiv-dependent-sequential-diagram B C
  equiv-eq-dependent-sequential-diagram .B refl =
    id-equiv-dependent-sequential-diagram B

  abstract
    is-torsorial-equiv-dependent-sequential-diagram :
      is-torsorial (equiv-dependent-sequential-diagram {l3 = l2} B)
    is-torsorial-equiv-dependent-sequential-diagram =
      is-torsorial-Eq-structure
        ( is-torsorial-Eq-Π
          ( λ n →
            is-torsorial-Eq-Π
              ( λ a →
                is-torsorial-equiv
                  ( family-dependent-sequential-diagram B n a))))
        ( family-dependent-sequential-diagram B , λ n a → id-equiv)
        ( is-torsorial-Eq-Π
          ( λ n →
            is-torsorial-Eq-Π
              ( λ a →
                is-torsorial-htpy (map-dependent-sequential-diagram B n a))))

  is-equiv-equiv-eq-dependent-sequential-diagram :
    (C : dependent-sequential-diagram A l2) →
    is-equiv (equiv-eq-dependent-sequential-diagram C)
  is-equiv-equiv-eq-dependent-sequential-diagram =
    fundamental-theorem-id
      ( is-torsorial-equiv-dependent-sequential-diagram)
      ( equiv-eq-dependent-sequential-diagram)

  extensionality-dependent-sequential-diagram :
    (C : dependent-sequential-diagram A l2) →
    (B ＝ C) ≃ equiv-dependent-sequential-diagram B C
  pr1 (extensionality-dependent-sequential-diagram C) =
    equiv-eq-dependent-sequential-diagram C
  pr2 (extensionality-dependent-sequential-diagram C) =
    is-equiv-equiv-eq-dependent-sequential-diagram C

  eq-equiv-dependent-sequential-diagram :
    (C : dependent-sequential-diagram A l2) →
    equiv-dependent-sequential-diagram B C → (B ＝ C)
  eq-equiv-dependent-sequential-diagram C =
    map-inv-equiv (extensionality-dependent-sequential-diagram C)

Recent changes