Injective maps
Content created by Egbert Rijke, Fredrik Bakke and Jonathan Prieto-Cubides.
Created on 2022-01-26.
Last modified on 2023-06-08.
module foundation.injective-maps where open import foundation-core.injective-maps public
Imports
open import foundation.universe-levels open import foundation-core.empty-types open import foundation-core.negation
Idea
A map f : A → B
is injective if f x = f y
implies x = y
.
Warning
The notion of injective map is, however, not homotopically coherent. It is fine to use injectivity for maps between sets, but for maps between general types it is recommended to use the notion of embedding.
Definitions
Non-injective maps
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} where is-not-injective : (A → B) → UU (l1 ⊔ l2) is-not-injective f = ¬ (is-injective f)
Any map out of an empty type is injective
is-injective-is-empty : {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → is-empty A → is-injective f is-injective-is-empty f is-empty-A {x} = ex-falso (is-empty-A x)
Recent changes
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-06-07. Fredrik Bakke. Move public imports before "Imports" block (#642).
- 2023-04-28. Fredrik Bakke. Miscellaneous refactoring and small additions (#579).
- 2023-04-08. Egbert Rijke. Refactoring elementary number theory files (#546).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).