------------------------------------------------------------------------
-- Quotients
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

-- Partly based on the presentation of quotients in the HoTT book.
-- Perhaps that presentation is partly based on work by Voevodsky.

-- The generalisation from propositional equivalence relations to
-- "strong" equivalence relations is my own. In light of the results
-- below I see little use for this generalisation…

open import Equality

module Quotient {r} (eq :  {a p}  Equality-with-J a p r) where

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection eq as Bij using (_↔_)
open import Bool eq
private
module D = Derived-definitions-and-properties eq
open D hiding (elim)
open import Equality.Decidable-UIP eq using (Constant)
open import Equality.Decision-procedures eq
import Equality.Groupoid eq as EG
open import Equivalence eq as Eq using (_≃_)
open import Fin eq
open import Function-universe eq as F hiding (_∘_)
open import Groupoid
open import H-level eq as H-level
open import H-level.Closure eq
open import H-level.Truncation eq as Trunc hiding (rec)
open import Nat eq as Nat
open import Univalence-axiom eq

------------------------------------------------------------------------
-- Equivalence relations

-- The definition of an equivalence relation.

record Is-equivalence-relation
{a r} {A : Set a} (R : A  A  Set r) : Set (a  r) where
field
reflexive  :  {x}  R x x
symmetric  :  {x y}  R x y  R y x
transitive :  {x y z}  R x y  R y z  R x z

------------------------------------------------------------------------
-- Strong equivalence relations

-- A strengthening of the concept of "equivalence relation".

Strong-equivalence :  {a r} {A : Set a}
(A  A  Set r)  Set (a  lsuc r)
Strong-equivalence R =  {x y}  R x y  (R x  R y)

-- Strong equivalence relations are equivalence relations.

strong-equivalence⇒equivalence :
{a r} {A : Set a} {R : A  A  Set r}
Strong-equivalence R
Is-equivalence-relation R
strong-equivalence⇒equivalence {R = R} strong-equivalence = record
{ reflexive = λ {x}
\$⟨ refl (R x)
R x  R x  ↝⟨ _≃_.from strong-equivalence ⟩□
R x x
; symmetric = λ {x y}
R x y      ↝⟨ _≃_.to strong-equivalence
R x  R y  ↝⟨ sym
R y  R x  ↝⟨ _≃_.from strong-equivalence ⟩□
R y x
; transitive = λ {x y z} Rxy Ryz
_≃_.from strong-equivalence (
R x  ≡⟨ _≃_.to strong-equivalence Rxy
R y  ≡⟨ _≃_.to strong-equivalence Ryz ⟩∎
R z  )
}

-- A relation that is an equivalence relation, and a family of
-- propositions, is a strong equivalence relation (assuming
-- extensionality and univalence).

propositional-equivalence⇒strong-equivalence :
{a r} {A : Set a} {R : A  A  Set r}
Extensionality (a  r) (lsuc r)
Univalence r
Is-equivalence-relation R
(∀ x y  Is-proposition (R x y))
Strong-equivalence R
propositional-equivalence⇒strong-equivalence
{a} {r} {R = R} ext univ R-equiv R-prop {x = x} {y = y} =

Eq.↔⇒≃ (record
{ surjection = record
{ logical-equivalence = record
{ to = λ Rxy  apply-ext (lower-extensionality r lzero ext) λ z
≃⇒≡ univ \$
_↔_.to (Eq.⇔↔≃ (lower-extensionality a _ ext)
(R-prop x z) (R-prop y z))
(R x z  ↝⟨ record { to   = transitive (symmetric Rxy)
; from = transitive Rxy
} ⟩□
R y z  )
; from = λ Rx≡Ry         \$⟨ reflexive
R y y  ↝⟨ subst (_\$ y) (sym Rx≡Ry) ⟩□
R x y
}
; right-inverse-of = λ _
_⇔_.to propositional⇔irrelevant
(H-level.respects-surjection
(_≃_.surjection \$ Eq.extensionality-isomorphism
(lower-extensionality r lzero ext))
1 \$
Π-closure (lower-extensionality r lzero ext) 1 λ z
H-level-H-level-≡ˡ
(lower-extensionality a _ ext)
univ 0 (R-prop x z))
_ _
}
; left-inverse-of = λ _
_⇔_.to propositional⇔irrelevant (R-prop x y) _ _
})
where
open Is-equivalence-relation R-equiv

-- _≡_ is a strong equivalence relation (assuming extensionality and
-- univalence).

equality-strong-equivalence :
{a} {A : Set a}
Extensionality a (lsuc a)
Univalence a
Strong-equivalence (_≡_ {A = A})
equality-strong-equivalence ext univ {x = x} {y = y} =
x  y                      ↔⟨ inverse \$ Π≡≃≡-↔-≡ (lower-extensionality lzero _ ext) _ _
(∀ z  (z  x)  (z  y))  ↝⟨ (∀-cong (lower-extensionality lzero _ ext) λ _  Eq.↔⇒≃ \$
Eq.≃-preserves-bijections (lower-extensionality lzero _ ext)
(Groupoid.⁻¹-bijection (EG.groupoid _))
(Groupoid.⁻¹-bijection (EG.groupoid _)))
(∀ z  (x  z)  (y  z))  ↝⟨ (∀-cong ext λ _  inverse \$ ≡≃≃ univ)
(∀ z  (x  z)  (y  z))  ↝⟨ Eq.extensionality-isomorphism ext ⟩□
(x ≡_)  (y ≡_)

-- If λ (_ _ : ⊤) → Fin n is a strong equivalence relation, then n is
-- equal to n ! (assuming extensionality and univalence).

