Epimorphisms

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-04-26.
Last modified on 2023-06-10.

module foundation.epimorphisms where
Imports 
open import foundation.universe-levels

open import foundation-core.embeddings
open import foundation-core.function-types

Idea

A map f : A → B is said to be an epimorphism if the precomposition function

  - ∘ f : (B → X) → (A → X)

is an embedding for every type X.

Definitions

is-epimorphism :
  {l1 l2 : Level} (l : Level) {A : UU l1} {B : UU l2} →
  (A → B) → UU (l1 ⊔ l2 ⊔ lsuc l)
is-epimorphism l f = (X : UU l) → is-emb (precomp f X)

Recent changes