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