------------------------------------------------------------------------
-- A variant of the set quotients from Quotient
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

-- Partly following the HoTT book.
--
-- Unlike the HoTT book, but following the cubical library (in which
-- set quotients were implemented by Zesen Qian and Anders Mörtberg),
-- the quotienting relations are not always required to be
-- propositional. Furthermore, unlike the code in the cubical library,
-- the set truncation constructor takes an argument stating that the
-- quotienting relation is propositional.

-- The module is parametrised by a notion of equality. The higher
-- constructors of the HIT defining quotients use path equality, but
-- the supplied notion of equality is used for many other things.

import Equality.Path as P

module Quotient.Set-truncated-if-propositional
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

private
  open module D = P.Derived-definitions-and-properties eq hiding (elim)

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

open import Bijection equality-with-J using (_↔_)
open import Equality.Decidable-UIP equality-with-J
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq using (_≃_)
open import Equivalence-relation equality-with-J
open import Function-universe equality-with-J as F hiding (_∘_; id)
open import H-level equality-with-J as H
import H-level P.equality-with-J as PH
open import H-level.Closure equality-with-J
import H-level.Truncation.Church equality-with-J as Trunc
open import H-level.Truncation.Propositional eq as TruncP
  using (∥_∥; ∣_∣; Surjective; Axiom-of-countable-choice)
open import Preimage equality-with-J using (_⁻¹_)
import Quotient eq as Quotient
import Quotient.Families-of-equivalence-classes equality-with-J as QF
open import Sum equality-with-J
open import Surjection equality-with-J using (_↠_)
open import Univalence-axiom equality-with-J

private
  variable
    a a₁ a₂ b p     : Level
    k               : Isomorphism-kind
    A A₁ A₂ B       : Type a
    P               : A → Type p
    e f r r₁ r₂ x y : A
    R R₁ R₂         : A → A → Type r

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

-- The quotient type constructor.

infix  _/_

data _/_ (A : Type a) (R : A → A → Type r) : Type (a ⊔ r) where
  [_]                   : A → A / R
  []-respects-relationᴾ : R x y → [ x ] P.≡ [ y ]
  /-is-setᴾ             : (∀ x y → Is-proposition (R x y)) →
                          P.Is-set (A / R)

-- [_] respects the quotient relation.

[]-respects-relation : R x y → _≡_ {A = A / R} [ x ] [ y ]
[]-respects-relation = _↔_.from ≡↔≡ ∘ []-respects-relationᴾ

-- If R is pointwise propositional, then A / R is a set.

/-is-set : (∀ x y → Is-proposition (R x y)) → Is-set (A / R)
/-is-set = _↔_.from (H-level↔H-level ) ∘ /-is-setᴾ

------------------------------------------------------------------------
-- Eliminators

-- An eliminator, expressed using paths.

record Elimᴾ′ {A : Type a} {R : A → A → Type r} (P : A / R → Type p) :
              Type (a ⊔ r ⊔ p) where
  no-eta-equality
  field
    []ʳ : ∀ x → P [ x ]

    []-respects-relationʳ :
      (r : R x y) →
      P.[ (λ i → P ([]-respects-relationᴾ r i)) ] []ʳ x ≡ []ʳ y

    is-setʳ :
      (prop : ∀ x y → Is-proposition (R x y))
      {eq₁ eq₂ : x P.≡ y} {p : P x} {q : P y}
      (eq₃ : P.[ (λ i → P (eq₁ i)) ] p ≡ q)
      (eq₄ : P.[ (λ i → P (eq₂ i)) ] p ≡ q) →
      P.[ (λ i → P.[ (λ j → P (/-is-setᴾ prop eq₁ eq₂ i j)) ] p ≡ q) ]
        eq₃ ≡ eq₄

open Elimᴾ′ public

elimᴾ′ : Elimᴾ′ P → (x : A / R) → P x
elimᴾ′ {A} {R} {P} e = helper
  where
  module E = Elimᴾ′ e

  helper : (x : A / R) → P x
  helper [ x ]                       = E.[]ʳ x
  helper ([]-respects-relationᴾ r i) = E.[]-respects-relationʳ r i
  helper (/-is-setᴾ prop p q i j)    =
    E.is-setʳ prop (λ i → helper (p i)) (λ i → helper (q i)) i j

-- A possibly more useful eliminator, expressed using paths.

record Elimᴾ {A : Type a} {R : A → A → Type r} (P : A / R → Type p) :
             Type (a ⊔ r ⊔ p) where
  no-eta-equality
  field
    []ʳ : ∀ x → P [ x ]

    []-respects-relationʳ :
      (r : R x y) →
      P.[ (λ i → P ([]-respects-relationᴾ r i)) ] []ʳ x ≡ []ʳ y

    is-setʳ :
      (∀ x y → Is-proposition (R x y)) →
      ∀ x → P.Is-set (P x)

open Elimᴾ public

elimᴾ : Elimᴾ P → (x : A / R) → P x
elimᴾ e = elimᴾ′ λ where
    .[]ʳ                   → E.[]ʳ
    .[]-respects-relationʳ → E.[]-respects-relationʳ
    .is-setʳ prop          → P.heterogeneous-UIP (E.is-setʳ prop) _
  where
  module E = Elimᴾ e

private

  -- One can define elimᴾ′ using elimᴾ.

  elimᴾ′₂ : Elimᴾ′ P → (x : A / R) → P x
  elimᴾ′₂ {P} e = elimᴾ λ where
      .[]ʳ                                → E.[]ʳ
      .[]-respects-relationʳ              → E.[]-respects-relationʳ
      .is-setʳ prop x {x = y} {y = z} p q →                        $⟨ E.is-setʳ prop p q ⟩
        P.[ (λ i →
               P.[ (λ j → P (/-is-setᴾ prop P.refl P.refl i j)) ]
                 y ≡ z) ]
          p ≡ q                                                    ↝⟨ P.subst (λ eq → P.[ (λ i → P.[ (λ j → P (eq i j)) ] y ≡ z) ] p ≡ q)
                                                                              (PH.mono₁  (/-is-setᴾ prop) _ _) ⟩
        P.[ (λ _ → P.[ (λ _ → P x) ] y ≡ z) ] p ≡ q                ↔⟨⟩

        p P.≡ q                                                    □
    where
    module E = Elimᴾ′ e

-- A non-dependent eliminator, expressed using paths.

record Recᴾ {A : Type a} (R : A → A → Type r) (B : Type b) :
            Type (a ⊔ r ⊔ b) where
  no-eta-equality
  field
    []ʳ                   : A → B
    []-respects-relationʳ : (r : R x y) → []ʳ x P.≡ []ʳ y
    is-setʳ               : (∀ x y → Is-proposition (R x y)) →
                            P.Is-set B

open Recᴾ public

recᴾ : Recᴾ R B → A / R → B
recᴾ r = elimᴾ λ where
    .[]ʳ                   → R.[]ʳ
    .[]-respects-relationʳ → R.[]-respects-relationʳ
    .is-setʳ prop _        → R.is-setʳ prop
  where
  module R = Recᴾ r

-- An eliminator.

record Elim {A : Type a} {R : A → A → Type r} (P : A / R → Type p) :
            Type (a ⊔ r ⊔ p) where
  no-eta-equality
  field
    []ʳ : ∀ x → P [ x ]

    []-respects-relationʳ :
      (r : R x y) →
      subst P ([]-respects-relation r) ([]ʳ x) ≡ []ʳ y

    is-setʳ : (∀ x y → Is-proposition (R x y)) → ∀ x → Is-set (P x)

open Elim public

elim : Elim P → (x : A / R) → P x
elim e = elimᴾ λ where
    .[]ʳ                   → E.[]ʳ
    .[]-respects-relationʳ → subst≡→[]≡ ∘ E.[]-respects-relationʳ
    .is-setʳ prop          →
      _↔_.to (H-level↔H-level ) ∘ E.is-setʳ prop
  where
  module E = Elim e

-- A computation rule.

elim-[]-respects-relation :
  dcong (elim e) ([]-respects-relation r) ≡ e .[]-respects-relationʳ r