const-Fin-strong-equivalence⇒≡! :
Extensionality (# 0) (# 1)
Univalence (# 0)
n  Strong-equivalence  (_ _ : )  Fin n)  n  n !
const-Fin-strong-equivalence⇒≡! ext univ n strong-equivalence =
_⇔_.to isomorphic-same-size (
Fin n                          ↔⟨ strong-equivalence
const (Fin n)  const (Fin n)  ↔⟨ inverse \$ Eq.extensionality-isomorphism ext
(  Fin n  Fin n)            ↝⟨ Π-left-identity
Fin n  Fin n                  ↝⟨ [Fin≡Fin]↔Fin! (lower-extensionality _ _ ext) univ n
Fin (n !)                      )

-- Thus there is at least one equivalence relation that is not a
-- strong equivalence relation (assuming extensionality and
-- univalence).

equivalence-but-not-strong-equivalence :
Extensionality (# 0) (# 1)
Univalence (# 0)
λ (A : Set)
λ (R : A  A  Set)
(∀ {x}  R x x) ×
(∀ {x y}  R x y  R y x) ×
(∀ {x y z}  R x y  R y z  R x z) ×
¬ Strong-equivalence R
equivalence-but-not-strong-equivalence ext univ =
A , R , rfl , sm , trns , not-strong-equivalence
where
A : Set
A =

R : A  A  Set
R _ _ = Fin 3

rfl :  {x}  R x x
rfl = fzero

sm :  {x y}  R x y  R y x
sm _ = fzero

trns :  {x y z}  R x y  R y z  R x z
trns _ _ = fzero

not-strong-equivalence : ¬ Strong-equivalence R
not-strong-equivalence =
Strong-equivalence R  ↝⟨ const-Fin-strong-equivalence⇒≡! ext univ 3
3  3 !               ↝⟨ from-⊎ (3 Nat.≟ (3 !)) ⟩□

-- On the other hand, if n is 2, then λ (_ _ : ⊤) → Fin n is a strong
-- equivalence relation (assuming extensionality and univalence).

const-Fin-2-strong-equivalence :
Extensionality (# 0) (# 1)
Univalence (# 0)  Strong-equivalence  (_ _ : )  Fin 2)
const-Fin-2-strong-equivalence ext univ =
Fin 2                          ↔⟨ inverse \$ [Fin≡Fin]↔Fin! (lower-extensionality _ _ ext) univ 2
Fin 2  Fin 2                  ↔⟨ inverse Π-left-identity
(  Fin 2  Fin 2)            ↝⟨ Eq.extensionality-isomorphism ext ⟩□
const (Fin 2)  const (Fin 2)

-- Thus there is at least one example of a strong equivalence relation
-- that is neither propositional nor the identity type (assuming
-- extensionality and univalence).

strong-equivalence-that-is-neither-propositional-nor-≡ :
Extensionality (# 0) (# 1)
Univalence (# 0)
λ (A : Set)
λ (R : A  A  Set)
Strong-equivalence R ×
¬ (∀ x y  Is-proposition (R x y)) ×
¬ (∀ x y  R x y  (x  y))
strong-equivalence-that-is-neither-propositional-nor-≡ ext univ =
,  _ _  Fin 2) , const-Fin-2-strong-equivalence ext univ ,
is-prop                    \$⟨ is-prop _ _
Is-proposition (    )  ↝⟨ H-level.respects-surjection (_↔_.surjection \$ inverse Bool↔Fin2) 1
Is-proposition Bool         ↝⟨ ¬-Bool-propositional ⟩□
) ,
≃≡  let eq = ≃≡ tt tt in
⊎.inj₁≢inj₂ (
fzero                                 ≡⟨ sym \$ _≃_.left-inverse-of eq _
_≃_.from eq (_≃_.to eq fzero)         ≡⟨ cong (_≃_.from eq) \$
_⇔_.to propositional⇔irrelevant
(mono (zero≤ 2) ⊤-contractible _ _)
_ _
_≃_.from eq (_≃_.to eq (fsuc fzero))  ≡⟨ _≃_.left-inverse-of eq _ ⟩∎
fsuc fzero                            ))

-- It is not in general the case that, if R is a strong equivalence
-- relation, then R on f is a strong equivalence relation (assuming
-- extensionality and univalence).

strong-equivalence-not-closed-under-on :
Extensionality (# 1) (# 2)
Univalence (# 1)
Univalence (# 0)
λ (A : Set₁)
λ (B : Set₁)
λ (R : A  A  Set₁)
λ (f : B  A)
Strong-equivalence R ×
¬ Strong-equivalence (R on f)
strong-equivalence-not-closed-under-on ext univ₁ univ₀ =
Set ,  _  , _≡_ , const (Fin 3) ,
equality-strong-equivalence ext univ₁ ,
not-strong-equivalence
where
not-strong-equivalence : ¬ Strong-equivalence (_≡_ on const (Fin 3))
where
3!≡3!! = _⇔_.to isomorphic-same-size (
Fin (3 !)                                      ↝⟨ inverse \$ [Fin≡Fin]↔Fin! (lower-extensionality _ _ ext) univ₀ 3
Fin 3  Fin 3                                  ↔⟨ strong-equivalence
const (Fin 3  Fin 3)  const (Fin 3  Fin 3)  ↔⟨ inverse \$ Eq.extensionality-isomorphism ext
( _   (Fin 3  Fin 3)  (Fin 3  Fin 3))    ↝⟨ →-cong ext Bij.↑↔ F.id
(  (Fin 3  Fin 3)  (Fin 3  Fin 3))        ↝⟨ Π-left-identity
(Fin 3  Fin 3)  (Fin 3  Fin 3)              ↔⟨ ≡-preserves-≃ (lower-extensionality lzero _ ext) univ₁ univ₀
(Eq.↔⇒≃ \$ [Fin≡Fin]↔Fin! (lower-extensionality _ _ ext) univ₀ 3)
(Eq.↔⇒≃ \$ [Fin≡Fin]↔Fin! (lower-extensionality _ _ ext) univ₀ 3)
Fin (3 !)  Fin (3 !)                          ↝⟨ [Fin≡Fin]↔Fin! (lower-extensionality _ _ ext) univ₀ (3 !) ⟩□
Fin (3 ! !)                                    )

contradiction = from-⊎ ((3 !) Nat.≟ (3 ! !)) 3!≡3!!

-- However, Strong-equivalence is closed under _on f when f is an
-- equivalence (assuming extensionality).

strong-equivalence-closed-under-on :
{a b r} {A : Set a} {B : Set b} {R : A  A  Set r}
Extensionality (a  b) (lsuc r)
(B≃A : B  A)
Strong-equivalence R
Strong-equivalence (R on _≃_.to B≃A)
strong-equivalence-closed-under-on
{a} {b} {R = R} ext B≃A strong-equivalence {x} {y} =

R (f x) (f y)                                  ↝⟨ strong-equivalence
R (f x)  R (f y)                              ↝⟨ F.id
z  R (f x)    z)    z  R (f y)    z)   ↝⟨ inverse \$ Eq.extensionality-isomorphism
(lower-extensionality b lzero ext)
(∀ z  R (f x)    z           R (f y)    z)   ↝⟨ (Π-cong ext (inverse B≃A) λ z
≡⇒≃ \$ cong₂ _≡_ (lemma x z) (lemma y z))
(∀ z  R (f x) (f z)          R (f y) (f z))  ↝⟨ Eq.extensionality-isomorphism
(lower-extensionality a lzero ext)
z  R (f x) (f z))   z  R (f y) (f z))  ↝⟨ F.id ⟩□
(R on f) x  (R on f) y
where
f   = _≃_.to   B≃A
f⁻¹ = _≃_.from B≃A

lemma = λ x z
R (f x) z            ≡⟨ cong (R (f x)) \$ sym \$ _≃_.right-inverse-of B≃A _ ⟩∎
R (f x) (f (f⁻¹ z))

-- Various closure properties related to _×_ and _⊎_ fail to hold for
-- Strong-equivalence (assuming extensionality and univalence).

strong-equivalence-not-closed-under-×-or-⊎ :
Extensionality (# 0) (# 1)
Univalence (# 0)
λ (A : Set)
λ (R₁ : A  A  Set)
λ (R₂ : A  A  Set)
Strong-equivalence R₁ ×
Strong-equivalence R₂ ×
¬ Strong-equivalence  x y  R₁ x y × R₂ x y) ×
¬ Strong-equivalence  x y  R₁ x y  R₂ x y) ×
¬ Strong-equivalence  x y  R₁ (proj₁ x) (proj₁ y) ×
R₂ (proj₂ x) (proj₂ y)) ×
¬ Strong-equivalence  x y  R₁ (proj₁ x) (proj₁ y)
R₂ (proj₂ x) (proj₂ y))
strong-equivalence-not-closed-under-×-or-⊎ ext univ =
, R , R ,
strong-equivalence , strong-equivalence ,
not-strong-equivalence  (Fin×Fin↔Fin* 2 2) ,
not-strong-equivalence  (Fin⊎Fin↔Fin+ 2 2) ,
not-strong-equivalence′ (Fin×Fin↔Fin* 2 2) ,
not-strong-equivalence′ (Fin⊎Fin↔Fin+ 2 2)
where
R :     Set
R = λ _ _  Fin 2

strong-equivalence : Strong-equivalence R
strong-equivalence =
proj₁ \$ proj₂ \$ proj₂ \$
strong-equivalence-that-is-neither-propositional-nor-≡ ext univ

not-strong-equivalence :
{B : Set}
B  Fin 4
¬ Strong-equivalence  (_ _ : )  B)
not-strong-equivalence {B} B↔Fin4 =
Strong-equivalence  _ _  B)      ↝⟨ (≡⇒↝ _ \$ cong Strong-equivalence \$ apply-ext ext λ _  apply-ext ext λ _
≃⇒≡ univ \$ Eq.↔⇒≃ B↔Fin4)
Strong-equivalence  _ _  Fin 4)  ↝⟨ const-Fin-strong-equivalence⇒≡! ext univ 4
4  4 !                             ↝⟨ from-⊎ (4 Nat.≟ (4 !)) ⟩□

