Quotient.Families-of-equivalence-classes

------------------------------------------------------------------------
-- Quotients, defined as families of equivalence classes
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --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.Families-of-equivalence-classes
  {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 Equivalence-relation eq
open import Extensionality eq
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.Church eq as Trunc hiding (rec)
open import Nat eq as Nat
open import Surjection eq using (_↠_)
open import Univalence-axiom eq

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

mutual

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

  Strong-equivalence :
    ∀ {a r} {A : Type a} →
    (A → A → Type r) → Type (a ⊔ lsuc r)
  Strong-equivalence = Strong-equivalence-with equivalence

  -- A generalisation of "strong equivalence".

  Strong-equivalence-with :
    ∀ {a r} {A : Type a} →
    Kind → (A → A → Type r) → Type (a ⊔ lsuc r)
  Strong-equivalence-with k R = ∀ {x y} → R x y ↝[ k ] (R x ≡ R y)

-- Strong equivalence relations (with equivalence) are strong
-- equivalence relations with any kind.

strong-equivalence⇒strong-equivalence-with :
  ∀ {k a r} {A : Type a} {R : A → A → Type r} →
  Strong-equivalence R → Strong-equivalence-with k R
strong-equivalence⇒strong-equivalence-with strong-equivalence =
  from-equivalence strong-equivalence

-- Strong equivalence relations with logical equivalence are
-- equivalence relations.

strong-equivalence-with-⇔⇒equivalence :
  ∀ {a r} {A : Type a} {R : A → A → Type r} →
  Strong-equivalence-with logical-equivalence R →
  Is-equivalence-relation R
strong-equivalence-with-⇔⇒equivalence {R} strong-equivalence =
  record
    { reflexive = λ {x} →
                   $⟨ refl (R x) ⟩
        R x ≡ R x  ↝⟨ to-implication $ inverse strong-equivalence ⟩□
        R x x      □
    ; symmetric = λ {x y} →
        R x y      ↝⟨ to-implication strong-equivalence ⟩
        R x ≡ R y  ↝⟨ sym ⟩
        R y ≡ R x  ↝⟨ to-implication $ inverse strong-equivalence ⟩□
        R y x      □
    ; transitive = λ {x y z} Rxy Ryz →
       to-implication (inverse strong-equivalence) (
         R x  ≡⟨ to-implication strong-equivalence Rxy ⟩
         R y  ≡⟨ to-implication strong-equivalence Ryz ⟩∎
         R z  ∎)
    }

-- Strong equivalence relations are equivalence relations.

strong-equivalence⇒equivalence :
  ∀ {a r} {A : Type a} {R : A → A → Type r} →
  Strong-equivalence R →
  Is-equivalence-relation R
strong-equivalence⇒equivalence =
  strong-equivalence-with-⇔⇒equivalence ∘
  strong-equivalence⇒strong-equivalence-with

-- 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 : Type a} {R : A → A → Type 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} ext univ R-equiv R-prop {x} {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 = λ _ →
          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 = λ _ → 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 : Type a} →
  Extensionality a (lsuc a) →
  Univalence a →
  Strong-equivalence (_≡_ {A = A})
equality-strong-equivalence ext univ {x} {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 : Type) →
  ∃ λ (R : A → A → Type) →
    (∀ {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 : Type
  A = ⊤

  R : A → A → Type
  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 : Type) →
  ∃ λ (R : A → A → Type) →
    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) $
                                                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 : Type₁) →
  ∃ λ (B : Type₁) →
  ∃ λ (R : A → A → Type₁) →
  ∃ λ (f : B → A) →
    Strong-equivalence R ×
    ¬ Strong-equivalence (R on f)