elim-[]-respects-relation = dcong-subst≡→[]≡ (refl _)

-- A non-dependent eliminator.

record Rec {A : Type a} (R : A → A → Type r) (B : Type b) :
           Type (a ⊔ r ⊔ b) where
  no-eta-equality
  field
    []ʳ                   : A → B
    []-respects-relationʳ : (r : R x y) → []ʳ x ≡ []ʳ y
    is-setʳ               : (∀ x y → Is-proposition (R x y)) → Is-set B

open Rec public

rec : Rec R B → A / R → B
rec r = recᴾ λ where
    .[]ʳ                   → R.[]ʳ
    .[]-respects-relationʳ → _↔_.to ≡↔≡ ∘ R.[]-respects-relationʳ
    .is-setʳ               → _↔_.to (H-level↔H-level ) ∘ R.is-setʳ
  where
  module R = Rec r

-- A computation rule.

rec-[]-respects-relation :
  cong (rec {R = R} {B = B} r₁)
       ([]-respects-relation {x = x} {y = y} r₂) ≡
  r₁ .[]-respects-relationʳ r₂
rec-[]-respects-relation = cong-≡↔≡ (refl _)

-- 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.

record Elim-prop
         {A : Type a} {R : A → A → Type r} (P : A / R → Type p) :
         Type (a ⊔ r ⊔ p) where
  no-eta-equality
  field
    []ʳ             : ∀ x → P [ x ]
    is-propositionʳ : ∀ x → Is-proposition (P [ x ])

open Elim-prop public

elim-prop : Elim-prop P → (x : A / R) → P x
elim-prop e = elim λ where
    .[]ʳ                     → E.[]ʳ
    .[]-respects-relationʳ _ → E.is-propositionʳ _ _ _
    .is-setʳ _               → elim λ where
      .[]ʳ                     → mono₁  ∘ E.is-propositionʳ
      .[]-respects-relationʳ _ → H-level-propositional ext  _ _
      .is-setʳ _ _             → mono₁  (H-level-propositional ext )
  where
  module E = Elim-prop e

-- A variant of rec that can be used if the motive is a proposition.

record Rec-prop (A : Type a) (B : Type b) : Type (a ⊔ b) where
  no-eta-equality
  field
    []ʳ             : A → B
    is-propositionʳ : Is-proposition B

open Rec-prop public

rec-prop : Rec-prop A B → A / R → B
rec-prop r = elim-prop λ where
    .[]ʳ               → R.[]ʳ
    .is-propositionʳ _ → R.is-propositionʳ
  where
  module R = Rec-prop r

------------------------------------------------------------------------
-- Some properties

-- [_] is surjective.

[]-surjective : Surjective ([_] {R = R})
[]-surjective = elim-prop λ where
  .[]ʳ x             → ∣ x , refl _ ∣
  .is-propositionʳ _ → TruncP.truncation-is-proposition

-- If the relation is a propositional equivalence relation, then it is
-- equivalent to equality under [_] (assuming propositional
-- extensionality).
--
-- The basic structure of this proof is that of Proposition 2 in
-- "Quotienting the Delay Monad by Weak Bisimilarity" by Chapman,
-- Uustalu and Veltri.

related≃[equal] :
  {R : A → A → Type r} →
  Propositional-extensionality r →
  Is-equivalence-relation R →
  (∀ {x y} → Is-proposition (R x y)) →
  ∀ {x y} → R x y ≃ _≡_ {A = A / R} [ x ] [ y ]
related≃[equal] {A} {r} {R} prop-ext R-equiv R-prop {x} {y} =
  _↠_.from (Eq.≃↠⇔ R-prop (/-is-set λ _ _ → R-prop))
    (record
       { to   = []-respects-relation
       ; from = λ [x]≡[y] →
                               $⟨ reflexive ⟩
           proj₁ (R′ x [ x ])  ↝⟨ ≡⇒→ (cong (proj₁ ∘ R′ x) [x]≡[y]) ⟩
           proj₁ (R′ x [ y ])  ↝⟨ id ⟩□
           R x y               □
       })
  where
  open Is-equivalence-relation R-equiv

  lemma : ∀ {x y z} → R y z → (R x y , R-prop) ≡ (R x z , R-prop)
  lemma {x} {y} {z} =
    R y z                                ↝⟨ (λ r → record
                                               { to   = flip transitive r
                                               ; from = flip transitive (symmetric r)
                                               }) ⟩
    R x y ⇔ R x z                        ↔⟨ ⇔↔≡″ ext prop-ext ⟩□
    (R x y , R-prop) ≡ (R x z , R-prop)  □

  R′ : A → A / R → Proposition r
  R′ x = rec λ where
    .[]ʳ y                 → R x y , R-prop
    .[]-respects-relationʳ → lemma
    .is-setʳ _             → Is-set-∃-Is-proposition ext prop-ext

-- Quotienting with equality (for a set) amounts to the same thing as
-- not quotienting at all.

/≡↔ : Is-set A → A / _≡_ ↔ A
/≡↔ A-set = record
  { surjection = record
    { logical-equivalence = record
      { from = [_]
      ; to   = rec λ where
          .[]ʳ                   → id
          .[]-respects-relationʳ → id
          .is-setʳ prop          → prop _ _
      }
    ; right-inverse-of = λ _ → refl _
    }
  ; left-inverse-of = elim λ where
      .[]ʳ _ → refl _

      .is-setʳ prop _ → mono₁  (/-is-set prop)

      .[]-respects-relationʳ _ →
        /-is-set (λ _ _ → A-set) _ _
  }

-- Quotienting with a trivial, pointwise propositional relation
-- amounts to the same thing as using the propositional truncation
-- operator.

/trivial↔∥∥ :
  (∀ x y → R x y) →
  (∀ {x y} → Is-proposition (R x y)) →
  A / R ↔ ∥ A ∥
/trivial↔∥∥ {A} {R} trivial prop = record
  { surjection = record
    { logical-equivalence = record
      { from = TruncP.rec /-prop [_]
      ; to   = rec-prop λ where
          .[]ʳ             → ∣_∣
          .is-propositionʳ → TruncP.truncation-is-proposition
      }
    ; right-inverse-of = TruncP.elim
        _
        (λ _ → ⇒≡  TruncP.truncation-is-proposition)
        (λ _ → refl _)
    }
  ; left-inverse-of = elim-prop λ where
      .[]ʳ _             → refl _
      .is-propositionʳ _ → /-is-set λ _ _ → prop
  }
  where
  /-prop : Is-proposition (A / R)
  /-prop = elim-prop λ where
    .[]ʳ x → elim-prop λ where
      .[]ʳ y             → []-respects-relation (trivial x y)
      .is-propositionʳ _ → /-is-set λ _ _ → prop
    .is-propositionʳ _ →
      Π-closure ext  λ _ →
      /-is-set λ _ _ → prop

-- The previous property gives us an alternative to
-- constant-function≃∥inhabited∥⇒inhabited.

constant-function↔∥inhabited∥⇒inhabited :
  Is-set B →
  (∃ λ (f : A → B) → Constant f) ↔ (∥ A ∥ → B)
constant-function↔∥inhabited∥⇒inhabited {B} {A} B-set =
  (∃ λ (f : A → B) → Constant f)  ↝⟨ record
                                       { surjection = record
                                         { logical-equivalence = record
                                           { to   = λ { (f , c) → rec λ where
                                                        .[]ʳ                     → f
                                                        .[]-respects-relationʳ _ → c _ _
                                                        .is-setʳ _               → B-set }
                                           ; from = λ f → (f ∘ [_])
                                                        , (λ _ _ → cong f ([]-respects-relation _))
                                           }
                                         ; right-inverse-of = λ f → ⟨ext⟩ $ elim λ where
                                             .[]ʳ _                   → refl _
                                             .[]-respects-relationʳ _ → B-set _ _
                                             .is-setʳ _ _             → mono₁  B-set
                                         }
                                       ; left-inverse-of = λ _ → Σ-≡,≡→≡
                                           (refl _)
                                           ((Π-closure ext  λ _ →
                                             Π-closure ext  λ _ →
                                             B-set) _ _)
                                       } ⟩
  (A / (λ _ _ → ⊤) → B)           ↝⟨ →-cong₁ ext (/trivial↔∥∥ _ (mono₁  ⊤-contractible)) ⟩□
  (∥ A ∥ → B)                     □

