{-# OPTIONS --without-K #-}
open import lib.Base
open import lib.PathGroupoid
open import lib.PathFunctor
open import lib.Equivalences
module lib.Univalence where
coe-equiv : ∀ {i} {A B : Type i} → A == B → A ≃ B
coe-equiv p = equiv (coe p) (coe! p) (coe!-inv-r p) (coe!-inv-l p)
postulate
ua : ∀ {i} {A B : Type i} → (A ≃ B) → A == B
coe-equiv-β : ∀ {i} {A B : Type i} (e : A ≃ B) → coe-equiv (ua e) == e
ua-η : ∀ {i} {A B : Type i} (p : A == B) → ua (coe-equiv p) == p
ua-equiv : ∀ {i} {A B : Type i} → (A ≃ B) ≃ (A == B)
ua-equiv = equiv ua coe-equiv ua-η coe-equiv-β
coe-β : ∀ {i} {A B : Type i} (e : A ≃ B) (a : A)
→ coe (ua e) a == –> e a
coe-β e a = ap (λ e → –> e a) (coe-equiv-β e)
coe!-β : ∀ {i} {A B : Type i} (e : A ≃ B) (b : B)
→ coe! (ua e) b == <– e b
coe!-β e a = ap (λ e → <– e a) (coe-equiv-β e)
↓-idf-ua-out : ∀ {i} {A B : Type i} (e : A ≃ B) {u : A} {v : B}
→ u == v [ (λ x → x) ↓ (ua e) ]
→ –> e u == v
↓-idf-ua-out e p = ! (coe-β e _) ∙ aux (ua e) p where
aux : ∀ {i} {A B : Type i} (p : A == B) {u : A} {v : B}
→ u == v [ (λ x → x) ↓ p ]
→ coe p u == v
aux idp = idf _
↓-idf-ua-in : ∀ {i} {A B : Type i} (e : A ≃ B) {u : A} {v : B}
→ –> e u == v
→ u == v [ (λ x → x) ↓ (ua e) ]
↓-idf-ua-in e p = aux (ua e) (coe-β e _ ∙ p) where
aux : ∀ {i} {A B : Type i} (p : A == B) {u : A} {v : B}
→ coe p u == v
→ u == v [ (λ x → x) ↓ p ]
aux idp = idf _
equiv-induction : ∀ {i j} (P : {A B : Type i} (f : A ≃ B) → Type j)
(d : (A : Type i) → P (ide A)) {A B : Type i} (f : A ≃ B)
→ P f
equiv-induction {i} {j} P d f =
transport P (coe-equiv-β f)
(aux P d (ua f)) where
aux : ∀ {j} (P : {A : Type i} {B : Type i} (f : A ≃ B) → Type j)
(d : (A : Type i) → P (ide A)) {A B : Type i} (p : A == B)
→ P (coe-equiv p)
aux P d idp = d _