not-strong-equivalence′ :
{B : Set}
B  Fin 4
¬ Strong-equivalence  (_ _ :  × )  B)
not-strong-equivalence′ {B} B↔Fin4 =
Strong-equivalence  (_ _ :  × )  B)  ↝⟨  se {_ _}
B                                           ↝⟨ se {y = _}
const B  const B                           ↝⟨ inverse \$ Eq.extensionality-isomorphism ext
( ×   B  B)                             ↔⟨ →-cong ext ×-right-identity F.id
(  B  B)                                 ↝⟨ Eq.extensionality-isomorphism ext ⟩□
const B  const B                           )
Strong-equivalence  (_ _ : )      B)  ↝⟨ not-strong-equivalence B↔Fin4 ⟩□

-- Is the following a strong equivalence relation?
--
--   R (x , _) (y , _) = x ≡ y
--
-- (This is a combination of equality and the trivial relation, both
-- of which are strong equivalence relations.)
--
-- Answer: No, not in general (assuming extensionality and
-- univalence).

another-negative-result :
Extensionality (# 1) (# 2)
Univalence (# 1)
Univalence (# 0)
λ (A : Set₁)
λ (B : Set)
¬ Strong-equivalence {A = A × B} (_≡_ on proj₁)
another-negative-result ext univ₁ univ₀ =
Set , Fin 2 , not-strong-equivalence
where
not-strong-equivalence : ¬ Strong-equivalence (_≡_ on proj₁)
where
4≡2 = _⇔_.to isomorphic-same-size (
Fin 4                                                        ↝⟨ inverse \$ [Fin→Fin]↔Fin^ (lower-extensionality _ _ ext) 2 2
(Fin 2  Fin 2)                                              ↝⟨ →-cong (lower-extensionality _ _ ext) F.id \$ inverse \$
[Fin≡Fin]↔Fin! (lower-extensionality _ _ ext) univ₀ 2
(Fin 2  Fin 2  Fin 2)                                      ↔⟨ →-cong (lower-extensionality _ lzero ext) F.id \$
equality-strong-equivalence ext univ₁
(Fin 2   A  Fin 2        A)   A  Fin 2        A))  ↔⟨ →-cong (lower-extensionality _ lzero ext) F.id \$ inverse \$
Eq.extensionality-isomorphism ext
(Fin 2   A  (Fin 2        A)        (Fin 2        A))  ↝⟨ Π-comm
(∀ A  Fin 2  (Fin 2        A)        (Fin 2        A))  ↝⟨ inverse currying
(∀ A          (Fin 2  proj₁ A)        (Fin 2  proj₁ A))  ↔⟨ Eq.extensionality-isomorphism ext
A           Fin 2  proj₁ A)   A  Fin 2  proj₁ A)   ↔⟨ inverse \$ strong-equivalence {x = _ , fzero} {y = _ , fzero}
Fin 2  Fin 2                                                ↝⟨ [Fin≡Fin]↔Fin! (lower-extensionality _ _ ext) univ₀ 2 ⟩□
Fin 2                                                        )

