Effective maps for equivalence relations

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Julian KG, fernabnor and louismntnu.

Created on 2022-02-17.
Last modified on 2023-11-24.

module foundation.effective-maps-equivalence-relations where
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


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.


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)

  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

Recent changes