Home

Strict category

module category-theory.strict-category where
Imports 
open import foundations.universe
open import foundations.set
open import foundations.sigma-type
open import category-theory.category

対象の型が集合であるような圏をstrict categoryと呼ぶ。

private variable o h : Level

isStrictCategory : Category o h → Type o
isStrictCategory 𝒞 = isSet Ob
  where open Category 𝒞

StrictCategory : ∀ o h → Type (lsuc (o ⊔ h))
StrictCategory o h = Σ (Category o h) isStrictCategory