# Equivalence induction

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

Created on 2022-02-15.

module foundation-core.equivalence-induction where

Imports
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.contractible-types
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.sections
open import foundation-core.singleton-induction


## Idea

Equivalence induction is a condition equivalent to the univalence axiom

## Properties

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

ev-id :
{ l : Level} (P : (B : UU l1) → (A ≃ B) → UU l) →
( (B : UU l1) (e : A ≃ B) → P B e) → P A id-equiv
ev-id P f = f A id-equiv

IND-EQUIV :
{l : Level} (P : (B : UU l1) (e : A ≃ B) → UU l) → UU (lsuc l1 ⊔ l)
IND-EQUIV P = section (ev-id P)

triangle-ev-id :
{ l : Level}
( P : (Σ (UU l1) (λ X → A ≃ X)) → UU l) →
( ev-point (pair A id-equiv) {P}) ~
( ( ev-id (λ X e → P (pair X e))) ∘
( ev-pair {A = UU l1} {B = λ X → A ≃ X} {C = P}))
triangle-ev-id P f = refl


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

  abstract
IND-EQUIV-is-contr-total-equiv :
is-contr (Σ (UU l1) (λ X → A ≃ X)) →
{l : Level} →
(P : (Σ (UU l1) (λ X → A ≃ X)) → UU l) → IND-EQUIV (λ B e → P (pair B e))
IND-EQUIV-is-contr-total-equiv c P =
section-left-factor
( ev-id (λ X e → P (pair X e)))
( ev-pair)
( is-singleton-is-contr
( pair A id-equiv)
( pair
( pair A id-equiv)
( λ t → ( inv (contraction c (pair A id-equiv))) ∙
( contraction c t)))
( P))


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

  abstract
is-contr-total-equiv-IND-EQUIV :
( {l : Level} (P : (Σ (UU l1) (λ X → A ≃ X)) → UU l) →
IND-EQUIV (λ B e → P (pair B e))) →
is-contr (Σ (UU l1) (λ X → A ≃ X))
is-contr-total-equiv-IND-EQUIV ind =
is-contr-is-singleton
( Σ (UU l1) (λ X → A ≃ X))
( pair A id-equiv)
( λ P → section-comp
( ev-id (λ X e → P (pair X e)))
( ev-pair {A = UU l1} {B = λ X → A ≃ X} {C = P})
( pair ind-Σ refl-htpy)
( ind P))