集合の圏

module category-theory.category-of-sets where

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
      }
    }