The category of sets
Content created by Fredrik Bakke, Egbert Rijke, Julian KG, fernabnor and louismntnu.
Created on 2023-05-06.
Last modified on 2024-03-11.
module foundation.category-of-sets where
Imports
open import category-theory.categories open import category-theory.isomorphisms-in-large-precategories open import category-theory.large-categories open import category-theory.large-precategories open import category-theory.precategories open import foundation.dependent-pair-types open import foundation.fundamental-theorem-of-identity-types open import foundation.isomorphisms-of-sets open import foundation.sets open import foundation.strictly-involutive-identity-types open import foundation.universe-levels open import foundation-core.contractible-types open import foundation-core.function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.identity-types
Idea
The category of sets consists of sets and functions. There is a category of sets for each universe level, and there is a large category of sets.
Definitions
The large precategory of sets
Set-Large-Precategory : Large-Precategory lsuc (_⊔_) obj-Large-Precategory Set-Large-Precategory = Set hom-set-Large-Precategory Set-Large-Precategory = hom-set-Set comp-hom-Large-Precategory Set-Large-Precategory g f = g ∘ f id-hom-Large-Precategory Set-Large-Precategory = id involutive-eq-associative-comp-hom-Large-Precategory Set-Large-Precategory h g f = reflⁱ left-unit-law-comp-hom-Large-Precategory Set-Large-Precategory f = refl right-unit-law-comp-hom-Large-Precategory Set-Large-Precategory f = refl
The large category of sets
id-iso-Set : {l : Level} {X : obj-Large-Precategory Set-Large-Precategory l} → iso-Large-Precategory Set-Large-Precategory X X id-iso-Set {l} {X} = id-iso-Large-Precategory (Set-Large-Precategory) {l} {X} iso-eq-Set : {l : Level} (X Y : obj-Large-Precategory Set-Large-Precategory l) → X = Y → iso-Large-Precategory Set-Large-Precategory X Y iso-eq-Set = iso-eq-Large-Precategory Set-Large-Precategory is-large-category-Set-Large-Precategory : is-large-category-Large-Precategory Set-Large-Precategory is-large-category-Set-Large-Precategory {l} X = fundamental-theorem-id ( is-contr-equiv' ( Σ (Set l) (equiv-Set X)) ( equiv-tot (equiv-iso-equiv-Set X)) ( is-torsorial-equiv-Set X)) ( iso-eq-Set X) Set-Large-Category : Large-Category lsuc (_⊔_) large-precategory-Large-Category Set-Large-Category = Set-Large-Precategory is-large-category-Large-Category Set-Large-Category = is-large-category-Set-Large-Precategory
The precategory of small sets
Set-Precategory : (l : Level) → Precategory (lsuc l) l Set-Precategory = precategory-Large-Precategory Set-Large-Precategory
The category of small sets
The precategory of sets and functions in a given universe is a category.
Set-Category : (l : Level) → Category (lsuc l) l Set-Category = category-Large-Category Set-Large-Category is-category-Set-Precategory : (l : Level) → is-category-Precategory (Set-Precategory l) is-category-Set-Precategory l = is-category-Category (Set-Category l)
Comments
Since sets are equivalent to their set-truncations, the category of sets forms a full subprecategory of the homotopy precategory of types.
See also
External links
- Set at Lab
- Category of sets at Wikipedia
Recent changes
- 2024-03-11. Fredrik Bakke. Refactor category theory to use strictly involutive identity types (#1052).
- 2024-01-31. Fredrik Bakke and Egbert Rijke. Transport-split and preunivalent type families (#1013).
- 2023-11-27. Fredrik Bakke. Refactor categories to carry a bidirectional witness of associativity (#945).
- 2023-11-24. Egbert Rijke. Abelianization (#877).
- 2023-11-09. Fredrik Bakke. Typeset
nlab
as$n$Lab
(#911).