Isomorphism induction in categories

Content created by Fredrik Bakke and Egbert Rijke.

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

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

open import foundation.commuting-triangles-of-maps
open import foundation.contractible-maps
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.identity-types
open import foundation.sections
open import foundation.universal-property-identity-systems
open import foundation.universe-levels

Idea

Isomorphism induction in a category 𝒞 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.

Statement

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

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

  induction-principle-iso-Category :
    {l : Level} (P : (B : obj-Category C) (e : iso-Category C A B) → UU l) →
    UU (l1 ⊔ l2 ⊔ l)
  induction-principle-iso-Category =
    induction-principle-iso-Precategory (precategory-Category C)

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

Properties

Isomorphism induction in a category

module _
  {l1 l2 l3 : Level} (C : Category l1 l2) {A : obj-Category C}
  (P : (B : obj-Category C) (e : iso-Category C A B) → UU l3)
  where

  abstract
    is-identity-system-iso-Category : section (ev-id-iso-Category C P)
    is-identity-system-iso-Category =
      is-identity-system-is-torsorial-iso-Precategory
        ( precategory-Category C)
        ( is-torsorial-iso-Category C A)
        ( P)

  ind-iso-Category :
    P A (id-iso-Category C) →
    {B : obj-Category C} (e : iso-Category C A B) → P B e
  ind-iso-Category p {B} = pr1 is-identity-system-iso-Category p B

  compute-ind-iso-Category :
    (u : P A (id-iso-Category C)) → ind-iso-Category u (id-iso-Category C) ＝ u
  compute-ind-iso-Category = pr2 is-identity-system-iso-Category

The evaluation map ev-id-iso-Category is an equivalence

module _
  {l1 l2 l3 : Level} (C : Category l1 l2) {A : obj-Category C}
  (P : (B : obj-Category C) (e : iso-Category C A B) → UU l3)
  where

  is-equiv-ev-id-iso-Category : is-equiv (ev-id-iso-Category C P)
  is-equiv-ev-id-iso-Category =
    dependent-universal-property-identity-system-is-torsorial
      ( id-iso-Category C)
      ( is-torsorial-iso-Category C A)
      ( P)

  is-contr-map-ev-id-iso-Category :
    is-contr-map (ev-id-iso-Category C P)
  is-contr-map-ev-id-iso-Category =
    is-contr-map-is-equiv is-equiv-ev-id-iso-Category

Recent changes