The category of sets

module foundation.category-of-sets where

open import category-theory.large-precategories

open import foundation.sets

open import foundation-core.functions
open import foundation-core.identity-types
open import foundation-core.universe-levels

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 category of sets

Set-Large-Precategory : Large-Precategory lsuc (λ l1 l2 → l1 ⊔ l2)
obj-Large-Precategory Set-Large-Precategory = Set
hom-Large-Precategory Set-Large-Precategory = hom-Set
comp-hom-Large-Precategory Set-Large-Precategory g f = g ∘ f
id-hom-Large-Precategory Set-Large-Precategory = id
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