contradiction = from-⊎ (4 Nat.≟ 2) 4≡2

------------------------------------------------------------------------
-- Quotients

-- Equivalence classes.

_is-equivalence-class-of_ :
{a} {A : Set a}
(A  Set a)  (A  A  Set a)  Set (lsuc (lsuc a))
_is-equivalence-class-of_ {a} P R =
( λ x  R x  P)  1 (lsuc a)

-- Quotients.

infix 5 _/_

_/_ :  {a} (A : Set a)  (A  A  Set a)  Set (lsuc (lsuc a))
A / R =  λ (P : A  Set _)  P is-equivalence-class-of R

-- Quotienting with equality amounts to the same thing as not
-- quotienting at all (assuming extensionality and univalence).

/≡↔ :
{a} {A : Set a}
Extensionality (lsuc (lsuc a)) (lsuc a)
Univalence a
A / _≡_  A
/≡↔ {A = A} ext univ =
( λ P   ( λ x  (x ≡_)  P)  1 _)  ↝⟨ (∃-cong λ _  ∥∥↔ lzero ext \$ _⇔_.from propositional⇔irrelevant irr)
( λ P   λ x  (x ≡_)  P)            ↝⟨ ∃-comm
( λ x   λ P  (x ≡_)  P)            ↝⟨ drop-⊤-right  _  _⇔_.to contractible⇔↔⊤ \$ other-singleton-contractible _) ⟩□
A
where
se = equality-strong-equivalence
(lower-extensionality _ lzero ext) univ

se-refl :
x  _≃_.to se (refl x)  refl (x ≡_)
se-refl x = _≃_.from-to se (
sym (_≃_.to (≡⇒↝ _ (cong (_\$ x) (refl (x ≡_)))) (sym (refl x)))  ≡⟨ cong  p  sym (_≃_.to (≡⇒↝ _ p) (sym (refl x)))) \$ cong-refl _
sym (_≃_.to (≡⇒↝ _ (refl (x  x))) (sym (refl x)))               ≡⟨ cong  eq  sym (_≃_.to eq (sym (refl x)))) ≡⇒↝-refl
sym (sym (refl x))                                               ≡⟨ sym-sym _ ⟩∎
refl x                                                           )

lemma :
{x y : A} (p : (x ≡_)  (y ≡_))
cong _≡_ (subst (_\$ x) p (refl x))  sym p
lemma {x = x} p =
cong _≡_ (subst (_\$ x) p (refl x))                            ≡⟨ cong  p  cong _≡_ (subst (_\$ x) p (refl x))) \$ sym \$
_≃_.right-inverse-of se _
cong _≡_ (subst (_\$ x) (_≃_.to se (_≃_.from se p)) (refl x))  ≡⟨ D.elim  p  cong _≡_ (subst (_\$ _) (_≃_.to se p) (refl _))
sym (_≃_.to se p))
x
cong _≡_ (subst (_\$ x) (_≃_.to se (refl x)) (refl x))                  ≡⟨ cong  p  cong _≡_ (subst (_\$ x) p (refl x))) \$ se-refl x
cong _≡_ (subst (_\$ x) (refl (x ≡_)) (refl x))                         ≡⟨ cong (cong _≡_) \$ subst-refl _ _
cong _≡_ (refl x)                                                      ≡⟨ cong-refl _
refl (x ≡_ )                                                           ≡⟨ sym sym-refl
sym (refl (x ≡_ ))                                                     ≡⟨ cong sym \$ sym \$ se-refl x ⟩∎
sym (_≃_.to se (refl x))                                               )
(_≃_.from se p)
sym (_≃_.to se (_≃_.from se p))                               ≡⟨ cong sym \$ _≃_.right-inverse-of se _ ⟩∎
sym p

