Set presented types
Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Elisabeth Stenholm.
Created on 2022-02-17.
Last modified on 2025-08-14.
module foundation.set-presented-types where
Imports
open import foundation.1-types open import foundation.action-on-identifications-functions open import foundation.connected-maps open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.embeddings open import foundation.empty-types open import foundation.equality-coproduct-types open import foundation.equivalences open import foundation.existential-quantification open import foundation.fibers-of-maps open import foundation.functoriality-coproduct-types open import foundation.homotopies open import foundation.identity-types open import foundation.images open import foundation.injective-maps open import foundation.propositional-truncations open import foundation.set-truncations open import foundation.sets open import foundation.subtypes open import foundation.surjective-maps open import foundation.truncation-levels open import foundation.universe-levels open import foundation-core.function-types open import foundation-core.propositions
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
η ∘ f : X → A → ║A║₀
is an equivalence.
Definitions
The underlying structure of a set presentation
is-set-presentation-map : {l1 l2 : Level} {A : UU l1} (X : Set l2) → (type-Set X → A) → UU (l1 ⊔ l2) is-set-presentation-map X f = is-equiv (unit-trunc-Set ∘ f) set-presentation-structure : {l1 l2 : Level} → UU l1 → Set l2 → UU (l1 ⊔ l2) set-presentation-structure A X = Σ (type-Set X → A) (is-set-presentation-map X) module _ {l1 l2 : Level} {A : UU l1} (X : Set l2) (f : set-presentation-structure A X) where map-set-presentation-structure : type-Set X → A map-set-presentation-structure = pr1 f is-set-presentation-map-map-set-presentation-structure : is-set-presentation-map X map-set-presentation-structure is-set-presentation-map-map-set-presentation-structure = pr2 f
The predicate on a set of being a set presentation of a type
module _ {l1 l2 : Level} (A : UU l1) (X : Set l2) where is-set-presentation-Prop : Prop (l1 ⊔ l2) is-set-presentation-Prop = trunc-Prop (set-presentation-structure A X) is-set-presentation : UU (l1 ⊔ l2) is-set-presentation = type-Prop is-set-presentation-Prop is-prop-is-set-presentation : is-prop is-set-presentation is-prop-is-set-presentation = is-prop-type-Prop is-set-presentation-Prop
The type of set presentations of a type at a universe level
module _ {l1 : Level} (l2 : Level) (A : UU l1) where set-presentation : UU (l1 ⊔ lsuc l2) set-presentation = Σ (Set l2) (is-set-presentation A) is-1-type-set-presentation : is-1-type set-presentation is-1-type-set-presentation = is-1-type-type-subtype (is-set-presentation-Prop A) is-1-type-Set
The predicate of having a set presentation at a universe level
module _ {l1 : Level} (l2 : Level) (A : UU l1) where has-set-presentation-Prop : Prop (l1 ⊔ lsuc l2) has-set-presentation-Prop = trunc-Prop (set-presentation l2 A) has-set-presentation : UU (l1 ⊔ lsuc l2) has-set-presentation = type-Prop has-set-presentation-Prop is-prop-has-set-presentation : is-prop has-set-presentation is-prop-has-set-presentation = is-prop-type-Prop has-set-presentation-Prop
Propositions
Types set presented by coproducts are coproducts
Given a type A
that is set presented by a coproduct
A
∧ \
f / \ η
/ ~ ∨
(X1 + X2) -----> ║A║₀,
then A
computes as the coproduct of the images of the restrictions of f
along the left and right inclusion of the coproduct X1 + X2
A ≃ im (f ∘ inl) + im (f ∘ inr).
module _ {l1 l2 l3 : Level} {X1 : UU l1} {X2 : UU l2} {A : UU l3} (f : X1 + X2 → A) (e : (X1 + X2) ≃ ║ A ║₀) (H : unit-trunc-Set ∘ f ~ map-equiv e) where map-is-coproduct-codomain : (im (f ∘ inl) + im (f ∘ inr)) → A map-is-coproduct-codomain = rec-coproduct pr1 pr1 triangle-is-coproduct-codomain : ( ( map-is-coproduct-codomain) ∘ ( map-coproduct (map-unit-im (f ∘ inl)) (map-unit-im (f ∘ inr)))) ~ f triangle-is-coproduct-codomain (inl x) = refl triangle-is-coproduct-codomain (inr x) = refl abstract is-emb-map-is-coproduct-codomain : is-emb map-is-coproduct-codomain is-emb-map-is-coproduct-codomain = is-emb-coproduct ( is-emb-inclusion-subtype (λ b → trunc-Prop _)) ( is-emb-inclusion-subtype (λ b → trunc-Prop _)) ( λ (b1 , u) (b2 , v) → apply-universal-property-trunc-Prop u ( function-Prop _ empty-Prop) ( λ where ( x , refl) → apply-universal-property-trunc-Prop v ( function-Prop _ empty-Prop) ( λ where ( y , refl) r → is-empty-eq-coproduct-inl-inr x y ( is-injective-is-equiv ( is-equiv-map-equiv e) ( ( inv (H (inl x))) ∙ ( ap unit-trunc-Set r) ∙ ( H (inr y))))))) abstract is-surjective-map-is-coproduct-codomain : is-surjective map-is-coproduct-codomain is-surjective-map-is-coproduct-codomain b = apply-universal-property-trunc-Prop ( apply-effectiveness-unit-trunc-Set ( inv (is-section-map-inv-equiv e (unit-trunc-Set b)) ∙ inv (H a))) ( trunc-Prop (fiber map-is-coproduct-codomain b)) ( λ p → unit-trunc-Prop ( ( map-coproduct ( map-unit-im (f ∘ inl)) ( map-unit-im (f ∘ inr)) ( a)) , ( triangle-is-coproduct-codomain a ∙ inv p))) where a : X1 + X2 a = map-inv-equiv e (unit-trunc-Set b) is-coproduct-codomain : (im (f ∘ inl) + im (f ∘ inr)) ≃ A pr1 is-coproduct-codomain = map-is-coproduct-codomain pr2 is-coproduct-codomain = is-equiv-is-emb-is-surjective is-surjective-map-is-coproduct-codomain is-emb-map-is-coproduct-codomain
Recent changes
- 2025-08-14. Fredrik Bakke. Dedekind finiteness of various notions of finite type (#1422).
- 2024-08-22. Fredrik Bakke. Cleanup of finite types (#1166).
- 2024-04-11. Fredrik Bakke and Egbert Rijke. Propositional operations (#1008).
- 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).