-- The two directions of the proposition above compute in the
-- "right" way. Note that (at the time of writing) an analogue of
-- the second property below fails to hold definitionally for
-- constant-function≃∥inhabited∥⇒inhabited.

_ :
  {B-set : Is-set B} →
  _↔_.to (constant-function↔∥inhabited∥⇒inhabited B-set) f ∣ x ∣ ≡
  proj₁ f x
_ = refl _

_ :
  {B-set : Is-set B} →
  proj₁ (_↔_.from (constant-function↔∥inhabited∥⇒inhabited B-set) f)
        x ≡
  f ∣ x ∣
_ = refl _

------------------------------------------------------------------------
-- Preservation lemmas

-- A preservation lemma for functions.

/-map :
  ((∀ x y → Is-proposition (R₁ x y)) →
   (∀ x y → Is-proposition (R₂ x y))) →
  (A₁→A₂ : A₁ → A₂) →
  (∀ x y → R₁ x y → R₂ (A₁→A₂ x) (A₁→A₂ y)) →
  A₁ / R₁ → A₂ / R₂
/-map {R₁} {R₂} prop A₁→A₂ R₁→R₂ = rec λ where
  .[]ʳ → [_] ∘ A₁→A₂

  .is-setʳ → /-is-set ∘ prop

  .[]-respects-relationʳ {x} {y} →
     R₁ x y                     ↝⟨ R₁→R₂ _ _ ⟩
     R₂ (A₁→A₂ x) (A₁→A₂ y)     ↝⟨ []-respects-relation ⟩□
     [ A₁→A₂ x ] ≡ [ A₁→A₂ y ]  □

-- A preservation lemma for logical equivalences.

/-cong-⇔ :
  ((∀ x y → Is-proposition (R₁ x y)) ⇔
   (∀ x y → Is-proposition (R₂ x y))) →
  (A₁⇔A₂ : A₁ ⇔ A₂) →
  (∀ x y → R₁ x y → R₂ (_⇔_.to   A₁⇔A₂ x) (_⇔_.to   A₁⇔A₂ y)) →
  (∀ x y → R₂ x y → R₁ (_⇔_.from A₁⇔A₂ x) (_⇔_.from A₁⇔A₂ y)) →
  A₁ / R₁ ⇔ A₂ / R₂
/-cong-⇔ prop A₁⇔A₂ R₁→R₂ R₂→R₁ = record
  { to   = /-map (_⇔_.to   prop) (_⇔_.to   A₁⇔A₂) R₁→R₂
  ; from = /-map (_⇔_.from prop) (_⇔_.from A₁⇔A₂) R₂→R₁
  }

-- A preservation lemma for split surjections.

/-cong-↠ :
  ((∀ x y → Is-proposition (R₁ x y)) ⇔
   (∀ x y → Is-proposition (R₂ x y))) →
  (A₁↠A₂ : A₁ ↠ A₂) →
  (∀ x y → R₁ x y ↠ R₂ (_↠_.to A₁↠A₂ x) (_↠_.to A₁↠A₂ y)) →
  A₁ / R₁ ↠ A₂ / R₂
/-cong-↠ {R₁} {R₂} prop A₁↠A₂ R₁↠R₂ = record
  { logical-equivalence = /-cong-⇔
      prop
      (_↠_.logical-equivalence A₁↠A₂)
      (λ x y → _↠_.to (R₁↠R₂ x y))
      (λ x y → R₂ x y                          ↝⟨ ≡⇒↝ _ (sym $ cong₂ R₂ (right-inverse-of x) (right-inverse-of y)) ⟩
               R₂ (to (from x)) (to (from y))  ↝⟨ _↠_.from (R₁↠R₂ _ _) ⟩□
               R₁ (from x) (from y)            □)
  ; right-inverse-of = elim λ where
      .[]ʳ x →
        [ to (from x) ]  ≡⟨ cong [_] $ right-inverse-of x ⟩∎
        [ x ]            ∎

      .is-setʳ prop _ → mono₁  (/-is-set prop)

      .[]-respects-relationʳ {x} {y} r →
        let tr = λ x y → _↠_.to (R₁↠R₂ x y)

            fr = λ x y →
                   _↠_.from (R₁↠R₂ (from x) (from y)) ∘
                   ≡⇒↝ _
                     (sym (cong₂ R₂ (right-inverse-of x)
                                    (right-inverse-of y)))

            t = /-map (_⇔_.to prop) to tr

            f = /-map (_⇔_.from prop) from fr
        in
        subst (λ x → t (f x) ≡ x)
          ([]-respects-relation r)
          (cong [_] (right-inverse-of x))                       ≡⟨ subst-in-terms-of-trans-and-cong ⟩

        trans
          (sym (cong (t ∘ f) ([]-respects-relation r)))
          (trans (cong [_] (right-inverse-of x))
             (cong id ([]-respects-relation r)))                ≡⟨ cong₂ (λ eq₁ eq₂ → trans (sym eq₁)
                                                                                        (trans (cong [_] (right-inverse-of x)) eq₂))
                                                                     (sym $ cong-∘ _ _ _)
                                                                     (sym $ cong-id _) ⟩
        trans
          (sym (cong t (cong f ([]-respects-relation r))))
          (trans (cong [_] (right-inverse-of x))
             ([]-respects-relation r))                          ≡⟨ cong (λ eq → trans (sym (cong t eq))
                                                                                  (trans (cong [_] (right-inverse-of x))
                                                                                     ([]-respects-relation r))) $
                                                                   rec-[]-respects-relation ⟩
        trans
          (sym (cong t ([]-respects-relation (fr _ _ r))))
          (trans (cong [_] (right-inverse-of x))
             ([]-respects-relation r))                          ≡⟨ cong (λ eq → trans (sym eq)
                                                                                  (trans (cong [_] (right-inverse-of x))
                                                                                     ([]-respects-relation r))) $
                                                                   rec-[]-respects-relation ⟩
        trans
          (sym ([]-respects-relation (tr _ _ (fr _ _ r))))
          (trans (cong [_] (right-inverse-of x))
             ([]-respects-relation r))                          ≡⟨ cong (λ r′ → trans (sym ([]-respects-relation r′))
                                                                                  (trans (cong [_] (right-inverse-of x))
                                                                                     ([]-respects-relation r))) $
                                                                   _↠_.right-inverse-of (R₁↠R₂ _ _) _ ⟩
        trans
          (sym ([]-respects-relation
                  (≡⇒↝ _ (sym (cong₂ R₂ (right-inverse-of x)
                                        (right-inverse-of y)))
                     r)))
          (trans (cong [_] (right-inverse-of x))
             ([]-respects-relation r))                          ≡⟨ lemma _ _ _ ⟩∎

        cong [_] (right-inverse-of y)                           ∎
  }
  where
  open _↠_ A₁↠A₂

  lemma : ∀ _ _ _ → _
  lemma x y r =
    elim₁
      (λ eq →
         trans
           (sym ([]-respects-relation
                   (≡⇒↝ _ (sym (cong₂ R₂ (right-inverse-of x) eq)) r)))
           (trans (cong [_] (right-inverse-of x))
              ([]-respects-relation r)) ≡
         cong [_] eq)
      (elim₁
         (λ eq →
            trans
              (sym ([]-respects-relation
                      (≡⇒↝ _ (sym (cong₂ R₂ eq (refl _))) r)))
              (trans (cong [_] eq) ([]-respects-relation r)) ≡
            cong [_] (refl _))
         (trans
            (sym ([]-respects-relation
                    (≡⇒↝ _ (sym (cong₂ R₂ (refl _) (refl _))) r)))
            (trans (cong [_] (refl _)) ([]-respects-relation r))    ≡⟨ cong₂ (λ eq₁ eq₂ →
                                                                                trans (sym ([]-respects-relation (≡⇒↝ _ eq₁ r)))
                                                                                  (trans eq₂ ([]-respects-relation r)))
                                                                         (trans (cong sym $ cong₂-refl R₂) sym-refl)
                                                                         (cong-refl _) ⟩
          trans
            (sym ([]-respects-relation (≡⇒↝ _ (refl _) r)))
            (trans (refl _) ([]-respects-relation r))               ≡⟨ cong₂ (λ eq₁ eq₂ → trans (sym ([]-respects-relation eq₁)) eq₂)
                                                                         (cong (_$ r) ≡⇒↝-refl)
                                                                         (trans-reflˡ _) ⟩
          trans
            (sym ([]-respects-relation r))
            ([]-respects-relation r)                                ≡⟨ trans-symˡ _ ⟩

          refl _                                                    ≡⟨ sym $ cong-refl _ ⟩∎

          cong [_] (refl _)                                         ∎)
         (right-inverse-of x))
      (right-inverse-of y)

