# Isomorphism induction in categories

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-10-20.

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