-- 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) = ?
-}