This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Effective maps for equivalence relations

module foundation.effective-maps-equivalence-relations where
Imports 
open import foundation.surjective-maps
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.equivalence-relations
open import foundation-core.equivalences
open import foundation-core.identity-types

Idea

Consider a type A equipped with an equivalence relation R, and let f : A → X be a map. Then f is effective if R x y ≃ Id (f x) (f y) for all x y : A. If f is both effective and surjective, then it follows that X satisfies the universal property of the quotient A/R.

Definition

Effective maps

is-effective :
  {l1 l2 l3 : Level} {A : UU l1} (R : equivalence-relation l2 A) {B : UU l3}
  (f : A → B) → UU (l1 ⊔ l2 ⊔ l3)
is-effective {A = A} R f =
  (x y : A) → (f x ＝ f y) ≃ sim-equivalence-relation R x y

Maps that are effective and surjective

module _
  {l1 l2 : Level} {A : UU l1} (R : equivalence-relation l2 A)
  where

  is-surjective-and-effective :
    {l3 : Level} {B : UU l3} (f : A → B) → UU (l1 ⊔ l2 ⊔ l3)
  is-surjective-and-effective f = is-surjective f × is-effective R f