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
- 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490).