irr :  {P} (p q :  λ x  (x ≡_)  P)  p  q
irr {P} (x , x≡≡) (y , y≡≡) =
Σ-≡,≡→≡
(_≃_.from se ((x ≡_)  ≡⟨ x≡≡
P       ≡⟨ sym y≡≡ ⟩∎
(y ≡_)  ))

(subst  x  (x ≡_)  P)
(_≃_.from se (trans x≡≡ (sym y≡≡)))
x≡≡                                                        ≡⟨⟩

subst  x  (x ≡_)  P)
(sym \$ _≃_.to (≡⇒↝ _ (cong (_\$ x) (trans x≡≡ (sym y≡≡))))
(sym (refl x)))
x≡≡                                                        ≡⟨ cong  eq  subst  x  (x ≡_)  P) (sym eq) x≡≡) \$ sym \$
subst-in-terms-of-≡⇒↝ equivalence _ _ _
subst  x  (x ≡_)  P)
(sym \$ subst (_\$ x) (trans x≡≡ (sym y≡≡)) (sym (refl x)))
x≡≡                                                        ≡⟨ cong  eq  subst  x  (x ≡_)  P)
(sym (subst (_\$ x) (trans x≡≡ (sym y≡≡)) eq)) _)
sym-refl
subst  x  (x ≡_)  P)
(sym \$ subst (_\$ x) (trans x≡≡ (sym y≡≡)) (refl x))
x≡≡                                                        ≡⟨ subst-∘ _ _ _

subst  Q  Q  P)
(cong _≡_ \$
sym \$ subst (_\$ x) (trans x≡≡ (sym y≡≡)) (refl x))
x≡≡                                                        ≡⟨ cong  eq  subst  Q  Q  P) eq _) \$ cong-sym _ _

subst  Q  Q  P)
(sym \$ cong _≡_ \$
subst (_\$ x) (trans x≡≡ (sym y≡≡)) (refl x))
x≡≡                                                        ≡⟨ subst-trans _

trans (cong _≡_ \$ subst (_\$ x) (trans x≡≡ (sym y≡≡)) (refl x))
x≡≡                                                        ≡⟨ cong (flip trans x≡≡) \$ lemma _

trans (sym (trans x≡≡ (sym y≡≡))) x≡≡                            ≡⟨ cong (flip trans x≡≡) \$ sym-trans _ _

trans (trans (sym (sym y≡≡)) (sym x≡≡)) x≡≡                      ≡⟨ trans-[trans-sym]- _ _

sym (sym y≡≡)                                                    ≡⟨ sym-sym _ ⟩∎

y≡≡                                                              )

module _ {a} {A : Set a} {R : A  A  Set a} where

-- Equality characterisation lemmas for the quotient type.

equality-characterisation₁ :
Extensionality (lsuc (lsuc a)) (lsuc a)
{x y : A / R}
x  y

proj₁ x  proj₁ y
equality-characterisation₁ ext {x} {y} =
x  y                                                          ↝⟨ inverse Bij.Σ-≡,≡↔≡

( λ (eq : proj₁ x  proj₁ y)
subst (_is-equivalence-class-of R) eq (proj₂ x)  proj₂ y)  ↝⟨ (drop-⊤-right λ _  _⇔_.to contractible⇔↔⊤ \$
truncation-has-correct-h-level 1 ext _ _) ⟩□
proj₁ x  proj₁ y

equality-characterisation₂ :
Extensionality (lsuc (lsuc a)) (lsuc a)
{x y : A / R}
x  y

(∀ z  proj₁ x z  proj₁ y z)
equality-characterisation₂ ext {x} {y} =
x  y                          ↝⟨ equality-characterisation₁ ext

proj₁ x  proj₁ y              ↔⟨ inverse \$ Eq.extensionality-isomorphism
(lower-extensionality _ lzero ext) ⟩□
(∀ z  proj₁ x z  proj₁ y z)

equality-characterisation₃ :
Extensionality (lsuc (lsuc a)) (lsuc a)
Univalence a
{x y : A / R}
x  y

(∀ z  proj₁ x z  proj₁ y z)
equality-characterisation₃ ext univ {x} {y} =
x  y                          ↝⟨ equality-characterisation₂ ext

(∀ z  proj₁ x z  proj₁ y z)  ↔⟨ (∀-cong (lower-extensionality _ lzero ext) λ _
≡≃≃ univ) ⟩□
(∀ z  proj₁ x z  proj₁ y z)

-- Constructor for the quotient type.

[_] : A  A / R
[ a ] = R a ,  (a , refl (R a))

-- [_] is surjective (assuming extensionality).

[]-surjective :
Extensionality (lsuc (lsuc a)) (lsuc a)
Surjective (lsuc a) [_]
[]-surjective ext (P , P-is-class) =
∥∥-map
(Σ-map
F.id
{x} Rx≡P
[ x ]             ≡⟨ _↔_.from (equality-characterisation₁ ext) Rx≡P ⟩∎
(P , P-is-class)  ))
P-is-class

-- If the relation is a family of types of h-level n, then the
-- equivalence classes are also families of types of h-level n
-- (assuming extensionality).

equivalence-classes-have-same-h-level-as-relation :
Extensionality a a
n
(∀ x y  H-level n (R x y))
(x : A / R)   y  H-level n (proj₁ x y)
equivalence-classes-have-same-h-level-as-relation
ext n h (P , P-is-class) y =

Trunc.rec
(H-level-propositional ext n)
{ (z , Rz≡P)  H-level.respects-surjection
(≡⇒↝ _ (R z y  ≡⟨ cong (_\$ y) Rz≡P ⟩∎
P y    ))
n
(h z y) })
(with-lower-level _ P-is-class)