private

  -- A preservation lemma for equivalences.

  /-cong-≃ :
    ((∀ x y → Is-proposition (R₁ x y)) ⇔
     (∀ x y → Is-proposition (R₂ x y))) →
    (A₁≃A₂ : A₁ ≃ A₂) →
    (∀ x y →
       R₁ x y ≃ R₂ (to-implication A₁≃A₂ x) (to-implication A₁≃A₂ y)) →
    A₁ / R₁ ≃ A₂ / R₂
  /-cong-≃ {R₁} {R₂} prop A₁≃A₂ R₁≃R₂ = Eq.↔⇒≃ (record
    { surjection = /-cong-↠ prop (_≃_.surjection A₁≃A₂) λ x y →
        R₁ x y            ↔⟨ R₁≃R₂ x y ⟩□
        R₂ (to x) (to y)  □
    ; left-inverse-of = elim λ where
        .[]ʳ x →
          [ from (to x) ]  ≡⟨ cong [_] $ left-inverse-of x ⟩∎
          [ x ]            ∎

        .is-setʳ prop _ → mono₁  (/-is-set prop)

        .[]-respects-relationʳ {x} {y} r →
          let tr = λ x y → _≃_.to (R₁≃R₂ x y)

              fr = λ x y →
                     _≃_.from (R₁≃R₂ (from x) (from y)) ∘
                     ≡⇒↝ _
                       (sym (cong₂ R₂ (right-inverse-of x)
                                      (right-inverse-of y)))

              t = /-map (_⇔_.to prop) to tr

              f = /-map (_⇔_.from prop) from fr
          in
          subst (λ x → f (t x) ≡ x)
            ([]-respects-relation r)
            (cong [_] (left-inverse-of x))                       ≡⟨ subst-in-terms-of-trans-and-cong ⟩

          trans
            (sym (cong (f ∘ t) ([]-respects-relation r)))
            (trans (cong [_] (left-inverse-of x))
               (cong id ([]-respects-relation r)))               ≡⟨ cong₂ (λ eq₁ eq₂ → trans (sym eq₁)
                                                                                         (trans (cong [_] (left-inverse-of x)) eq₂))
                                                                      (sym $ cong-∘ _ _ _)
                                                                      (sym $ cong-id _) ⟩
          trans
            (sym (cong f (cong t ([]-respects-relation r))))
            (trans (cong [_] (left-inverse-of x))
               ([]-respects-relation r))                         ≡⟨ cong (λ eq → trans (sym (cong f eq))
                                                                                   (trans (cong [_] (left-inverse-of x))
                                                                                      ([]-respects-relation r))) $
                                                                    rec-[]-respects-relation ⟩
          trans
            (sym (cong f ([]-respects-relation (tr _ _ r))))
            (trans (cong [_] (left-inverse-of x))
               ([]-respects-relation r))                         ≡⟨ cong (λ eq → trans (sym eq)
                                                                                   (trans (cong [_] (left-inverse-of x))
                                                                                      ([]-respects-relation r))) $
                                                                    rec-[]-respects-relation ⟩
          trans
            (sym ([]-respects-relation (fr _ _ (tr _ _ r))))
            (trans (cong [_] (left-inverse-of x))
               ([]-respects-relation r))                         ≡⟨ cong (λ r′ → trans (sym ([]-respects-relation r′))
                                                                                   (trans (cong [_] (left-inverse-of x))
                                                                                      ([]-respects-relation r))) $
                                                                    lemma₁ _ _ _ ⟩
          trans
            (sym ([]-respects-relation
                    (≡⇒↝ _ (sym (cong₂ R₁ (left-inverse-of x)
                                          (left-inverse-of y)))
                       r)))
            (trans (cong [_] (left-inverse-of x))
               ([]-respects-relation r))                         ≡⟨ lemma₂ _ _ _ ⟩∎

          cong [_] (left-inverse-of y)                           ∎
    })
    where
    open _≃_ A₁≃A₂

    lemma₀ : ∀ _ _ _ → _
    lemma₀ x y r =
      elim₁
        (λ eq →
           _≃_.from (R₁≃R₂ (from (to x)) _)
             (≡⇒↝ _ (sym (cong₂ (λ x y → R₂ (to x) (to y))
                            (left-inverse-of x) eq))
                (_≃_.to (R₁≃R₂ x y) r)) ≡
           ≡⇒↝ _ (sym (cong₂ R₁ (left-inverse-of x) eq)) r)
        (elim₁
           (λ eq →
              _≃_.from (R₁≃R₂ _ _)
                (≡⇒↝ _ (sym (cong₂ (λ x y → R₂ (to x) (to y))
                               eq (refl _)))
                   (_≃_.to (R₁≃R₂ x y) r)) ≡
              ≡⇒↝ _ (sym (cong₂ R₁ eq (refl _))) r)
           (_≃_.from (R₁≃R₂ _ _)
              (≡⇒↝ _ (sym (cong₂ (λ x y → R₂ (to x) (to y))
                             (refl _) (refl _)))
                 (_≃_.to (R₁≃R₂ x y) r))                                  ≡⟨ cong (λ eq → _≃_.from (R₁≃R₂ _ _) (≡⇒↝ _ eq (_≃_.to (R₁≃R₂ x y) r))) $
                                                                             trans (cong sym $ cong₂-refl _) sym-refl ⟩

            _≃_.from (R₁≃R₂ _ _) (≡⇒↝ _ (refl _) (_≃_.to (R₁≃R₂ x y) r))  ≡⟨ cong (_≃_.from (R₁≃R₂ _ _)) $ cong (_$ _≃_.to (R₁≃R₂ x y) r)
                                                                             ≡⇒↝-refl ⟩

            _≃_.from (R₁≃R₂ _ _) (_≃_.to (R₁≃R₂ x y) r)                   ≡⟨ _≃_.left-inverse-of (R₁≃R₂ _ _) _ ⟩

            r                                                             ≡⟨ sym $ cong (_$ r) ≡⇒↝-refl ⟩

            ≡⇒↝ _ (refl _) r                                              ≡⟨ cong (λ eq → ≡⇒↝ _ eq r) $ sym $
                                                                             trans (cong sym $ cong₂-refl _) sym-refl ⟩∎
            ≡⇒↝ _ (sym (cong₂ R₁ (refl _) (refl _))) r                    ∎)
           (left-inverse-of x))
        (left-inverse-of y)

    lemma₁ : ∀ _ _ _ → _
    lemma₁ x y r =
      _≃_.from (R₁≃R₂ (from (to x)) (from (to y)))
        (≡⇒↝ _ (sym (cong₂ R₂ (right-inverse-of (to x))
                              (right-inverse-of (to y))))
           (_≃_.to (R₁≃R₂ x y) r))                                       ≡⟨⟩

      _≃_.from (R₁≃R₂ (from (to x)) (from (to y)))
        (≡⇒↝ _ (sym (trans (cong (flip R₂ _) (right-inverse-of (to x)))
                       (cong (R₂ _) (right-inverse-of (to y)))))
           (_≃_.to (R₁≃R₂ x y) r))                                       ≡⟨ cong₂ (λ eq₁ eq₂ →
                                                                                     _≃_.from (R₁≃R₂ (from (to x)) (from (to y)))
                                                                                       (≡⇒↝ _ (sym (trans eq₁ eq₂)) (_≃_.to (R₁≃R₂ x y) r)))
                                                                              (trans (cong (cong _) $ sym $ left-right-lemma _) (cong-∘ _ _ _))
                                                                              (trans (cong (cong _) $ sym $ left-right-lemma _) (cong-∘ _ _ _)) ⟩
      _≃_.from (R₁≃R₂ (from (to x)) (from (to y)))
        (≡⇒↝ _ (sym (trans (cong (flip R₂ _ ∘ to) (left-inverse-of x))
                       (cong (R₂ _ ∘ to) (left-inverse-of y))))
           (_≃_.to (R₁≃R₂ x y) r))                                       ≡⟨⟩

      _≃_.from (R₁≃R₂ (from (to x)) (from (to y)))
        (≡⇒↝ _ (sym (cong₂ (λ x y → R₂ (to x) (to y))
                       (left-inverse-of x)
                       (left-inverse-of y)))
           (_≃_.to (R₁≃R₂ x y) r))                                       ≡⟨ lemma₀ _ _ _ ⟩∎

      ≡⇒↝ _ (sym (cong₂ R₁ (left-inverse-of x) (left-inverse-of y))) r   ∎

    lemma₂ : ∀ _ _ _ → _
    lemma₂ x y r =
      elim₁
        (λ eq →
           trans
             (sym ([]-respects-relation
                     (≡⇒↝ _ (sym (cong₂ R₁ (left-inverse-of x) eq)) r)))
             (trans (cong [_] (left-inverse-of x))
                ([]-respects-relation r)) ≡
           cong [_] eq)
        (elim₁
           (λ eq →
              trans
                (sym ([]-respects-relation
                        (≡⇒↝ _ (sym (cong₂ R₁ eq (refl _))) r)))
                (trans (cong [_] eq) ([]-respects-relation r)) ≡
              cong [_] (refl _))
           (trans
              (sym ([]-respects-relation
                      (≡⇒↝ _ (sym (cong₂ R₁ (refl _) (refl _))) r)))
              (trans (cong [_] (refl _)) ([]-respects-relation r))    ≡⟨ cong₂ (λ eq₁ eq₂ →
                                                                                  trans (sym ([]-respects-relation (≡⇒↝ _ eq₁ r)))
                                                                                    (trans eq₂ ([]-respects-relation r)))
                                                                           (trans (cong sym $ cong₂-refl R₁) sym-refl)
                                                                           (cong-refl _) ⟩
            trans
              (sym ([]-respects-relation (≡⇒↝ _ (refl _) r)))
              (trans (refl _) ([]-respects-relation r))               ≡⟨ cong₂ (λ eq₁ eq₂ → trans (sym ([]-respects-relation eq₁)) eq₂)
                                                                           (cong (_$ r) ≡⇒↝-refl)
                                                                           (trans-reflˡ _) ⟩
            trans
              (sym ([]-respects-relation r))
              ([]-respects-relation r)                                ≡⟨ trans-symˡ _ ⟩

            refl _                                                    ≡⟨ sym $ cong-refl _ ⟩∎

            cong [_] (refl _)                                         ∎)
           (left-inverse-of x))
        (left-inverse-of y)

