Effective maps for equivalence relations

module foundation.effective-maps-equivalence-relations where

Imports

open import foundation.surjective-maps

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

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 : Eq-Rel 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-Eq-Rel R x y

Maps that are effective and surjective

module _
  {l1 l2 : Level} {A : UU l1} (R : Eq-Rel 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