-- If R is a family of types of h-level n, then A / R has h-level
-- 1 + n (assuming extensionality and univalence).

quotient's-h-level-is-1-+-relation's-h-level :
Extensionality (lsuc (lsuc a)) (lsuc a)
Univalence a
Univalence (# 0)
n
(∀ x y  H-level n (R x y))
H-level (1 + n) (A / R)
quotient's-h-level-is-1-+-relation's-h-level ext univ univ₀ = h′
where
lemma₁ :
n
(∀ x y z  H-level n (proj₁ x z  proj₁ y z))
H-level (1 + n) (A / R)
lemma₁ n h x y =                             \$⟨ h x y
(∀ z  H-level n (proj₁ x z  proj₁ y z))  ↝⟨ Π-closure (lower-extensionality _ lzero ext) n
H-level n (∀ z  proj₁ x z  proj₁ y z)    ↝⟨ H-level.respects-surjection
(_↔_.surjection (inverse \$ equality-characterisation₂ ext))
n ⟩□
H-level n (x  y)

lemma₂ :
n
(∀ x y  H-level (1 + n) (R x y))
x y z  H-level (1 + n) (proj₁ x z  proj₁ y z)
lemma₂ n h x _ z =
H-level-H-level-≡ˡ
(lower-extensionality _ _ ext) univ n
(equivalence-classes-have-same-h-level-as-relation
(lower-extensionality _ _ ext) (1 + n) h x z)

h′ :  n
(∀ x y  H-level n (R x y))
H-level (1 + n) (A / R)
h′ (suc n) h = lemma₁ (suc n) (lemma₂ n h)
h′ zero    h =
lemma₁ zero λ x y z
propositional⇒inhabited⇒contractible
(lemma₂ 0  x y  mono₁ 0 (h x y)) x y z)
(                       \$⟨ refl _
↝⟨ ≡-preserves-≃ (lower-extensionality _ _ ext) univ₀ univ
(lemma₃ x z) (lemma₃ y z)
proj₁ x z  proj₁ y z  )
where
lemma₃ :  x z    proj₁ x z
lemma₃ x z =                \$⟨ equivalence-classes-have-same-h-level-as-relation
(lower-extensionality _ _ ext)
0 h x z
Contractible (proj₁ x z)  ↝⟨ _⇔_.to contractible⇔↔⊤
proj₁ x z               ↝⟨ inverse
proj₁ x z             ↝⟨ Eq.↔⇒≃ ⟩□
proj₁ x z

-- If the relation is a strong equivalence relation, then it is
-- isomorphic to equality under [_] (assuming extensionality).

related↔[equal] :
Extensionality (lsuc (lsuc a)) (lsuc a)
Strong-equivalence R
{x y}  R x y  [ x ]  [ y ]
related↔[equal] ext strong-equivalence {x} {y} =
R x y          ↔⟨ strong-equivalence
R x  R y      ↝⟨ inverse \$ equality-characterisation₁ ext ⟩□
[ x ]  [ y ]

-- If the relation is a strong equivalence relation, then functions
-- from quotients to sets are isomorphic to relation-respecting
-- functions (assuming extensionality).

/→set↔relation-respecting :
Extensionality (lsuc (lsuc a)) (lsuc (lsuc a))
Strong-equivalence R
{B : Set a}
Is-set B
(A / R  B)   λ (f : A  B)   x y  R x y  f x  f y
/→set↔relation-respecting ext strong-equivalence {B = B} B-set =

(( λ P   ( λ x  R x  P)  1 _)  B)             ↝⟨ currying

(∀ P   ( λ x  R x  P)  1 _  B)                 ↔⟨ (∀-cong (lower-extensionality _ lzero ext) λ P  inverse \$
constant-function≃∥inhabited∥⇒inhabited
lzero (lower-extensionality lzero _ ext) B-set)
(∀ P   λ (f : ( λ x  R x  P)  B)  Constant f)  ↝⟨ (∀-cong (lower-extensionality _ _ ext) λ _
Σ-cong currying λ _  F.id)
(∀ P   λ (f : (x : A)  R x  P  B)
Constant (uncurry f))                      ↝⟨ ΠΣ-comm

( λ (f :  P  (x : A)  R x  P  B)
P  Constant (uncurry (f P)))                    ↝⟨ Σ-cong Π-comm  _  F.id)

( λ (f : (x : A)   P  R x  P  B)
P  Constant (uncurry (flip f P)))               ↝⟨ Σ-cong (∀-cong (lower-extensionality _ _ ext) λ _
inverse currying)  _
F.id)
( λ (f : (x : A)  ( λ P  R x  P)  B)
P  Constant (uncurry λ x eq  f x (P , eq)))    ↝⟨ inverse \$
Σ-cong (Bij.inverse \$
∀-cong (lower-extensionality _ _ ext) λ _
drop-⊤-left-Π (lower-extensionality _ _ ext) \$
_⇔_.to contractible⇔↔⊤ \$
other-singleton-contractible _)
lemma ⟩□
( λ (f : A  B)   x y  R x y  f x  f y)

where

