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


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.


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