# Isomorphism induction in precategories ```agda module category-theory.isomorphism-induction-precategories where ``` <details><summary>Imports</summary> ```agda 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 ``` </details> ## Idea **Isomorphism induction** in a precategory `𝒞` is the principle asserting that, given an object `A : 𝒞` and any type family ```text P : (B : 𝒞) (ϕ : A ≅ B) → 𝒰 ``` of types indexed by all [isomorphisms](category-theory.isomorphisms-in-categories.md) with domain `A`, there is a [section](foundation.sections.md) of the evaluation map ```text ((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 ```agda 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 ```agda 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 ```agda 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) ```