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

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

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

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

open import Equality

module Quotient.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 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 = 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 = R} ext univ R-equiv R-prop {x = x} {y = y} =

  Eq.↔⇒≃ (record
    { surjection = record
      { logical-equivalence = record
        { to = λ Rxy → apply-ext (lower-extensionality r lzero ext) λ z →
                 ≃⇒≡ univ $
                 _↔_.to (Eq.⇔↔≃ (lower-extensionality a _ ext)
                                (R-prop x z) (R-prop y z))
                 (R x z  ↝⟨ record { to   = transitive (symmetric Rxy)
                                   ; from = transitive Rxy
                                   } ⟩□
                  R y z  □)
        ; from = λ Rx≡Ry →        $⟨ reflexive ⟩
                           R y y  ↝⟨ subst (_$ y) (sym Rx≡Ry) ⟩□
                           R x y  □
        }
      ; right-inverse-of = λ _ →
          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 = x} {y = y} =
  x ≡ y                      ↝⟨ inverse $ Π≡≃≡-↔-≡ _ _ (lower-extensionality lzero _ ext) ⟩
  (∀ z → (z ≡ x) ≃ (z ≡ y))  ↝⟨ (∀-cong (lower-extensionality lzero _ ext) λ _ → Eq.↔⇒≃ $
                                 Eq.≃-preserves-bijections (lower-extensionality lzero _ ext)
                                   (Groupoid.⁻¹-bijection (EG.groupoid _))
                                   (Groupoid.⁻¹-bijection (EG.groupoid _))) ⟩
  (∀ z → (x ≡ z) ≃ (y ≡ z))  ↝⟨ (∀-cong ext λ _ → inverse $ ≡≃≃ univ) ⟩
  (∀ z → (x ≡ z) ≡ (y ≡ z))  ↝⟨ Eq.extensionality-isomorphism ext ⟩□
  (x ≡_) ≡ (y ≡_)            □

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

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

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

equivalence-but-not-strong-equivalence :
  Extensionality (# 0) (# 1) →
  Univalence (# 0) →
  ∃ λ (A : 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 = a} {b} {R = 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 = 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 = 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} 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))

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


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

module Definition.Typed.Consequences.Injectivity where

open import Definition.Untyped hiding (wk)
import Definition.Untyped as U
open import Definition.Untyped.Properties

open import Definition.Typed
open import Definition.Typed.Weakening
open import Definition.Typed.Properties
open import Definition.Typed.EqRelInstance
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Fundamental.Reducibility

open import Tools.Embedding
open import Tools.Product
import Tools.PropositionalEquality as PE

-- Helper function of injectivity for specific reducible Π-types
injectivity′ : ∀ {F G H E Γ l}
               ([ΠFG] : Γ ⊩⟨ l ⟩Π Π F ▹ G)
             → Γ ⊩⟨ l ⟩ Π F ▹ G ≡ Π H ▹ E / Π-intr [ΠFG]
             → Γ ⊢ F ≡ H
             × Γ ∙ F ⊢ G ≡ E
injectivity′ (noemb (Πᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext))
         (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  let F≡F₁ , G≡G₁ = Π-PE-injectivity (whnfRed* (red D) Πₙ)
      H≡F′ , E≡G′ = Π-PE-injectivity (whnfRed* D′ Πₙ)
      ⊢Γ = wf ⊢F
      [F]₁ = [F] id ⊢Γ
      [F]′ = irrelevance′ (PE.trans (wk-id _) (PE.sym F≡F₁)) [F]₁
      [x∷F] = neuTerm ([F] (step id) (⊢Γ ∙ ⊢F)) (var 0) (var (⊢Γ ∙ ⊢F) here)
                      (refl (var (⊢Γ ∙ ⊢F) here))
      [G]₁ = [G] (step id) (⊢Γ ∙ ⊢F) [x∷F]
      [G]′ = PE.subst₂ (λ x y → _ ∙ y ⊩⟨ _ ⟩ x)
                       (PE.trans (wkSingleSubstId _) (PE.sym G≡G₁))
                       (PE.sym F≡F₁) [G]₁
      [F≡H]₁ = [F≡F′] id ⊢Γ
      [F≡H]′ = irrelevanceEq″ (PE.trans (wk-id _) (PE.sym F≡F₁))
                               (PE.trans (wk-id _) (PE.sym H≡F′))
                               [F]₁ [F]′ [F≡H]₁
      [G≡E]₁ = [G≡G′] (step id) (⊢Γ ∙ ⊢F) [x∷F]
      [G≡E]′ = irrelevanceEqLift″ (PE.trans (wkSingleSubstId _) (PE.sym G≡G₁))
                                   (PE.trans (wkSingleSubstId _) (PE.sym E≡G′))
                                   (PE.sym F≡F₁) [G]₁ [G]′ [G≡E]₁
  in  escapeEq [F]′ [F≡H]′ , escapeEq [G]′ [G≡E]′
injectivity′ (emb 0<1 x) (ιx [ΠFG≡ΠHE]) = injectivity′ x [ΠFG≡ΠHE]

-- Injectivity of Π
injectivity : ∀ {Γ F G H E} → Γ ⊢ Π F ▹ G ≡ Π H ▹ E → Γ ⊢ F ≡ H × Γ ∙ F ⊢ G ≡ E
injectivity ⊢ΠFG≡ΠHE =
  let [ΠFG] , _ , [ΠFG≡ΠHE] = reducibleEq ⊢ΠFG≡ΠHE
  in  injectivity′ (Π-elim [ΠFG])
                   (irrelevanceEq [ΠFG] (Π-intr (Π-elim [ΠFG])) [ΠFG≡ΠHE])

ext: agda

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
import Relation.Binary.PropositionalEquality as PEq

module Relation.Binary.PropositionalEquality.Extensionality
  (funext : ∀ {ℓ₁ ℓ₂} → PEq.Extensionality ℓ₁ ℓ₂) where

funext² : ∀ {p q r}{P : Set p}{Q : P → Set q}
          {R : (p : P) → Q p → Set r} →
          {f g : ∀ (p : P)(q : Q p) → R p q} → (∀ p q → f p q PEq.≡ g p q) →
          f PEq.≡ g
funext² f = funext λ p → funext λ q → f p q

funext³ : ∀ {p q r s}{P : Set p}{Q : P → Set q}
          {R : (p : P) → Q p → Set r}{S : (p : P)(q : Q p) → R p q → Set s} →
          {f g : ∀ (p : P)(q : Q p)(r : R p q) → S p q r} → (∀ p q r → f p q r PEq.≡ g p q r) →
          f PEq.≡ g
funext³ f = funext λ p → funext λ q → funext λ r → f p q r


text:
{-# OPTIONS --prop --without-K --rewriting #-}

module Data.Nat.Log2 where

open import Data.Nat
open import Data.Nat.Properties

open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)

open import Agda.Builtin.Equality.Rewrite

private
  aux : (P : ℕ → Set) → P zero → P (suc zero) → ((n : ℕ) → P ⌈ suc (suc n) /2⌉ → P (suc (suc n))) →
    (n : ℕ) → (m : ℕ) → m ≤ n → P m
  aux P bc₀ bc₁ is n zero h = bc₀
  aux P bc₀ bc₁ is n (suc zero) h = bc₁
  aux P bc₀ bc₁ is (suc (suc n)) (suc (suc m)) (s≤s (s≤s h)) =
    is m (aux P bc₀ bc₁ is (suc n) ⌈ suc (suc m) /2⌉ (s≤s (≤-trans (⌈n/2⌉≤n m) h)))

strong-induction : (P : ℕ → Set) → P zero → P (suc zero) → ((n : ℕ) → P ⌈ suc (suc n) /2⌉ → P (suc (suc n))) → (n : ℕ) → P n
strong-induction P bc₀ bc₁ is n = aux P bc₀ bc₁ is n n ≤-refl

strong-induction/is : ∀ {P bc₀ bc₁ is n} →
  aux P bc₀ bc₁ is (suc n) ⌈ suc (suc n) /2⌉ (s≤s (≤-trans (⌈n/2⌉≤n n) ≤-refl)) ≡
  strong-induction P bc₀ bc₁ is ⌈ suc (suc n) /2⌉
strong-induction/is {P} {bc₀} {bc₁} {is} {n} = aux/unique
  where
    aux/unique : ∀ {m n₁ n₂ h₁ h₂} → aux P bc₀ bc₁ is n₁ m h₁ ≡ aux P bc₀ bc₁ is n₂ m h₂
    aux/unique {zero} = refl
    aux/unique {suc zero} = refl
    aux/unique {suc (suc m)} {h₁ = s≤s (s≤s h₁)} {h₂ = s≤s (s≤s h₂)} = Eq.cong (is m) aux/unique
{-# REWRITE strong-induction/is #-}

⌈log₂_⌉ : ℕ → ℕ
⌈log₂_⌉ = strong-induction (λ _ → ℕ) zero zero (λ _ → suc)

log₂-mono : ⌈log₂_⌉ Preserves _≤_ ⟶ _≤_
log₂-mono {n₁} {n₂} =
  strong-induction (λ n₁ → ∀ n₂ → n₁ ≤ n₂ → ⌈log₂ n₁ ⌉ ≤ ⌈log₂ n₂ ⌉)
    (λ _ _ → z≤n)
    (λ _ _ → z≤n)
    (λ { n₁ ih (suc (suc n₂)) (s≤s (s≤s h)) → s≤s (ih ⌈ suc (suc n₂) /2⌉ (⌈n/2⌉-mono (s≤s (s≤s h))))})
    n₁
    n₂

⌈log₂n⌉≤n : ∀ n → ⌈log₂ n ⌉ ≤ n
⌈log₂n⌉≤n n = strong-induction' n n ≤-refl
  where
    strong-induction' : (n m : ℕ) → m ≤ n → ⌈log₂ m ⌉ ≤ m
    strong-induction' n zero    h = z≤n
    strong-induction' n (suc zero) h = z≤n
    strong-induction' (suc (suc n)) (suc (suc m)) (s≤s (s≤s h)) =
      s≤s (
        let open ≤-Reasoning in
        begin
          ⌈log₂ suc ⌈ m /2⌉ ⌉
        ≤⟨ strong-induction' (suc n) (suc ⌈ m /2⌉) (s≤s (≤-trans (⌈n/2⌉≤n m) h)) ⟩
          suc ⌈ m /2⌉
        ≤⟨ s≤s (⌈n/2⌉≤n m) ⟩
          suc m
        ∎
      )

log₂-suc : ∀ n {k} → ⌈log₂ n ⌉ ≤ suc k → ⌈log₂ ⌈ n /2⌉ ⌉ ≤ k
log₂-suc zero h = z≤n
log₂-suc (suc zero) h = z≤n
log₂-suc (suc (suc n)) (s≤s h) = h

⌈log₂n⌉≡0⇒n≤1 : {n : ℕ} → ⌈log₂ n ⌉ ≡ 0 → n ≤ 1
⌈log₂n⌉≡0⇒n≤1 {zero} refl = z≤n
⌈log₂n⌉≡0⇒n≤1 {suc zero} refl = s≤s z≤n

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
import      Lvl

module Structure.Category.Dual {ℓₒ ℓₘ ℓₑ : Lvl.Level} where

open import Data.Tuple as Tuple using ()
open import Functional using (swap)
open import Structure.Category
open import Structure.Categorical.Names
open import Structure.Categorical.Properties
import      Structure.Operator.Properties as Properties
open import Structure.Operator
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Structure.Setoid
open import Type

module _
  {Obj : Type{ℓₒ}}
  {Morphism : Obj → Obj → Type{ℓₘ}}
  ⦃ morphism-equiv : ∀{x y} → Equiv{ℓₑ}(Morphism x y) ⦄
  (cat : Category(Morphism))
  where

  open Category.ArrowNotation(cat)
  open Category(cat)
  private open module MorphismEquiv {x}{y} = Equivalence (Equiv-equivalence ⦃ morphism-equiv{x}{y} ⦄) using ()

  -- The opposite/dual category of a category.
  dualCategory : Category(_⟵_)
  Category._∘_ dualCategory = swap(_∘_)
  Category.id  dualCategory = id
  BinaryOperator.congruence             (Category.binaryOperator dualCategory) p₁ p₂ = congruence₂(_∘_) p₂ p₁
  Morphism.Associativity.proof          (Category.associativity  dualCategory)  = symmetry(_≡_) (Morphism.associativity(_∘_))
  Morphism.Identityₗ.proof (Tuple.left  (Category.identity       dualCategory)) = Morphism.identity-right(_∘_)(id)
  Morphism.Identityᵣ.proof (Tuple.right (Category.identity       dualCategory)) = Morphism.identity-left (_∘_)(id)

dual : CategoryObject{ℓₒ}{ℓₘ} → CategoryObject{ℓₒ}{ℓₘ}
dual(intro cat) = intro(dualCategory cat)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module RecordsAndModules where

module Setoids where

  record Equiv (a : Set) : Set where
    field
      x : a
      y : a

  record Setoid : Set1 where
    field
      carrier : Set
      equiv   : Equiv carrier

module RegExps (S : Setoids.Setoid) where

  data RegExp : Set where
    ε : RegExp

module SimpleMatcher (S : Setoids.Setoid) where

  open module R = RegExps S

  foo : RegExp -> RegExp
  foo ε = ε

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- The values of terms in Nehemiah.Change.Term.
------------------------------------------------------------------------

module Nehemiah.Change.Value where

open import Nehemiah.Syntax.Type
open import Nehemiah.Syntax.Term
open import Nehemiah.Denotation.Value

open import Data.Integer
open import Structure.Bag.Nehemiah

import Parametric.Change.Value Const ⟦_⟧Base ΔBase as ChangeValue

⟦apply-base⟧ : ChangeValue.ApplyStructure
⟦apply-base⟧ base-int n Δn = n +  Δn
⟦apply-base⟧ base-bag b Δb = b ++ Δb

⟦diff-base⟧ : ChangeValue.DiffStructure
⟦diff-base⟧ base-int m n = m -  n
⟦diff-base⟧ base-bag a b = a \\ b

⟦nil-base⟧ : ChangeValue.NilStructure
⟦nil-base⟧ base-int n = + 0
⟦nil-base⟧ base-bag b = emptyBag

open ChangeValue.Structure ⟦apply-base⟧ ⟦diff-base⟧ ⟦nil-base⟧ public

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
module Data.QuadTree.Implementation.Functors where

open import Haskell.Prelude renaming (zero to Z; suc to S)
open import Data.Lens.Lens
open import Data.Logic
open import Data.QuadTree.Implementation.Definition
open import Data.QuadTree.Implementation.ValidTypes
open import Data.QuadTree.Implementation.QuadrantLenses

{-# FOREIGN AGDA2HS
{-# LANGUAGE Safe #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE Rank2Types #-}
import Data.Nat
import Data.Lens.Lens
import Data.Logic
import Data.QuadTree.Implementation.Definition
import Data.QuadTree.Implementation.ValidTypes
import Data.QuadTree.Implementation.QuadrantLenses
#-}

record FunctorEq (f : (y : Set) -> {{ eqT : Eq y }} -> Set) : Set₁ where
  field
    fmapₑ : {a b : Set} -> {{ eqA : Eq a }} {{ eqB : Eq b }} -> (a → b) → f a → f b
open FunctorEq public
{-# COMPILE AGDA2HS FunctorEq class #-}

quadrantFunctor : (dep : Nat) -> FunctorEq (λ y -> VQuadrant y {dep})
quadrantFunctor dep .fmapₑ fn (CVQuadrant (Leaf v) {p}) = (CVQuadrant (Leaf $ fn v) {p})
quadrantFunctor (S dep) .fmapₑ fn (CVQuadrant (Node a b c d) {p}) =
  (combine (fmapₑ (quadrantFunctor dep) fn sA) (fmapₑ (quadrantFunctor dep) fn sB) (fmapₑ (quadrantFunctor dep) fn sC) (fmapₑ (quadrantFunctor dep) fn sD)) where
  sA = CVQuadrant a {aSub a b c d p}
  sB = CVQuadrant b {bSub a b c d p}
  sC = CVQuadrant c {cSub a b c d p}
  sD = CVQuadrant d {dSub a b c d p}

toQt : {b : Set} -> {{ eqB : Eq b }}
  -> (dep w h : Nat) .(q : IsTrue (dep == log2up (if w < h then h else w))) -> VQuadrant b {dep} -> VQuadTree b {dep}
toQt dep w h q (CVQuadrant qd {p}) = CVQuadTree (Wrapper (w , h) qd) {p} {q}

quadtreeFunctor : (dep : Nat) -> FunctorEq (λ y -> VQuadTree y {dep})
quadtreeFunctor dep .fmapₑ {a} {b} fn (CVQuadTree (Wrapper (w , h) qd) {p} {q}) =
  toQt dep w h q (fmapₑ (quadrantFunctor dep) fn (CVQuadrant qd {p}))

max_stars_repo_name: JonathanBrouwer/research-project

max_issues_repo_name: JonathanBrouwer/research-project

max_forks_repo_name: JonathanBrouwer/research-project


text:
module Issue978 where

module A where

  infixr 4 _,_

  record _×_ (A B : Set) : Set where
    constructor _,_
    field
      fst : A
      snd : B

module B where

  infixl 2 _,_

  data Ty : Set where

  data Cxt : Set where
    ε   : Cxt
    _,_ : (Γ : Cxt) (a : Ty) → Cxt

open A
open B

test : (Γ : Cxt) → Set₁
test ε = Set
test (ε , a) = ?
test (Γ , a , a₁) = ?

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda