{-# OPTIONS --rewriting #-}

module Quotient where

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

infix 6 _/_ [_]/_
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)