Preimages of subtypes

Content created by Jonathan Prieto-Cubides, Fredrik Bakke and Egbert Rijke.

Created on 2022-09-15.
Last modified on 2023-06-08.

module foundation.preimages-of-subtypes where

open import foundation.universe-levels

open import foundation-core.subtypes

Idea

The preimage of a subtype S ⊆ B under a map f : A → B is the subtype of A consisting of elements a such that f a ∈ S.

Definition

preimage-subtype :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
  subtype l3 B → subtype l3 A
preimage-subtype f S a = S (f a)

Recent changes

• 2023-06-08. Fredrik Bakke. Remove empty foundation modules and replace them by their core counterparts (#644).
• 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
• 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
• 2023-03-07. Fredrik Bakke. Add blank lines between <details> tags and markdown syntax (#490).
• 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).