-- A preservation lemma for isomorphisms.

/-cong-↔ :
  {A₁ : Type a₁} {R₁ : A₁ → A₁ → Type r₁}
  {A₂ : Type a₂} {R₂ : A₂ → A₂ → Type r₂} →
  ((∀ x y → Is-proposition (R₁ x y)) ⇔
   (∀ x y → Is-proposition (R₂ x y))) →
  (A₁↔A₂ : A₁ ↔[ k ] A₂) →
  (∀ x y →
     R₁ x y ↔[ k ]
     R₂ (to-implication A₁↔A₂ x) (to-implication A₁↔A₂ y)) →
  A₁ / R₁ ↔[ k ] A₂ / R₂
/-cong-↔ {k} {R₁} {R₂} prop A₁↔A₂ R₁↔R₂ =
  from-isomorphism $
  /-cong-≃ prop A₁≃A₂ λ x y →
    R₁ x y                                                ↔⟨ R₁↔R₂ x y ⟩
    R₂ (to-implication A₁↔A₂ x) (to-implication A₁↔A₂ y)  ↝⟨ ≡⇒↝ _ $ cong₂ (λ f g → R₂ (f x) (g y))
                                                                       (to-implication∘from-isomorphism k equivalence)
                                                                       (to-implication∘from-isomorphism k equivalence) ⟩□
    R₂ (_≃_.to A₁≃A₂ x) (_≃_.to A₁≃A₂ y)                  □
  where
  A₁≃A₂ = from-isomorphism A₁↔A₂

------------------------------------------------------------------------
-- The quotients defined here can be related to the ones defined in
-- Quotient

-- If the quotient relation is propositional, then the definition of
-- quotients given in Quotient is equivalent to the one given here.

/≃/ :
  (∀ {x y} → Is-proposition (R x y)) →
  A / R ≃ A Quotient./ R
/≃/ R-prop = Eq.↔⇒≃ (record
  { surjection = record
    { logical-equivalence = record
      { to = rec (λ where
          .[]ʳ → Quotient.[_]

          .[]-respects-relationʳ → Quotient.[]-respects-relation

          .is-setʳ _ → Quotient./-is-set)
      ; from = Quotient.rec λ where
          .Quotient.Rec.[]ʳ → [_]

          .Quotient.Rec.[]-respects-relationʳ → []-respects-relation

          .Quotient.Rec.is-setʳ → /-is-set λ _ _ → R-prop
      }
    ; right-inverse-of = Quotient.elim-prop λ where
        .Quotient.Elim-prop.[]ʳ _ → refl _

        .Quotient.Elim-prop.is-propositionʳ _ → Quotient./-is-set
    }
  ; left-inverse-of = elim-prop λ where
        .Elim-prop.[]ʳ _ → refl _

        .Elim-prop.is-propositionʳ _ → /-is-set λ _ _ → R-prop
  })

------------------------------------------------------------------------
-- The quotients defined here can be related to the ones defined in
-- QF.Families-of-equivalence-classes