lemma = λ f
(∀ x y  R x y  f x  f y)                                    ↔⟨ (∀-cong (lower-extensionality _ _ ext) λ x
∀-cong (lower-extensionality _ _ ext) λ y
→-cong (lower-extensionality _ _ ext) strong-equivalence F.id)
(∀ x y  R x  R y  f x  f y)                                ↝⟨ (∀-cong (lower-extensionality _ _ ext) λ _
∀-cong (lower-extensionality _ _ ext) λ _
→-cong (lower-extensionality _ _ ext)
(Groupoid.⁻¹-bijection (EG.groupoid _))
F.id)
(∀ x y  R y  R x  f x  f y)                                ↝⟨ (∀-cong (lower-extensionality _ _ ext) λ _
inverse currying)
(∀ x (q :  λ y  R y  R x)  f x  f (proj₁ q))              ↝⟨ (∀-cong (lower-extensionality _ _ ext) λ _
inverse \$ drop-⊤-left-Π (lower-extensionality _ _ ext) \$
_⇔_.to contractible⇔↔⊤ \$
other-singleton-contractible _)
(∀ x (Q :  λ P  R x  P) (q :  λ x  R x  proj₁ Q)
f x  f (proj₁ q))                                            ↝⟨ (∀-cong (lower-extensionality _ _ ext) λ _
currying)
(∀ x P  R x  P  (q :  λ x  R x  P)  f x  f (proj₁ q))  ↝⟨ Π-comm

(∀ P x  R x  P  (q :  λ x  R x  P)  f x  f (proj₁ q))  ↝⟨ (∀-cong (lower-extensionality _ _ ext) λ _
inverse currying)
(∀ P (p q :  λ x  R x  P)  f (proj₁ p)  f (proj₁ q))      ↝⟨ F.id

(∀ P  Constant (uncurry λ x _  f x))                         ↝⟨ (∀-cong (lower-extensionality _ _ ext) λ _
≡⇒↝ _ \$ cong Constant \$ apply-ext (lower-extensionality _ _ ext) λ _
sym \$ subst-const _) ⟩□
(∀ P  Constant (uncurry λ x _  subst (const B) _ (f x)))

-- "Computation rule" for /→set↔relation-respecting.

proj₁-to-/→set↔relation-respecting :
(ext : Extensionality (lsuc (lsuc a)) (lsuc (lsuc a)))
(strong-equivalence : Strong-equivalence R)
{B : Set a}
(B-set : Is-set B)
(f : A / R  B)
proj₁ (_↔_.to (/→set↔relation-respecting
ext strong-equivalence B-set) f)

f  [_]
proj₁-to-/→set↔relation-respecting ext _ {B} _ f =
apply-ext (lower-extensionality _ _ ext) λ x
subst (const B) (refl _) (f [ x ])  ≡⟨ subst-refl _ _ ⟩∎
f [ x ]

-- Recursor (used to eliminate into sets). The recursor uses
-- extensionality and reflexivity.

rec :
Extensionality (lsuc (lsuc a)) (lsuc a)
(∀ {x}  R x x)
(B : Set a)
Is-set B
(f : A  B)
(∀ {x y}  R x y  f x  f y)
A / R  B
rec ext refl B B-set f R⇒≡ (P , P-is-class) =
_≃_.to (constant-function≃∥inhabited∥⇒inhabited lzero ext B-set)
(f′ , f′-constant)
P-is-class
where
f′ : ( λ x  R x  P)  B
f′ (x , _) = f x

f′-constant : Constant f′
f′-constant (x₁ , Rx₁≡P) (x₂ , Rx₂≡P) = R⇒≡ (
\$⟨ refl
R x₂ x₂  ↝⟨ ≡⇒→ \$ cong  Q  Q x₂) Rx₂≡P
P x₂     ↝⟨ ≡⇒→ \$ cong  Q  Q x₂) \$ sym Rx₁≡P ⟩□
R x₁ x₂  )

private

-- The recursor's computation rule holds definitionally.

rec-[] :
(ext : Extensionality (lsuc (lsuc a)) (lsuc a))
(refl :  {x}  R x x)
(B : Set a)
(B-set : Is-set B)
(f : A  B)
(R⇒≡ :  {x y}  R x y  f x  f y)
(x : A)
rec ext refl B B-set f R⇒≡ [ x ]  f x
rec-[] _ _ _ _ _ _ _ = refl _

-- Eliminator (used to eliminate into sets). The eliminator uses
-- extensionality, and the assumption that the relation is a strong
-- equivalence relation. (The latter assumption could perhaps be
-- weakened.)

elim :
(ext : Extensionality (lsuc (lsuc a)) (lsuc a))
(strong-equivalence : Strong-equivalence R)
(B : A / R  Set (lsuc a))
(∀ x  Is-set (B x))
(f :  x  B [ x ])
(∀ {x y} (Rxy : R x y)
subst B (_↔_.to (related↔[equal]
ext strong-equivalence) Rxy) (f x)
f y)
x  B x
elim ext strong-equivalence B B-set f R⇒≡ (P , P-is-class) =
_≃_.to (constant-function≃∥inhabited∥⇒inhabited
lzero ext (B-set _))
(f′ , f′-constant)
P-is-class
where
f′ : ( λ x  R x  P)  B (P , P-is-class)
f′ (x , Rx≡P) =
subst B
(_↔_.from (equality-characterisation₁ ext) Rx≡P)
(f x)

f′-constant : Constant f′
f′-constant (x , Rx≡P) (y , Ry≡P) =
subst B
(_↔_.from (equality-characterisation₁ ext) Rx≡P)
(f x)                                                     ≡⟨ cong (subst _ _) \$ sym \$ R⇒≡ _

subst B
(_↔_.from (equality-characterisation₁ ext) Rx≡P)
(subst B (_↔_.to (related↔[equal]
ext strong-equivalence) lemma₁)
(f y))                                             ≡⟨ subst-subst _ _ _ _

subst B
(trans (_↔_.to (related↔[equal]
ext strong-equivalence) lemma₁)
(_↔_.from (equality-characterisation₁ ext) Rx≡P))
(f y)                                                     ≡⟨ cong  eq  subst B eq _) lemma₄ ⟩∎

