Set presented types

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

Created on 2022-02-17.
Last modified on 2024-04-11.

module foundation.set-presented-types where
open import foundation.equivalences
open import foundation.existential-quantification
open import foundation.set-truncations
open import foundation.universe-levels

open import foundation-core.function-types
open import foundation-core.propositions
open import foundation-core.sets


A type A is said to be set presented if there exists a map f : X → A from a set X such that the composite X → A → type-trunc-Set A is an equivalence.

module _
  {l1 l2 : Level} (A : Set l1) (B : UU l2)

  has-set-presentation-Prop : Prop (l1  l2)
  has-set-presentation-Prop =
     (type-Set A  B)  f  is-equiv-Prop (unit-trunc-Set  f))

Recent changes