Home

具体圏

module category-theory.concrete-category where
Imports 
open import foundations.universe
open import foundations.proposition
open import foundations.sigma-type
open import category-theory.category
open import category-theory.displayed-category

具体圏はdisplayed categoryを用いて定義する。こうすると、忠実関手を使った定義と比べて、具体関手の定義において対象間の「等価性」に言及せずに済む。

isConcreteCategory : ∀ {o h} {𝒞 : Category o h}
  → ∀ {o′ h′} (𝒟 : DisplayedCategory 𝒞 o′ h′)
  → Type (o ⊔ h ⊔ o′ ⊔ h′)
isConcreteCategory {𝒞 = 𝒞} 𝒟 =
  ∀ {A B} {f : 𝒞.Hom A B} {X Y} → isProp (Hom f X Y)
  where
    open DisplayedCategory 𝒟
    module 𝒞 = Category 𝒞

ConcreteCategory : ∀ {o h} (𝒞 : Category o h) o′ h′
  → Type (o ⊔ h ⊔ lsuc o′ ⊔ lsuc h′)
ConcreteCategory 𝒞 o′ h′ =
  Σ (DisplayedCategory 𝒞 o′ h′) isConcreteCategory