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
Imports 
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

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.

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

  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