Equivalence extensionality

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Elisabeth Stenholm.

Created on 2023-01-18.
Last modified on 2024-02-06.

module foundation.equivalence-extensionality where
Imports 
open import foundation.dependent-pair-types
open import foundation.dependent-universal-property-equivalences
open import foundation.function-extensionality
open import foundation.fundamental-theorem-of-identity-types
open import foundation.identity-systems
open import foundation.subtype-identity-principle
open import foundation.universe-levels

open import foundation-core.contractible-maps
open import foundation-core.contractible-types
open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.sections
open import foundation-core.torsorial-type-families
open import foundation-core.type-theoretic-principle-of-choice

Characterizing the identity type of equivalences

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  where

  htpy-equiv : A ≃ B → A ≃ B → UU (l1 ⊔ l2)
  htpy-equiv e e' = (map-equiv e) ~ (map-equiv e')

  _~e_ = htpy-equiv

  extensionality-equiv : (f g : A ≃ B) → (f ＝ g) ≃ htpy-equiv f g
  extensionality-equiv f =
    extensionality-type-subtype
      ( is-equiv-Prop)
      ( pr2 f)
      ( refl-htpy' (pr1 f))
      ( λ g → equiv-funext)
    where
    is-equiv-Prop : (f : A → B) → Prop (l1 ⊔ l2)
    pr1 (is-equiv-Prop f) = is-equiv f
    pr2 (is-equiv-Prop f) H =
      is-prop-is-contr
        ( is-contr-product
          ( is-contr-equiv'
            ( (b : B) → fiber f b)
            ( distributive-Π-Σ)
            ( is-contr-Π (is-contr-map-is-equiv H)))
          ( is-contr-is-equiv'
            ( Σ (B → A) (λ h → (h ∘ f) ＝ id))
            ( tot (λ h → htpy-eq))
            ( is-equiv-tot-is-fiberwise-equiv
              ( λ h → funext (h ∘ f) id))
            ( is-contr-map-is-equiv
              ( is-equiv-precomp-Π-is-equiv H (λ y → A))
              ( id))))
        ( H)

  abstract
    is-torsorial-htpy-equiv :
      (e : A ≃ B) → is-torsorial (htpy-equiv e)
    is-torsorial-htpy-equiv e =
      fundamental-theorem-id'
        ( map-equiv ∘ extensionality-equiv e)
        ( is-equiv-map-equiv ∘ extensionality-equiv e)

  refl-htpy-equiv : (e : A ≃ B) → htpy-equiv e e
  refl-htpy-equiv e = refl-htpy

  eq-htpy-equiv : {e e' : A ≃ B} → htpy-equiv e e' → e ＝ e'
  eq-htpy-equiv {e} {e'} = map-inv-equiv (extensionality-equiv e e')

  htpy-eq-equiv : {e e' : A ≃ B} → e ＝ e' → htpy-equiv e e'
  htpy-eq-equiv {e} {e'} = map-equiv (extensionality-equiv e e')

  htpy-eq-map-equiv :
    {e e' : A ≃ B} → (map-equiv e) ＝ (map-equiv e') → htpy-equiv e e'
  htpy-eq-map-equiv = htpy-eq

Homotopy induction for homotopies between equivalences

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  where

  abstract
    induction-principle-htpy-equiv :
      {l3 : Level} (e : A ≃ B)
      (P : (e' : A ≃ B) (H : htpy-equiv e e') → UU l3) →
      section
        ( λ (h : (e' : A ≃ B) (H : htpy-equiv e e') → P e' H) →
          h e (refl-htpy-equiv e))
    induction-principle-htpy-equiv e =
      is-identity-system-is-torsorial e
        ( refl-htpy-equiv e)
        ( is-torsorial-htpy-equiv e)

  ind-htpy-equiv :
    {l3 : Level} (e : A ≃ B) (P : (e' : A ≃ B) (H : htpy-equiv e e') → UU l3) →
    P e (refl-htpy-equiv e) → (e' : A ≃ B) (H : htpy-equiv e e') → P e' H
  ind-htpy-equiv e P = pr1 (induction-principle-htpy-equiv e P)

  compute-ind-htpy-equiv :
    {l3 : Level} (e : A ≃ B) (P : (e' : A ≃ B) (H : htpy-equiv e e') → UU l3)
    (p : P e (refl-htpy-equiv e)) →
    ind-htpy-equiv e P p e (refl-htpy-equiv e) ＝ p
  compute-ind-htpy-equiv e P = pr2 (induction-principle-htpy-equiv e P)

Recent changes