# 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

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