{-# OPTIONS --rewriting #-}

module Quotient where

open import Agda.Builtin.TrustMe
open import Equality
open import EqualityRewriting
open import Level
open import UIP

infix  _/_ [_]/_
postulate
  -- quotient formation
  _/_ : {ℓ ℓ' : Level}(A : Set ℓ)(R : A → A → Set ℓ') → Set (ℓ ⊔ ℓ')
  -- quotient introduction
  [_]/_ : {ℓ ℓ' : Level}{A : Set ℓ} → A → (R : A → A → Set ℓ') → A / R

{-# POLARITY _/_ * * ++ * #-}

-- generating equalities
by :
  {ℓ ℓ' : Level}
  {A : Set ℓ}
  {x y : A}
  {R : A → A → Set ℓ'}
  (r : R x y)
  → ------------------
  [ x ]/ R ≡ [ y ]/ R
by _ = primTrustMe

postulate
  -- quotient elimination
  qelim :
    {ℓ ℓ' ℓ'' : Level}
    {A : Set ℓ}
    (R : A → A → Set ℓ')
    (B : A / R → Set ℓ'')
    (f : (x : A) → B ([ x ]/ R))
    (e : (x y : A)(r : R x y) → subst B (by r) (f x) ≡ f y)
    → -----------------------------------------------------
    (y : A / R) → B y

  -- quotient computation
  qcomp :
    {ℓ ℓ' ℓ'' : Level}
    {A : Set ℓ}
    (R : A → A → Set ℓ')
    (B : A / R → Set ℓ'')
    (f : (x : A) → B ([ x ]/ R))
    (e : (x y : A)(r : R x y) → subst B (by r) (f x) ≡ f y)
    (x : A)
    → -----------------------------------------------------
    qelim R B f e ([ x ]/ R) ≡ f x

{-# REWRITE qcomp   #-}

--quotient recursion
qrec :
  {ℓ ℓ' ℓ'' : Level}
  {A : Set ℓ}
  (R : A → A → Set ℓ')
  (B : Set ℓ'')
  (f : A → B)
  (e : (x y : A)(r : R x y) → f x ≡ f y)
  → ------------------------------------
  A / R → B
qrec R B f e =
  qelim R (λ _ → B) f
  (λ x y r → trans (e x y r) (subst-const (by r) (f x))) where
  subst-const :
    {ℓ ℓ' : Level}
    {A : Set ℓ}
    {B : Set ℓ'}
    {x y : A}
    (p : x ≡ y)
    (b : B)
    → ---------------------
    subst (λ _ → B) p b ≡ b
  subst-const refl _ = refl

qrec-comp :
  {ℓ ℓ' ℓ'' : Level}
  {A : Set ℓ}
  (R : A → A → Set ℓ')
  (B : Set ℓ'')
  (f : A → B)
  (e : (x y : A)(r : R x y) → f x ≡ f y)
  (x : A)
  → ------------------------------------
  qrec R B f e ([ x ]/ R) ≡ f x
qrec-comp _ _ _ _ _ = refl

qrec-uniq :
  {ℓ ℓ' ℓ'' : Level}
  {A : Set ℓ}
  (R : A → A → Set ℓ')
  (B : Set ℓ'')
  (f : A → B)
  (e : (x y : A)(r : R x y) → f x ≡ f y)
  (g : A / R → B)
  (_ : (x : A) → f x ≡ g ([ x ]/ R))
  → ------------------------------------
  (y : A / R) → qrec R B f e y ≡ g y
qrec-uniq R B f e g h =
  qelim R (λ y → qrec R B f e y ≡ g y)
  (λ x → trans (h x) (qrec-comp R B f e x))
  (λ _ _ _  → uip)