# Equivalence induction

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-02-15.

module foundation.equivalence-induction where

Imports
open import foundation.dependent-pair-types
open import foundation.identity-systems
open import foundation.subuniverses
open import foundation.univalence
open import foundation.universal-property-identity-systems
open import foundation.universe-levels

open import foundation-core.commuting-triangles-of-maps
open import foundation-core.contractible-maps
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.identity-types
open import foundation-core.postcomposition-functions
open import foundation-core.sections
open import foundation-core.torsorial-type-families


## Idea

Equivalence induction is the principle asserting that for any type family

  P : (B : 𝒰) (e : A ≃ B) → 𝒰


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

  ((B : 𝒰) (e : A ≃ B) → P B e) → P A id-equiv.


The principle of equivalence induction is equivalent to the univalence axiom.

By equivalence induction, it follows that any type family P : 𝒰 → 𝒱 on the universe has an action on equivalences

  (A ≃ B) → P A ≃ P B.


## Definitions

### Evaluation at the identity equivalence

module _
{l1 l2 : Level} {A : UU l1}
where

ev-id-equiv :
(P : (B : UU l1) → (A ≃ B) → UU l2) →
((B : UU l1) (e : A ≃ B) → P B e) → P A id-equiv
ev-id-equiv P f = f A id-equiv

triangle-ev-id-equiv :
(P : (Σ (UU l1) (A ≃_)) → UU l2) →
coherence-triangle-maps
( ev-point (A , id-equiv))
( ev-id-equiv (λ X e → P (X , e)))
( ev-pair)
triangle-ev-id-equiv P f = refl


### The equivalence induction principle

module _
{l1 : Level} (A : UU l1)
where

induction-principle-equivalences : UUω
induction-principle-equivalences =
is-identity-system (λ (B : UU l1) → A ≃ B) A id-equiv


## Properties

### Contractibility of the total space of equivalences implies equivalence induction

module _
{l1 : Level} {A : UU l1}
where

abstract
is-identity-system-is-torsorial-equiv :
is-torsorial (λ (B : UU l1) → A ≃ B) →
is-identity-system (A ≃_) A id-equiv
is-identity-system-is-torsorial-equiv =
is-identity-system-is-torsorial A id-equiv


### Equivalence induction implies contractibility of the total space of equivalences

module _
{l1 : Level} {A : UU l1}
where

abstract
is-torsorial-equiv-induction-principle-equivalences :
induction-principle-equivalences A →
is-torsorial (λ (B : UU l1) → A ≃ B)
is-torsorial-equiv-induction-principle-equivalences =
is-torsorial-is-identity-system A id-equiv

abstract
is-torsorial-is-identity-system-equiv :
is-identity-system (A ≃_) A id-equiv →
is-torsorial (λ (B : UU l1) → A ≃ B)
is-torsorial-is-identity-system-equiv =
is-torsorial-is-identity-system A id-equiv


### Equivalence induction in a universe

module _
{l1 : Level} {A : UU l1}
where

abstract
is-identity-system-equiv : induction-principle-equivalences A
is-identity-system-equiv =
is-identity-system-is-torsorial-equiv (is-torsorial-equiv A)

ind-equiv :
{l2 : Level} (P : (B : UU l1) → A ≃ B → UU l2) →
P A id-equiv → {B : UU l1} (e : A ≃ B) → P B e
ind-equiv P p {B} = pr1 (is-identity-system-equiv P) p B

compute-ind-equiv :
{l2 : Level} (P : (B : UU l1) → A ≃ B → UU l2) →
(u : P A id-equiv) → ind-equiv P u id-equiv ＝ u
compute-ind-equiv P = pr2 (is-identity-system-equiv P)


### Equivalence induction in a subuniverse

module _
{l1 l2 l3 : Level} (P : subuniverse l1 l2) (A : type-subuniverse P)
where

ev-id-equiv-subuniverse :
{F : (B : type-subuniverse P) → equiv-subuniverse P A B → UU l3} →
((B : type-subuniverse P) (e : equiv-subuniverse P A B) → F B e) →
F A id-equiv
ev-id-equiv-subuniverse f = f A id-equiv

triangle-ev-id-equiv-subuniverse :
(F : (B : type-subuniverse P) → equiv-subuniverse P A B → UU l3) →
coherence-triangle-maps
( ev-point (A , id-equiv))
( ev-id-equiv-subuniverse {F})
( ev-pair)
triangle-ev-id-equiv-subuniverse F E = refl

abstract
is-identity-system-equiv-subuniverse :
(F : (B : type-subuniverse P) → equiv-subuniverse P A B → UU l3) →
section (ev-id-equiv-subuniverse {F})
is-identity-system-equiv-subuniverse =
is-identity-system-is-torsorial A id-equiv
( is-torsorial-equiv-subuniverse P A)

ind-equiv-subuniverse :
(F : (B : type-subuniverse P) → equiv-subuniverse P A B → UU l3) →
F A id-equiv → (B : type-subuniverse P) (e : equiv-subuniverse P A B) →
F B e
ind-equiv-subuniverse F =
pr1 (is-identity-system-equiv-subuniverse F)

compute-ind-equiv-subuniverse :
(F : (B : type-subuniverse P) → equiv-subuniverse P A B → UU l3) →
(u : F A id-equiv) →
ind-equiv-subuniverse F u A id-equiv ＝ u
compute-ind-equiv-subuniverse F =
pr2 (is-identity-system-equiv-subuniverse F)


### The evaluation map ev-id-equiv is an equivalence

module _
{l1 l2 : Level} {A : UU l1} (P : (B : UU l1) (e : A ≃ B) → UU l2)
where

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

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


### The evaluation map ev-id-equiv-subuniverse is an equivalence

module _
{l1 l2 l3 : Level} (P : subuniverse l1 l2) (X : type-subuniverse P)
(F : (Y : type-subuniverse P) (e : equiv-subuniverse P X Y) → UU l3)
where

is-equiv-ev-id-equiv-subuniverse :
is-equiv (ev-id-equiv-subuniverse P X {F})
is-equiv-ev-id-equiv-subuniverse =
dependent-universal-property-identity-system-is-torsorial
( id-equiv) (is-torsorial-equiv-subuniverse P X) F

is-contr-map-ev-id-equiv-subuniverse :
is-contr-map (ev-id-equiv-subuniverse P X {F})
is-contr-map-ev-id-equiv-subuniverse =
is-contr-map-is-equiv is-equiv-ev-id-equiv-subuniverse


### Equivalence induction implies that postcomposing by an equivalence is an equivalence

Of course we already know that this fact follows from function extensionality. However, we prove it again from equivalence induction so that we can prove that univalence implies function extensionality.

abstract
is-equiv-postcomp-univalence :
{l1 l2 : Level} {X Y : UU l1} (A : UU l2) (e : X ≃ Y) →
is-equiv (postcomp A (map-equiv e))
is-equiv-postcomp-univalence A =
ind-equiv (λ Y e → is-equiv (postcomp A (map-equiv e))) is-equiv-id