-- Martin Escardo, 3rd August 2015

{-# OPTIONS --without-K #-}

module quotient where

open import preliminaries
open import prop
open import proptrunc

image : {i : Level} {X A : U i} → (X → A) → U i
image {i} {X} {A} f = Σ \(a : A) → ∥(Σ \(x : X) → f x ≡ a)∥

_/_ : {i : Level} (X : U i) (R : X → X → Prop) → U i
X / R = image R

_mod_ : {i : Level} {X : U i} (x : X) (R : X → X → Prop) → X / R
x mod R = R x , ∣ x , refl(R x) ∣

-- Elimination from a quotient takes more work. I will complete this later:
{-
 /-elim : {X A : U} (R : X → X → Prop) (f : X → A)
       → isSet A → ((x y : X) → (R x y) holds → f x ≡ f y) → X / R → A
/-elim {X} {A} R f iss ext (φ , P) = ?
-}