{-# OPTIONS --prop --rewriting --confluence-check #-}
module Quotient where

open import Agda.Primitive
open import Lib

record EqRel {i j} {A : Set i} (P : A  A  Prop j) : Prop (i  j) where
  field
    R :  {x}  P x x
    S :  {x y}  P x y  P y x
    T :  {x y z}  P x y  P y z  P x z

module _ {i j} (A : Set i) (P : A  A  Prop j) where
  postulate
    _//_ : Set i
    //-in : A  _//_
    //-≡ :  {x y}  P x y  //-in x  //-in y
    //-elim :  {j} (Q : _//_  Set j)
                    (//-in* : (x : A)  Q (//-in x))
                    (//-≡* : (x y : A) (r : P x y)  //-in* x L.≡[ L.ap Q (//-≡ r) ]≡ //-in* y)
               (x : _//_)  Q x
    //-elim-β :  {j P //-in* //-≡* x}  //-elim {j} P //-in* //-≡* (//-in x)  //-in* x
  {-# REWRITE //-elim-β #-}

  //-rec :  {j} (Q : Set j)
                 (//-in* : (x : A)  Q)
                 (//-≡* : (x y : A) (r : P x y)  //-in* x  //-in* y)
            _//_  Q
  //-rec P //-in* //-≡* x = //-elim  _  P) //-in*  _ _ r  L.uip-≡ {p = refl} (//-≡* _ _ r)) x

  module _ (EqRel-P : EqRel P) where
    private
      module EP = EqRel EqRel-P

    private
      code :  {x : A} (y : _//_)  Prop j
      code {x} = //-rec (Prop j) (P x)  x₁ y₁ r  propext  p  EP.T p r) λ p  EP.T p (EP.S r))

      encode :  {x : A} (y : _//_)  //-in x  y  code {x} y
      encode _ refl = EP.R

    //-≡-out :  {x y}  //-in x  //-in y  P x y
    //-≡-out {x} {y} p = encode {x} (//-in y) p