Home
module category-theory.category-of-sets where
Imports
open import foundations.universe
open import foundations.identity-type
open import foundations.sigma-type
open import foundations.set
open import foundations.function
open import foundations.h-level-pi
open import foundations.function-extensionality
open import category-theory.category
module _ ℓ (e : FunExtLevel ℓ ℓ) where
Sets : Category (lsuc ℓ) ℓ
Sets = record
{ 𝒞 = record
{ Ob = hSet ℓ
; Hom = λ A B → fst A → fst B
; id = λ A → idFunction (fst A)
; _∘_ = _∘_
}
; is-category = record
{ identˡ = λ _ → refl
; identʳ = λ _ → refl
; ident² = λ _ → refl
; assoc = refl
; sym-assoc = refl
; is-set-hom = λ {B = B} → isSet→ e λ _ → snd B
}
}