# 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)