subst B
(_↔_.from (equality-characterisation₁ ext) Ry≡P)
(f y)
where
lemma₁ = _≃_.from strong-equivalence (
R y  ≡⟨ Ry≡P
P    ≡⟨ sym Rx≡P ⟩∎
R x  )

lemma₂ = λ x
_↔_.to (equality-characterisation₁ ext) (refl x)  ≡⟨⟩
proj₁ (Σ-≡,≡←≡ (refl x))                          ≡⟨ proj₁-Σ-≡,≡←≡ _
cong proj₁ (refl x)                               ≡⟨ cong-refl _ ⟩∎
refl (proj₁ x)

lemma₃ =
trans (_≃_.to strong-equivalence lemma₁) Rx≡P                    ≡⟨⟩

trans (_≃_.to strong-equivalence
(_≃_.from strong-equivalence (trans Ry≡P (sym Rx≡P))))
Rx≡P                                                       ≡⟨ cong (flip trans _) \$ _≃_.right-inverse-of strong-equivalence _

trans (trans Ry≡P (sym Rx≡P)) Rx≡P                               ≡⟨ trans-[trans-sym]- _ _ ⟩∎

Ry≡P

lemma₄ =
trans (_↔_.to (related↔[equal] ext strong-equivalence) lemma₁)
(_↔_.from (equality-characterisation₁ ext) Rx≡P)          ≡⟨⟩

trans (_↔_.from (equality-characterisation₁ ext)
(_≃_.to strong-equivalence lemma₁))
(_↔_.from (equality-characterisation₁ ext) Rx≡P)          ≡⟨ Bij.trans-to-to≡to-trans
_ _  inverse \$ equality-characterisation₁ ext)
lemma₂
_↔_.from (equality-characterisation₁ ext)
(trans (_≃_.to strong-equivalence lemma₁) Rx≡P)        ≡⟨ cong (_↔_.from (equality-characterisation₁ ext)) lemma₃ ⟩∎

_↔_.from (equality-characterisation₁ ext) Ry≡P

------------------------------------------------------------------------
-- An example

module ⊤/2 where

-- What happens if we quotient the unit type by the "binary-valued
-- trivial relation"?

⊤/2 : Set₂
⊤/2 =  / λ _ _  Fin 2

-- The type is not a set (assuming extensionality and univalence).

not-a-set :
Extensionality (# 2) (# 1)
Univalence (# 0)
¬ Is-set ⊤/2
not-a-set ext univ =
Is-set ⊤/2                              ↝⟨ F.id
((x y : ⊤/2)  Is-proposition (x  y))  ↝⟨  prop  prop _ _)
Is-proposition ([ tt ]  [ tt ])        ↝⟨ H-level.respects-surjection
(_↔_.surjection \$ inverse \$
related↔[equal] ext
(const-Fin-2-strong-equivalence
(lower-extensionality _ lzero ext) univ))
1
Is-proposition (Fin 2)                  ↝⟨ H-level.respects-surjection (_↔_.surjection \$ inverse Bool↔Fin2) 1
Is-proposition Bool                     ↝⟨ ¬-Bool-propositional ⟩□

-- The type is a groupoid (assuming extensionality and univalence).

is-groupoid :
Extensionality (# 2) (# 1)
Univalence (# 0)
H-level 3 ⊤/2
is-groupoid ext univ =
quotient's-h-level-is-1-+-relation's-h-level
ext univ univ 2  _ _  Fin-set 2)

-- Every value in the quotient is merely equal to [ tt ] (assuming
-- extensionality).

∥≡[tt]∥ :
Extensionality (# 2) (# 1)
(x : ⊤/2)   x  [ tt ]  1 (# 1)
∥≡[tt]∥ ext x =           \$⟨ []-surjective ext x
× [ tt ]  x  1 _  ↝⟨ ∥∥-map (sym  proj₂) ⟩□
x  [ tt ]  1 _

-- The type is merely single-valued (assuming extensionality and a
-- resizing function for the propositional truncation).

merely-single-valued :
Extensionality (# 2) (# 2)
({A : Set₂}   A  1 (# 1)   A  1 (# 2))
(x y : ⊤/2)   x  y  1 (# 1)
merely-single-valued ext resize x y =
Trunc.rec
(truncation-has-correct-h-level 1 ext)
x≡[tt]  ∥∥-map  y≡[tt]  x       ≡⟨ x≡[tt]
[ tt ]  ≡⟨ sym y≡[tt] ⟩∎
y       )
(∥≡[tt]∥ ext′ y))
(resize (∥≡[tt]∥ ext′ x))
where
ext′ = lower-extensionality lzero _ ext

-- Every instance of the type's equality type is merely isomorphic
-- to Fin 2 (assuming extensionality, univalence, and a resizing
-- function for the propositional truncation).

∥≡↔2∥ :
Extensionality (# 2) (# 2)
Univalence (# 0)
({A : Set₂}   A  1 (# 1)   A  1 (# 2))
(x y : ⊤/2)   x  y  Fin 2  1 (# 1)
∥≡↔2∥ ext univ resize x y =
Trunc.rec
(truncation-has-correct-h-level 1 ext)
x≡[tt]
∥∥-map
y≡[tt]
x  y            ↝⟨ ≡⇒↝ _ \$ cong₂ _≡_ x≡[tt] y≡[tt]
[ tt ]  [ tt ]  ↝⟨ inverse \$
related↔[equal]
(lower-extensionality lzero _ ext)
(const-Fin-2-strong-equivalence
(lower-extensionality _ _ ext) univ) ⟩□
Fin 2            )
(∥≡[tt]∥ (lower-extensionality lzero _ ext) y))
(resize (∥≡[tt]∥ (lower-extensionality lzero _ ext) x))