strong-equivalence-not-closed-under-on ext univ₁ univ₀ =
  Type , ↑ _ ⊤ , _≡_ , const (Fin 3) ,
  equality-strong-equivalence ext univ₁ ,
  not-strong-equivalence
  where
  not-strong-equivalence : ¬ Strong-equivalence (_≡_ on const (Fin 3))
  not-strong-equivalence strong-equivalence = contradiction
    where
    3!≡3!! = _⇔_.to (isomorphic-same-size { n = 3 ! ! }) (
      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.↑↔ ⟩
      (⊤ → (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 : ⊥
    contradiction = from-⊎ ((3 !) Nat.≟ (3 ! !)) 3!≡3!!

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

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

  R (f x) (f y)                                  ↝⟨ strong-equivalence ⟩
  R (f x) ≡ R (f y)                              ↔⟨⟩
  (λ 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))  ↔⟨⟩
  (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 : Type) →
  ∃ λ (R₁ : A → A → Type) →
  ∃ λ (R₂ : A → A → Type) →
    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 : ⊤ → ⊤ → Type
  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 : Type} →
    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 : Type} →
    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 ⟩
        (⊤ → 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 : Type₁) →
  ∃ λ (B : Type) →
    ¬ Strong-equivalence {A = A × B} (_≡_ on proj₁)
another-negative-result ext univ₁ univ₀ =
  Type , Fin 2 , not-strong-equivalence
  where
  not-strong-equivalence : ¬ Strong-equivalence (_≡_ on proj₁)
  not-strong-equivalence strong-equivalence = contradiction
    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 : ⊥
    contradiction = from-⊎ (4 Nat.≟ 2) 4≡2

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

-- Equivalence classes.

_is-equivalence-class-of_ :
  ∀ {a} {A : Type a} →
  (A → Type a) → (A → A → Type a) → Type (lsuc (lsuc a))
_is-equivalence-class-of_ {a} P R =
  ∥ (∃ λ x → R x ≡ P) ∥ 1 (lsuc a)

-- Quotients.

infix 5 _/_

_/_ : ∀ {a} (A : Type a) → (A → A → Type a) → Type (lsuc (lsuc a))
A / R = ∃ λ (P : A → Type _) → 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 : Type a} →
  Extensionality (lsuc (lsuc a)) (lsuc a) →
  Univalence a →
  A / _≡_ ↔ A
