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
- 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-05-16. Fredrik Bakke. Swap from
md
totext
code blocks (#622). - 2023-04-28. Fredrik Bakke. Miscellaneous refactoring and small additions (#579).
- 2023-04-26. Egbert Rijke and Fredrik Bakke. Acyclic maps (#565).