{-# 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