/≡↔ {A} ext univ =
  (∃ λ P → ∥ (∃ λ x → (x ≡_) ≡ P) ∥ 1 _)  ↝⟨ (∃-cong λ _ → ∥∥↔ lzero ext 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} 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 : Type a} {R : A → A → Type 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
      1
      (Σ-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
      1
      (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 _ 1 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 with k, then it
  -- is k-related to equality under [_] (assuming extensionality).

  related↝[equal] :
    ∀ {k} →
    Extensionality (lsuc (lsuc a)) (lsuc a) →
    Strong-equivalence-with k R →
    ∀ {x y} → R x y ↝[ k ] [ 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 with a symmetric
  -- kind k, then functions from quotients to sets are k-related to
  -- relation-respecting functions (assuming extensionality).

  /→set↝relation-respecting :
    ∀ {k} →
    Extensionality (lsuc (lsuc a)) (lsuc (lsuc a)) →
    Strong-equivalence-with ⌊ k ⌋-sym R →
    {B : Type a} →
    Is-set B →
    (A / R → B)
      ↝[ ⌊ k ⌋-sym ]
    ∃ λ (f : A → B) → ∀ x y → R x y → f x ≡ f y
  /→set↝relation-respecting {k} ext strong-equivalence {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 λ _ → Bij.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 (forget-ext? ⌊ k ⌋-sym $ lower-extensionality _ _ ext) λ x →
                                                                         ∀-cong (forget-ext? ⌊ k ⌋-sym $ lower-extensionality _ _ ext) λ y →
                                                                         →-cong (forget-ext? ⌊ k ⌋-sym $ 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-Π {k = bijection} (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))      ↔⟨⟩

      (∀ P → Constant (uncurry λ x _ → f x))                         ↔⟨ (∀-cong (lower-extensionality _ _ ext) λ _ →
                                                                         ≡⇒↝ bijection $ 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 :
    ∀ {k}
    (ext : Extensionality (lsuc (lsuc a)) (lsuc (lsuc a)))
    (strong-equivalence : Strong-equivalence-with ⌊ k ⌋-sym R)
    {B : Type a}
    (B-set : Is-set B)
    (f : A / R → B) →
    proj₁ (to-implication
             (/→set↝relation-respecting ext strong-equivalence B-set) f)
      ≡
    f ∘ [_]
  proj₁-to-/→set↝relation-respecting ext eq {B} B-set f =
    apply-ext (lower-extensionality _ _ ext) (lemma _ eq)
    where
    lemma :
      ∀ k (eq : Strong-equivalence-with ⌊ k ⌋-sym R) x →
      proj₁
        (to-implication (/→set↝relation-respecting ext eq B-set) f)
        x
        ≡
      f [ x ]

    lemma logical-equivalence _ x =
      subst (const B) (refl _) (f [ x ])  ≡⟨ subst-refl _ _ ⟩∎
      f [ x ]                             ∎

    lemma bijection _ x =
      subst (const B) (refl _) (f [ x ])  ≡⟨ subst-refl _ _ ⟩∎
      f [ x ]                             ∎

    lemma equivalence _ x =
      subst (const B) (refl _) (f [ x ])  ≡⟨ subst-refl _ _ ⟩∎
      f [ x ]                             ∎

    lemma equivalenceᴱ _ 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 : Type 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 : Type 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 with split surjections".

  elim :
    (ext : Extensionality (lsuc (lsuc a)) (lsuc a))
    (strong-equivalence : Strong-equivalence-with surjection R)
    (B : A / R → Type (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                  ∎

  -- A variant of elim that can be used if the motive composed with
  -- [_] is a family of propositions.
  --
  -- I took the idea for this eliminator from Nicolai Kraus.

  elim-Prop :
    (ext : Extensionality (lsuc (lsuc a)) (lsuc a))
    (strong-equivalence : Strong-equivalence-with surjection R)
    (B : A / R → Type (lsuc a)) →
    (∀ x → Is-proposition (B [ x ])) →
    (f : ∀ x → B [ x ]) →
    ∀ x → B x
  elim-Prop ext strong-equivalence B B-prop f x = elim
    ext
    strong-equivalence
    B
    (elim
        ext
        strong-equivalence
        _
        (λ _ → mono₁ 1 $ H-level-propositional ext′ 2)
        (mono₁ 1 ∘ B-prop)
        (λ _ → H-level-propositional ext′ 2 _ _))
    f
    (λ _ → B-prop _ _ _)
    x
    where
    ext′ = lower-extensionality _ lzero ext

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

module ⊤/2 where

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

  ⊤/2 : Type₂
  ⊤/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                              ↝⟨ _⇔_.from (≡↔+ 1 _) ⟩
    ((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 1 (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 : Type₂} → ∥ A ∥ 1 (# 1) → ∥ A ∥ 1 (# 2)) →
    (x y : ⊤/2) → ∥ x ≡ y ∥ 1 (# 1)
  merely-single-valued ext resize x y =
    Trunc.rec
      1
      (truncation-has-correct-h-level 1 ext)
      (λ x≡[tt] → ∥∥-map 1
                         (λ 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 : Type₂} → ∥ A ∥ 1 (# 1) → ∥ A ∥ 1 (# 2)) →
    (x y : ⊤/2) → ∥ x ≡ y ↔ Fin 2 ∥ 1 (# 1)
  ∥≡↔2∥ ext univ resize x y =
    Trunc.rec
      1
      (truncation-has-correct-h-level 1 ext)
      (λ x≡[tt] →
         ∥∥-map
           1
           (λ 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))