private

  -- An alternative definition of the quotients from
  -- QF.Families-of-equivalence-classes.

  infix  _/′_

  _/′_ : (A : Type a) → (A → A → Type a) → Type (lsuc a)
  _/′_ {a} A R = ∃ λ (P : A → Type a) → ∥ (∃ λ x → R x ≡ P) ∥

  /↔/′ : A QF./ R ↔ A /′ R
  /↔/′ {A} {R} =
    A QF./ R                                                  ↔⟨⟩
    (∃ λ (P : A → Type _) → Trunc.∥ (∃ λ x → R x ≡ P) ∥  _)  ↝⟨ (∃-cong λ _ → inverse $ TruncP.∥∥↔∥∥ lzero) ⟩
    (∃ λ (P : A → Type _) → ∥ (∃ λ x → R x ≡ P) ∥)            ↔⟨⟩
    A /′ R                                                    □

  [_]′ : A → A /′ R
  [_]′ = _↔_.to /↔/′ ∘ QF.[_]

  rec′ :
    {A : Type a} {R : A → A → Type 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′ refl B B-set f R⇒≡ =
    QF.rec ext refl B B-set f R⇒≡ ∘
    _↔_.from /↔/′

  elim-Prop′ :
    {A : Type a} {R : A → A → Type a} →
    QF.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′ strong-equivalence B B-prop f x =
    subst B (_↔_.right-inverse-of /↔/′ _) $
      QF.elim-Prop
        ext
        strong-equivalence
        (B ∘ _↔_.to /↔/′)
        B-prop
        f
        (_↔_.from /↔/′ x)

-- If the relation is a propositional equivalence relation of a
-- certain size, then the quotients defined above are isomorphic to
-- families of equivalence relations, defined in a certain way
-- (assuming univalence).

/↔ :
  {A : Type a} {R : A → A → Type a} →
  Univalence a →
  Univalence lzero →
  Is-equivalence-relation R →
  (∀ {x y} → Is-proposition (R x y)) →
  A / R ↔ ∃ λ (P : A → Type a) → ∥ (∃ λ x → R x ≡ P) ∥
/↔ {a} {A} {R} univ univ₀ R-equiv R-prop = record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = to∘from
    }
  ; left-inverse-of = from∘to
  }
  where
  R-is-strong-equivalence : QF.Strong-equivalence R
  R-is-strong-equivalence =
    QF.propositional-equivalence⇒strong-equivalence
      ext univ R-equiv (λ _ _ → R-prop)

  to : A / R → A /′ R
  to = rec λ where
    .[]ʳ → [_]′

    .[]-respects-relationʳ {x} {y} →
      R x y                ↝⟨ _≃_.to (QF.related↝[equal] ext R-is-strong-equivalence) ⟩
      QF.[ x ] ≡ QF.[ y ]  ↝⟨ cong (_↔_.to /↔/′) ⟩□
      [ x ]′ ≡ [ y ]′      □

    .is-setʳ prop →      $⟨ (λ {_ _} → QF.quotient's-h-level-is-1-+-relation's-h-level
                                         ext univ univ₀  (λ _ _ → R-prop)) ⟩
      Is-set (A QF./ R)  ↝⟨ H.respects-surjection (_↔_.surjection /↔/′)  ⟩□
      Is-set (A /′ R)    □

  from : A /′ R → A / R
  from = rec′
    (Is-equivalence-relation.reflexive R-equiv)
    _
    (/-is-set λ _ _ → R-prop)
    [_]
    []-respects-relation

  to∘from : ∀ x → to (from x) ≡ x
  to∘from = elim-Prop′
    (QF.strong-equivalence⇒strong-equivalence-with
       R-is-strong-equivalence)
    _
    (λ x →                                         $⟨ (λ {_ _} → QF.quotient's-h-level-is-1-+-relation's-h-level
                                                                   ext univ univ₀  λ _ _ → R-prop) ⟩
       Is-set (A QF./ R)                           ↝⟨ H.respects-surjection (_↔_.surjection /↔/′)  ⟩
       Is-set (A /′ R)                             ↝⟨ +⇒≡ {n = } ⟩□
       Is-proposition (to (from [ x ]′) ≡ [ x ]′)  □)
    (λ _ → refl _)

  from∘to : ∀ x → from (to x) ≡ x
  from∘to = elim-prop λ where
    .[]ʳ _             → refl _
    .is-propositionʳ _ → /-is-set λ _ _ → R-prop

-- If the relation is a propositional equivalence relation of a
-- certain size, then the definition of quotients given in
-- QF.Families-of-equivalence-classes is isomorphic to the one given
-- here (assuming univalence).

/↔/ :
  {A : Type a} {R : A → A → Type a} →
  Univalence a →
  Univalence lzero →
  Is-equivalence-relation R →
  (R-prop : ∀ {x y} → Is-proposition (R x y)) →
  A QF./ R ↔ A / R
/↔/ {a} {A} {R} univ univ₀ R-equiv R-prop =
  A QF./ R                                                         ↔⟨⟩
  (∃ λ (P : A → Type a) → Trunc.∥ (∃ λ x → R x ≡ P) ∥  (lsuc a))  ↝⟨ (∃-cong λ _ → inverse $ TruncP.∥∥↔∥∥ lzero) ⟩
  (∃ λ (P : A → Type a) →       ∥ (∃ λ x → R x ≡ P) ∥)             ↝⟨ inverse $ /↔ univ univ₀ R-equiv R-prop ⟩□
  A / R                                                            □

------------------------------------------------------------------------
-- Various type formers commute with quotients

-- _⊎_ commutes with quotients if the relations are pointwise
-- propositional.

⊎/-comm :
  (∀ {x y} → Is-proposition (R₁ x y)) →
  (∀ {x y} → Is-proposition (R₂ x y)) →
  (A₁ ⊎ A₂) / (R₁ ⊎ᴾ R₂) ↔ A₁ / R₁ ⊎ A₂ / R₂
⊎/-comm R₁-prop R₂-prop = record
  { surjection = record
    { logical-equivalence = record
      { to = rec λ where
          .[]ʳ          → ⊎-map [_] [_]
          .is-setʳ prop → ⊎-closure  is-set₁ is-set₂

          .[]-respects-relationʳ {x = inj₁ _} {y = inj₁ _} →
            cong inj₁ ∘ []-respects-relation
          .[]-respects-relationʳ {x = inj₂ _} {y = inj₂ _} →
            cong inj₂ ∘ []-respects-relation

      ; from = Prelude.[ rec (λ where
                           .[]ʳ                   → [_] ∘ inj₁
                           .[]-respects-relationʳ → []-respects-relation
                           .is-setʳ prop          → is-set₁₂)
                       , rec (λ where
                           .[]ʳ                   → [_] ∘ inj₂
                           .[]-respects-relationʳ → []-respects-relation
                           .is-setʳ prop          → is-set₁₂)
                       ]
      }
    ; right-inverse-of =
        Prelude.[ elim-prop (λ where
                    .[]ʳ _             → refl _
                    .is-propositionʳ _ → ⊎-closure  is-set₁ is-set₂)
                , elim-prop (λ where
                    .[]ʳ _             → refl _
                    .is-propositionʳ _ → ⊎-closure  is-set₁ is-set₂)
                ]
    }
  ; left-inverse-of = elim-prop λ where
      .[]ʳ               → Prelude.[ (λ _ → refl _) , (λ _ → refl _) ]
      .is-propositionʳ _ → is-set₁₂
  }
  where
  is-set₁  = /-is-set λ _ _ → R₁-prop
  is-set₂  = /-is-set λ _ _ → R₂-prop
  is-set₁₂ = /-is-set λ x y → ⊎ᴾ-preserves-Is-proposition
                                R₁-prop R₂-prop {x = x} {y = y}

-- Maybe commutes with quotients if the relation is pointwise
-- propositional.
--
-- Chapman, Uustalu and Veltri mention a similar result in
-- "Quotienting the Delay Monad by Weak Bisimilarity".

Maybe/-comm :
  (∀ {x y} → Is-proposition (R x y)) →
  Maybe A / Maybeᴾ R ↔ Maybe (A / R)
Maybe/-comm {A} {R} R-prop =
  Maybe A / Maybeᴾ R   ↝⟨ ⊎/-comm (↑-closure  (mono₁  ⊤-contractible)) R-prop ⟩
  ⊤ / Trivial ⊎ A / R  ↝⟨ /trivial↔∥∥ _ (↑-closure  (mono₁  ⊤-contractible)) ⊎-cong F.id ⟩
  ∥ ⊤ ∥ ⊎ A / R        ↝⟨ TruncP.∥∥↔ (mono₁  ⊤-contractible) ⊎-cong F.id ⟩□
  Maybe (A / R)        □

-- A simplification lemma for Maybe/-comm.

Maybe/-comm-[] :
  {R : A → A → Type r}
  {R-prop : ∀ {x y} → Is-proposition (R x y)} →
  _↔_.to (Maybe/-comm {R = R} R-prop) ∘ [_] ≡ ⊎-map id [_]
Maybe/-comm-[] {R-prop} =
  _↔_.to (Maybe/-comm R-prop) ∘ [_]        ≡⟨⟩
  ⊎-map _ id ∘ ⊎-map _ id ∘ ⊎-map [_] [_]  ≡⟨ cong (_∘ ⊎-map [_] [_]) $ sym $ ⟨ext⟩ ⊎-map-∘ ⟩
  ⊎-map _ id ∘ ⊎-map [_] [_]               ≡⟨ sym $ ⟨ext⟩ ⊎-map-∘ ⟩∎
  ⊎-map id [_]                             ∎

-- The sigma type former commutes (kind of) with quotients, assuming
-- that certain families are propositional.

Σ/-comm :
  {P : A / R → Type p} →
  (∀ {x} → Is-proposition (P x)) →
  (∀ {x y} → Is-proposition (R x y)) →
  Σ (A / R) P ↔ Σ A (P ∘ [_]) / (R on proj₁)
