Set presented types

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

Created on 2022-02-17.
Last modified on 2023-06-10.

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

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

Idea

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.

has-set-presentation-Prop :
  {l1 l2 : Level} (A : Set l1) (B : UU l2) → Prop (l1 ⊔ l2)
has-set-presentation-Prop A B =
  ∃-Prop (type-Set A → B) (λ f → is-equiv (unit-trunc-Set ∘ f))

Recent changes