This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Preimages of subtypes

module foundation.preimages-of-subtypes where
Imports 
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)