Isomorphism induction in precategories

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-20.
Last modified on 2023-11-24.

module category-theory.isomorphism-induction-precategories where
Imports 
open import category-theory.isomorphisms-in-precategories
open import category-theory.precategories

open import foundation.commuting-triangles-of-maps
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.identity-systems
open import foundation.identity-types
open import foundation.sections
open import foundation.torsorial-type-families
open import foundation.universe-levels

Idea

Isomorphism induction in a precategory 𝒞 is the principle asserting that, given an object A : 𝒞 and any type family

  P : (B : 𝒞) (ϕ : A ≅ B) → 𝒰

of types indexed by all isomorphisms with domain A, there is a section of the evaluation map

  ((B : 𝒞) (ϕ : A ≅ B) → P B ϕ) → P A id-iso.

The principle of isomorphism induction is equivalent to the univalence axiom for categories, hence this is one approach to proving that a precategory is a category.

Statement

module _
  {l1 l2 : Level} (C : Precategory l1 l2) {A : obj-Precategory C}
  where

  ev-id-iso-Precategory :
    {l : Level} (P : (B : obj-Precategory C) → (iso-Precategory C A B) → UU l) →
    ((B : obj-Precategory C) (e : iso-Precategory C A B) → P B e) →
    P A (id-iso-Precategory C)
  ev-id-iso-Precategory P f = f A (id-iso-Precategory C)

  induction-principle-iso-Precategory :
    {l : Level} (P : (B : obj-Precategory C) → iso-Precategory C A B → UU l) →
    UU (l1 ⊔ l2 ⊔ l)
  induction-principle-iso-Precategory P = section (ev-id-iso-Precategory P)

  triangle-ev-id-iso-Precategory :
    {l : Level}
    (P : (B : obj-Precategory C) → iso-Precategory C A B → UU l) →
    coherence-triangle-maps
      ( ev-point (A , id-iso-Precategory C))
      ( ev-id-iso-Precategory P)
      ( ev-pair)
  triangle-ev-id-iso-Precategory P f = refl

Properties

Contractibility of the total space of isomorphisms implies isomorphism induction

module _
  {l1 l2 : Level} (C : Precategory l1 l2) {A : obj-Precategory C}
  where

  abstract
    is-identity-system-is-torsorial-iso-Precategory :
      is-torsorial (iso-Precategory C A) →
      is-identity-system (iso-Precategory C A) A (id-iso-Precategory C)
    is-identity-system-is-torsorial-iso-Precategory =
      is-identity-system-is-torsorial A (id-iso-Precategory C)

Isomorphism induction implies contractibility of the total space of isomorphisms

module _
  {l1 l2 : Level} (C : Precategory l1 l2) {A : obj-Precategory C}
  where

  is-torsorial-equiv-induction-principle-iso-Precategory :
    is-identity-system (iso-Precategory C A) A (id-iso-Precategory C) →
    is-torsorial (iso-Precategory C A)
  is-torsorial-equiv-induction-principle-iso-Precategory =
    is-torsorial-is-identity-system A (id-iso-Precategory C)

Recent changes