Images of subtypes
Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Victor Blanchi.
Created on 2022-09-15.
Last modified on 2023-06-10.
module foundation.images-subtypes where
Imports
open import foundation.images open import foundation.universe-levels open import foundation-core.function-types open import foundation-core.subtypes
Idea
Consider a map f : A → B
and a subtype S ⊆ A
, then the images of S
under
f
is the subtype of B
consisting of the values of the composite S ⊆ A → B
.
Definition
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) where subtype-im-subtype : {l3 : Level} → subtype l3 A → subtype (l1 ⊔ l2 ⊔ l3) B subtype-im-subtype S y = subtype-im (f ∘ inclusion-subtype S) y
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-03-21. Fredrik Bakke. Formatting fixes (#530).
- 2023-03-21. Victor Blanchi. Associativity of species composition (#478).
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).