Σ/-comm {A} {R} {P} P-prop R-prop = record
  { surjection = record
    { logical-equivalence = record
      { to =
          uncurry $
          elim λ where
            .[]ʳ → curry [_]
            .[]-respects-relationʳ {x} {y} r → ⟨ext⟩ λ P[y] →
              subst (λ x → P x → Σ A (P ∘ [_]) / (R on proj₁))
                    ([]-respects-relation r)
                    (curry [_] x) P[y]                               ≡⟨ subst-→-domain P {f = curry [_] _} ([]-respects-relation r) ⟩

              [ (x , subst P (sym $ []-respects-relation r) P[y]) ]  ≡⟨ []-respects-relation r ⟩∎

              [ (y , P[y]) ]                                         ∎
            .is-setʳ prop _ →
              Π-closure ext  λ _ →
              /-is-set λ _ _ → prop _ _
      ; from = rec λ where
          .[]ʳ       → Σ-map [_] id
          .is-setʳ _ →
            Σ-closure  (/-is-set λ _ _ → R-prop) (λ _ → mono₁  P-prop)

          .[]-respects-relationʳ {x = (x₁ , x₂)} {y = (y₁ , y₂)} →
            R x₁ y₁                        ↝⟨ []-respects-relation ⟩
            [ x₁ ] ≡ [ y₁ ]                ↔⟨ ignore-propositional-component P-prop ⟩
            ([ x₁ ] , x₂) ≡ ([ y₁ ] , y₂)  □
      }
    ; right-inverse-of = elim-prop λ where
        .[]ʳ _             → refl _
        .is-propositionʳ _ → /-is-set λ _ _ → R-prop
    }
  ; left-inverse-of = uncurry $ elim-prop λ where
      .[]ʳ _ _           → refl _
      .is-propositionʳ _ →
        Π-closure ext  λ _ →
        Σ-closure  (/-is-set λ _ _ → R-prop) (λ _ → mono₁  P-prop)
  }

-- The type former λ X → ℕ → X commutes with quotients, assuming that
-- the quotient relation is a propositional equivalence relation, and
-- also assuming countable choice and propositional extensionality.
--
-- This result is very similar to Proposition 5 in "Quotienting the
-- Delay Monad by Weak Bisimilarity" by Chapman, Uustalu and Veltri.

-- The forward component of the isomorphism. This component can be
-- defined without any extra assumptions.

ℕ→/-comm-to : (ℕ → A) / (ℕ →ᴾ R) → (ℕ → A / R)
ℕ→/-comm-to {A} = rec λ where
    .[]ʳ f n → [ f n ]

    .[]-respects-relationʳ r →
      ⟨ext⟩ ([]-respects-relation ∘ r)

    .is-setʳ prop →
      Π-closure ext  λ _ →
      /-is-set (prop⇒prop prop)
  where
  prop⇒prop :
    ((f g : ℕ → A) → Is-proposition ((ℕ →ᴾ R) f g)) →
    ((x y : A) → Is-proposition (R x y))
  prop⇒prop prop x y p q =
    cong (_$ ) $ prop (λ _ → x) (λ _ → y) (λ _ → p) (λ _ → q)

-- The isomorphism.

ℕ→/-comm :
  {A : Type a} {R : A → A → Type r} →
  Axiom-of-countable-choice (a ⊔ r) →
  Propositional-extensionality r →
  Is-equivalence-relation R →
  (∀ {x y} → Is-proposition (R x y)) →
  (ℕ → A) / (ℕ →ᴾ R) ↔ (ℕ → A / R)
ℕ→/-comm {A} {R} cc prop-ext R-equiv R-prop = record
  { surjection = record
    { logical-equivalence = record
      { to   = ℕ→/-comm-to
      ; from = from
      }
    ; right-inverse-of = to∘from
    }
  ; left-inverse-of = from∘to
  }
  where
  [_]→ : (ℕ → A) → (ℕ → A / R)
  [ f ]→ n = [ f n ]

  opaque

    []→-surjective : Surjective [_]→
    []→-surjective f =                    $⟨ []-surjective ⟩
      Surjective [_]                      ↝⟨ (λ surj → surj ∘ f) ⦂ (_ → _) ⟩
      (∀ n → ∥ (∃ λ x → [ x ] ≡ f n) ∥)   ↔⟨ TruncP.countable-choice-bijection cc ⟩
      ∥ (∀ n → ∃ λ x → [ x ] ≡ f n) ∥     ↔⟨ TruncP.∥∥-cong ΠΣ-comm ⟩
      ∥ (∃ λ g → ∀ n → [ g n ] ≡ f n) ∥   ↔⟨⟩
      ∥ (∃ λ g → ∀ n → [ g ]→ n ≡ f n) ∥  ↔⟨ TruncP.∥∥-cong (∃-cong λ _ → Eq.extensionality-isomorphism ext) ⟩□
      ∥ (∃ λ g → [ g ]→ ≡ f) ∥            □

  from₁ : ∀ f → [_]→ ⁻¹ f → ℕ→/-comm-to ⁻¹ f
  from₁ f (g , [g]→≡f) =
      [ g ]
    , (ℕ→/-comm-to [ g ]  ≡⟨⟩
       [ g ]→             ≡⟨ [g]→≡f ⟩∎
       f                  ∎)

  from₁-constant : ∀ f → Constant (from₁ f)
  from₁-constant f (g₁ , [g₁]→≡f) (g₂ , [g₂]→≡f) =
                                             $⟨ (λ n → cong (_$ n) (
        [ g₁ ]→                                    ≡⟨ [g₁]→≡f ⟩
        f                                          ≡⟨ sym [g₂]→≡f ⟩∎
        [ g₂ ]→                                    ∎)) ⟩

    (∀ n → [ g₁ ]→ n ≡ [ g₂ ]→ n)            ↔⟨⟩

    (∀ n → [ g₁ n ] ≡ [ g₂ n ])              ↔⟨ ∀-cong ext (λ _ → inverse $ related≃[equal] prop-ext R-equiv R-prop) ⟩

    (∀ n → R (g₁ n) (g₂ n))                  ↔⟨⟩

    (ℕ →ᴾ R) g₁ g₂                           ↝⟨ []-respects-relation ⟩

    [ g₁ ] ≡ [ g₂ ]                          ↔⟨ ignore-propositional-component
                                                  (Π-closure ext  λ _ →
                                                   /-is-set λ _ _ → R-prop) ⟩□
    ([ g₁ ] , [g₁]→≡f) ≡ ([ g₂ ] , [g₂]→≡f)  □

  opaque

    from₂ : ∀ f → ∥ [_]→ ⁻¹ f ∥ → ℕ→/-comm-to ⁻¹ f
    from₂ f =
      _≃_.to
        (TruncP.constant-function≃∥inhabited∥⇒inhabited
           (Σ-closure 
              (/-is-set λ _ _ →
                 →ᴾ-preserves-Is-proposition R ext R-prop) λ _ →
              mono₁  (Π-closure ext  (λ _ → /-is-set λ _ _ → R-prop))))
        (from₁ f , from₁-constant f)

    unblock-from₂ : ∀ f p → from₂ f ∣ p ∣ ≡ from₁ f p
    unblock-from₂ _ _ = refl _

  opaque

    from₃ : (f : ℕ → A / R) → ℕ→/-comm-to ⁻¹ f
    from₃ f = from₂ f ([]→-surjective f)

    from : (ℕ → A / R) → (ℕ → A) / (ℕ →ᴾ R)
    from f = proj₁ (from₃ f)

    to∘from : ∀ f → ℕ→/-comm-to (from f) ≡ f
    to∘from f = proj₂ (from₃ f)

    from∘to : ∀ f → from (ℕ→/-comm-to f) ≡ f
    from∘to = elim-prop λ where
      .[]ʳ f →
        from (ℕ→/-comm-to [ f ])                      ≡⟨⟩
        proj₁ (from₂ [ f ]→ ([]→-surjective [ f ]→))  ≡⟨ cong (proj₁ ∘ from₂ [ f ]→) $ TruncP.truncation-is-proposition _ _ ⟩
        proj₁ (from₂ [ f ]→ ∣ f , refl _ ∣)           ≡⟨ cong proj₁ $ unblock-from₂ _ (f , refl _) ⟩
        proj₁ (from₁ [ f ]→ (f , refl _))             ≡⟨⟩
        [ f ]                                         ∎
      .is-propositionʳ _ →
        /-is-set λ _ _ →
          →ᴾ-preserves-Is-proposition R ext R-prop

