```------------------------------------------------------------------------
-- Is-equivalence, defined in terms of contractible fibres
------------------------------------------------------------------------

-- Partly based on Voevodsky's work on univalent foundations.

{-# OPTIONS --cubical-compatible --safe #-}

open import Equality

module Equivalence.Contractible-preimages
{e⁺} (eq : ∀ {a p} → Equality-with-J a p e⁺) where

open Derived-definitions-and-properties eq

open import Prelude as P hiding (id)

open import Bijection eq using (_↔_)
open import Equality.Decision-procedures eq
open import H-level eq as H-level
open import Preimage eq as Preimage using (_⁻¹_)
open import Surjection eq using (_↠_)

private
variable
a b ℓ p q : Level
A B       : Type a
f g       : A → B

------------------------------------------------------------------------
-- Is-equivalence

-- A function f is an equivalence if all preimages under f are
-- contractible.

Is-equivalence :
{A : Type a} {B : Type b} →
(A → B) → Type (a ⊔ b)
Is-equivalence f = ∀ y → Contractible (f ⁻¹ y)

-- Is-equivalence respects extensional equality.

respects-extensional-equality :
(∀ x → f x ≡ g x) →
Is-equivalence f → Is-equivalence g
respects-extensional-equality f≡g f-eq = λ b →
H-level.respects-surjection
(_↔_.surjection (Preimage.respects-extensional-equality f≡g))
0
(f-eq b)

-- If f is an equivalence, then it has an inverse.

inverse :
{@0 A : Type a} {@0 B : Type b} {@0 f : A → B} →
Is-equivalence f → B → A
inverse eq y = proj₁₀ (proj₁₀ (eq y))

right-inverse-of :
{@0 A : Type a} {@0 B : Type b} {@0 f : A → B} →
(eq : Is-equivalence f) → ∀ x → f (inverse eq x) ≡ x
right-inverse-of eq x = proj₂₀ (proj₁₀ (eq x))

opaque

left-inverse-of :
(eq : Is-equivalence f) → ∀ x → inverse eq (f x) ≡ x
left-inverse-of {f} eq x =
cong (proj₁ {B = λ x′ → f x′ ≡ f x}) (
proj₁ (eq (f x))  ≡⟨ proj₂ (eq (f x)) (x , refl (f x)) ⟩∎
(x , refl (f x))  ∎)

-- All fibres of an equivalence over a given point are equal to a
-- given fibre.

irrelevance :
{@0 A : Type a} {@0 B : Type b} {@0 f : A → B} →
(eq : Is-equivalence f) →
∀ y (p : f ⁻¹ y) → (inverse eq y , right-inverse-of eq y) ≡ p
irrelevance eq y = proj₂₀ (eq y)

opaque
unfolding left-inverse-of

-- The two proofs left-inverse-of and right-inverse-of are
-- related.

left-right-lemma :
(eq : Is-equivalence f) →
∀ x → cong f (left-inverse-of eq x) ≡ right-inverse-of eq (f x)
left-right-lemma {f} eq x =
lemma₁ f _ _ (lemma₂ (irrelevance eq (f x) (x , refl (f x))))
where
lemma₁ : {x y : A} (f : A → B) (p : x ≡ y) (q : f x ≡ f y) →
refl (f y) ≡ trans (cong f (sym p)) q →
cong f p ≡ q
lemma₁ f = elim
(λ {x y} p → ∀ q → refl (f y) ≡ trans (cong f (sym p)) q →
cong f p ≡ q)
(λ x q hyp →
cong f (refl x)                  ≡⟨ cong-refl f ⟩
refl (f x)                       ≡⟨ hyp ⟩
trans (cong f (sym (refl x))) q  ≡⟨ cong (λ p → trans (cong f p) q) sym-refl ⟩
trans (cong f (refl x)) q        ≡⟨ cong (λ p → trans p q) (cong-refl f) ⟩
trans (refl (f x)) q             ≡⟨ trans-reflˡ _ ⟩∎
q                                ∎)

lemma₂ : ∀ {f : A → B} {y} {f⁻¹y₁ f⁻¹y₂ : f ⁻¹ y}
(p : f⁻¹y₁ ≡ f⁻¹y₂) →
proj₂ f⁻¹y₂ ≡
trans (cong f (sym (cong (proj₁ {B = λ x → f x ≡ y}) p)))
(proj₂ f⁻¹y₁)
lemma₂ {f} {y} =
let pr = proj₁ {B = λ x → f x ≡ y} in
elim {A = f ⁻¹ y}
(λ {f⁻¹y₁ f⁻¹y₂} p →
proj₂ f⁻¹y₂ ≡
trans (cong f (sym (cong pr p))) (proj₂ f⁻¹y₁))
(λ f⁻¹y →
proj₂ f⁻¹y                                               ≡⟨ sym \$ trans-reflˡ _ ⟩
trans (refl (f (proj₁ f⁻¹y))) (proj₂ f⁻¹y)               ≡⟨ cong (λ p → trans p (proj₂ f⁻¹y)) (sym (cong-refl f)) ⟩
trans (cong f (refl (proj₁ f⁻¹y))) (proj₂ f⁻¹y)          ≡⟨ cong (λ p → trans (cong f p) (proj₂ f⁻¹y)) (sym sym-refl) ⟩
trans (cong f (sym (refl (proj₁ f⁻¹y)))) (proj₂ f⁻¹y)    ≡⟨ cong (λ p → trans (cong f (sym p)) (proj₂ f⁻¹y))
(sym (cong-refl pr)) ⟩∎
trans (cong f (sym (cong pr (refl f⁻¹y)))) (proj₂ f⁻¹y)  ∎)

opaque

right-left-lemma :
(eq : Is-equivalence f) →
∀ x →
cong (inverse eq) (right-inverse-of eq x) ≡
left-inverse-of eq (inverse eq x)
right-left-lemma {f} eq x =
let f⁻¹ = inverse eq in
subst
(λ x → cong f⁻¹ (right-inverse-of eq x) ≡
left-inverse-of eq (f⁻¹ x))
(right-inverse-of eq x)
(cong f⁻¹ (right-inverse-of eq (f (f⁻¹ x)))             ≡⟨ cong (cong f⁻¹) \$ sym \$ left-right-lemma eq _ ⟩

cong f⁻¹ (cong f (left-inverse-of eq (f⁻¹ x)))         ≡⟨ cong-∘ f⁻¹ f _ ⟩

cong (f⁻¹ ∘ f) (left-inverse-of eq (f⁻¹ x))            ≡⟨ cong-roughly-id (f⁻¹ ∘ f) (λ _ → true) (left-inverse-of eq _) _ _
(λ z _ → left-inverse-of eq z) ⟩
trans (left-inverse-of eq (f⁻¹ (f (f⁻¹ x))))
(trans (left-inverse-of eq (f⁻¹ x))
(sym (left-inverse-of eq (f⁻¹ x))))               ≡⟨ cong (trans _) \$ trans-symʳ _ ⟩

trans (left-inverse-of eq (f⁻¹ (f (f⁻¹ x)))) (refl _)  ≡⟨ trans-reflʳ _ ⟩∎

left-inverse-of eq (f⁻¹ (f (f⁻¹ x)))                   ∎)

-- If Σ-map P.id f is an equivalence, then f is also an equivalence.

drop-Σ-map-id :
{A : Type a} {P : A → Type p} {Q : A → Type q}
(f : ∀ {x} → P x → Q x) →
Is-equivalence {A = Σ A P} {B = Σ A Q} (Σ-map P.id f) →
∀ x → Is-equivalence (f {x = x})
drop-Σ-map-id {p = ℓp} {q = ℓq} {A} {P} {Q} f eq x z =
H-level.respects-surjection surj 0 (eq (x , z))
where
map-f : Σ A P → Σ A Q
map-f = Σ-map P.id f

to-P : ∀ {x y} {p : ∃ Q} → (x , f y) ≡ p → Type (ℓp ⊔ ℓq)
to-P {y} {p} _ = ∃ λ y′ → f y′ ≡ proj₂ p

to : map-f ⁻¹ (x , z) → f ⁻¹ z
to ((x′ , y) , eq) = elim¹ to-P (y , refl (f y)) eq

from : f ⁻¹ z → map-f ⁻¹ (x , z)
from (y , eq) = (x , y) , cong (_,_ x) eq

to∘from : ∀ p → to (from p) ≡ p
to∘from (y , eq) = elim¹
(λ {z′} (eq : f y ≡ z′) →
_≡_ {A = ∃ λ (y : P x) → f y ≡ z′}
(elim¹ to-P (y , refl (f y)) (cong (_,_ x) eq))
(y , eq))
(elim¹ to-P (y , refl (f y)) (cong (_,_ x) (refl (f y)))  ≡⟨ cong (elim¹ to-P (y , refl (f y))) \$
cong-refl (_,_ x) ⟩
elim¹ to-P (y , refl (f y)) (refl (x , f y))             ≡⟨ elim¹-refl to-P _ ⟩∎
(y , refl (f y))                                         ∎)
eq

surj : map-f ⁻¹ (x , z) ↠ f ⁻¹ z
surj = record
{ logical-equivalence = record { to = to; from = from }
; right-inverse-of    = to∘from
}

-- A "computation" rule for drop-Σ-map-id.

inverse-drop-Σ-map-id :
{A : Type a} {P : A → Type p} {Q : A → Type q}
{f : ∀ {x} → P x → Q x} {x : A} {y : Q x}
{eq : Is-equivalence {A = Σ A P} {B = Σ A Q} (Σ-map P.id f)} →
inverse (drop-Σ-map-id f eq x) y ≡
subst P (cong proj₁ (right-inverse-of eq (x , y)))
(proj₂ (inverse eq (x , y)))
inverse-drop-Σ-map-id {P} {Q} {f} {x} {y} {eq} =

let lemma = elim¹
(λ {q′} eq →
cong proj₁
(proj₂ (other-singleton-contractible (Σ-map P.id f p′))
(q′ , eq)) ≡
eq)
(cong proj₁
(proj₂ (other-singleton-contractible (Σ-map P.id f p′))
(Σ-map P.id f p′ , refl _))                           ≡⟨ cong (cong proj₁) \$
other-singleton-contractible-refl _ ⟩

cong proj₁ (refl _)                                        ≡⟨ cong-refl _ ⟩∎

refl _                                                     ∎)
_
in
proj₁
(subst
(λ ((_ , y) , _) → f ⁻¹ y)
(proj₂
(other-singleton-contractible (Σ-map P.id f p′))
(q′ , right-inverse-of eq q′))
(proj₂ p′ , refl _))                                 ≡⟨ cong proj₁ \$ push-subst-pair _ _ ⟩

subst
(λ ((x , _) , _) → P x)
(proj₂
(other-singleton-contractible (Σ-map P.id f p′))
(q′ , right-inverse-of eq q′))
(proj₂ p′)                                              ≡⟨ trans (subst-∘ _ _ _) (subst-∘ _ _ _) ⟩

subst P
(cong proj₁ \$ cong proj₁ \$
proj₂
(other-singleton-contractible (Σ-map P.id f p′))
(q′ , right-inverse-of eq q′))
(proj₂ p′)                                              ≡⟨ cong (λ eq → subst P (cong proj₁ eq) (proj₂ p′))
lemma ⟩∎
subst P
(cong proj₁ (right-inverse-of eq q′))
(proj₂ p′)                                              ∎
where
q′ : ∃ Q
q′ = x , y

p′ : ∃ P
p′ = inverse eq q′

------------------------------------------------------------------------
-- _≃_

-- A notion of equivalence.

infix 4 _≃_

_≃_ : Type a → Type b → Type (a ⊔ b)
A ≃ B = ∃ λ (f : A → B) → Is-equivalence f

-- An identity equivalence.

id : A ≃ A
id = P.id , singleton-contractible

-- Equalities can be converted to equivalences.

≡⇒≃ : A ≡ B → A ≃ B
≡⇒≃ = elim (λ {A B} _ → A ≃ B) (λ _ → id)

-- If ≡⇒≃ is applied to reflexivity, then the result is equal to id.

≡⇒≃-refl : ≡⇒≃ (refl A) ≡ id
≡⇒≃-refl = elim-refl (λ {A B} _ → A ≃ B) (λ _ → id)

-- Univalence for fixed types.

Univalence′ : (A B : Type ℓ) → Type (lsuc ℓ)
Univalence′ A B = Is-equivalence (≡⇒≃ {A = A} {B = B})

-- Univalence.

Univalence : ∀ ℓ → Type (lsuc ℓ)
Univalence ℓ = {A B : Type ℓ} → Univalence′ A B
```