------------------------------------------------------------------------
-- Quotient-like eliminators

-- If there is a split surjection from a quotient type to some other
-- type, then one can construct a quotient-like eliminator for the
-- other type.
--
-- This kind of construction is used in "Quotienting the Delay Monad
-- by Weak Bisimilarity" by Chapman, Uustalu and Veltri.

↠-eliminator :
  (surj : A / R ↠ B)
  (P : B → Type p)
  (p-[] : ∀ x → P (_↠_.to surj [ x ])) →
  (∀ {x y} (r : R x y) →
   subst P (cong (_↠_.to surj) ([]-respects-relation r)) (p-[] x) ≡
   p-[] y) →
  ((∀ x y → Is-proposition (R x y)) → ∀ x → Is-set (P x)) →
  ∀ x → P x
↠-eliminator surj P p-[] ok P-set x =
  subst P (_↠_.right-inverse-of surj x) p′
  where
  p′ : P (_↠_.to surj (_↠_.from surj x))
  p′ = elim
    (λ where
       .[]ʳ                             → p-[]
       .[]-respects-relationʳ {x} {y} r →
         subst (P ∘ _↠_.to surj) ([]-respects-relation r) (p-[] x)       ≡⟨ subst-∘ P (_↠_.to surj) ([]-respects-relation r) ⟩
         subst P (cong (_↠_.to surj) ([]-respects-relation r)) (p-[] x)  ≡⟨ ok r ⟩∎
         p-[] y                                                          ∎
       .is-setʳ prop _ → P-set prop _)
    (_↠_.from surj x)

-- The eliminator "computes" in the "right" way for elements that
-- satisfy a certain property, assuming that the quotient relation is
-- pointwise propositional.

↠-eliminator-[] :
  ∀ (surj : A / R ↠ B)
  (P : B → Type p)
  (p-[] : ∀ x → P (_↠_.to surj [ x ]))
  (ok : ∀ {x y} (r : R x y) →
        subst P (cong (_↠_.to surj) ([]-respects-relation r)) (p-[] x) ≡
        p-[] y)
  (P-set : (∀ x y → Is-proposition (R x y)) → ∀ x → Is-set (P x))
  x →
  (∀ {x y} → Is-proposition (R x y)) →
  _↠_.from surj (_↠_.to surj [ x ]) ≡ [ x ] →
  ↠-eliminator surj P p-[] ok P-set (_↠_.to surj [ x ]) ≡ p-[] x
↠-eliminator-[] {R} surj P p-[] ok P-set x R-prop hyp =
  subst P (_↠_.right-inverse-of surj (_↠_.to surj [ x ]))
    (elim e′ (_↠_.from surj (_↠_.to surj [ x ])))          ≡⟨ cong (λ p → subst P p (elim e′ _)) $
                                                              H.respects-surjection surj  (/-is-set λ _ _ → R-prop)
                                                                (_↠_.right-inverse-of surj (_↠_.to surj [ x ]))
                                                                (cong (_↠_.to surj) hyp) ⟩
  subst P (cong (_↠_.to surj) hyp)
    (elim e′ (_↠_.from surj (_↠_.to surj [ x ])))          ≡⟨ D.elim
                                                                (λ {x y} p → subst P (cong (_↠_.to surj) p) (elim e′ x) ≡ elim e′ y)
                                                                (λ y →
      subst P (cong (_↠_.to surj) (refl _)) (elim e′ y)            ≡⟨ cong (λ p → subst P p (elim e′ _)) $ cong-refl (_↠_.to surj) ⟩
      subst P (refl _) (elim e′ y)                                 ≡⟨ subst-refl P _ ⟩∎
      elim e′ y                                                    ∎)
                                                                hyp ⟩
  elim e′ [ x ]                                            ≡⟨⟩

  p-[] x                                                   ∎
  where
  e′ = _

-- If there is a bijection from a quotient type to some other type,
-- then one can also construct a quotient-like eliminator for the
-- other type.

↔-eliminator :
  (bij : A / R ↔ B)
  (P : B → Type p)
  (p-[] : ∀ x → P (_↔_.to bij [ x ])) →
  (∀ {x y} (r : R x y) →
   subst P (cong (_↔_.to bij) ([]-respects-relation r)) (p-[] x) ≡
   p-[] y) →
  ((∀ x y → Is-proposition (R x y)) → ∀ x → Is-set (P x)) →
  ∀ x → P x
↔-eliminator bij = ↠-eliminator (_↔_.surjection bij)

-- This latter eliminator always "computes" in the "right" way,
-- assuming that the quotient relation is pointwise propositional.

↔-eliminator-[] :
  ∀ (bij : A / R ↔ B)
  (P : B → Type p)
  (p-[] : ∀ x → P (_↔_.to bij [ x ]))
  (ok : ∀ {x y} (r : R x y) →
        subst P (cong (_↔_.to bij) ([]-respects-relation r)) (p-[] x) ≡
        p-[] y)
  (P-set : (∀ x y → Is-proposition (R x y)) → ∀ x → Is-set (P x)) x →
  (∀ {x y} → Is-proposition (R x y)) →
  ↔-eliminator bij P p-[] ok P-set (_↔_.to bij [ x ]) ≡ p-[] x
↔-eliminator-[] bij P p-[] ok P-set x R-prop =
  ↠-eliminator-[] (_↔_.surjection bij) P p-[] ok P-set x
    R-prop
    (_↔_.left-inverse-of bij [ x ])

-- A quotient-like eliminator for functions of type ℕ → A / R, where R
-- is a propositional equivalence relation. Defined using countable
-- choice and propositional extensionality.
--
-- This eliminator is taken from Corollary 1 in "Quotienting the Delay
-- Monad by Weak Bisimilarity" by Chapman, Uustalu and Veltri.

ℕ→/-elim :
  {A : Type a} {R : A → A → Type r} →
  Axiom-of-countable-choice (a ⊔ r) →
  Propositional-extensionality r →
  Is-equivalence-relation R →
  (∀ {x y} → Is-proposition (R x y)) →
  (P : (ℕ → A / R) → Type p)
  (p-[] : ∀ f → P (λ n → [ f n ])) →
  (∀ {f g} (r : (ℕ →ᴾ R) f g) →
   subst P (cong ℕ→/-comm-to ([]-respects-relation r)) (p-[] f) ≡
   p-[] g) →
  (∀ f → Is-set (P f)) →
  ∀ f → P f
ℕ→/-elim cc prop-ext R-equiv R-prop P p-[] ok P-set =
  ↔-eliminator
    (ℕ→/-comm cc prop-ext R-equiv R-prop)
    P p-[] ok (λ _ → P-set)

-- The eliminator "computes" in the "right" way.

ℕ→/-elim-[] :
  ∀ {A : Type a} {R : A → A → Type r}
  (cc : Axiom-of-countable-choice (a ⊔ r))
  (prop-ext : Propositional-extensionality r)
  (R-equiv : Is-equivalence-relation R)
  (R-prop : ∀ {x y} → Is-proposition (R x y))
  (P : (ℕ → A / R) → Type p)
  (p-[] : ∀ f → P (λ n → [ f n ]))
  (ok : ∀ {f g} (r : (ℕ →ᴾ R) f g) →
        subst P (cong ℕ→/-comm-to ([]-respects-relation r)) (p-[] f) ≡
        p-[] g)
  (P-set : ∀ f → Is-set (P f)) f →
  ℕ→/-elim cc prop-ext R-equiv R-prop P p-[] ok P-set (λ n → [ f n ]) ≡
  p-[] f
ℕ→/-elim-[] {R} cc prop-ext R-equiv R-prop P p-[] ok P-set f =
  ↔-eliminator-[]
    (ℕ→/-comm cc prop-ext R-equiv R-prop)
    P p-[] ok (λ _ → P-set) f
    (→ᴾ-preserves-Is-proposition R ext R-prop)