module category-theory.category-of-strict-categories where
open import foundations.universe open import foundations.set open import foundations.sigma-type open import foundations.identity-type open import foundations.function open import foundations.functions-are-functors open import foundations.groupoid-laws open import foundations.function-extensionality open import foundations.h-level-sigma open import foundations.h-level-pi open import foundations.h-level-closed-under-retract open import foundations.h-level-closed-under-retract-of-identity open import category-theory.category open import category-theory.functor open import category-theory.functor-identity open import category-theory.composition-of-functors open import category-theory.strict-category
(小さい)圏全体は圏にはならないが、(小さい) strict category全体は圏を成す。
StrictFunctor : ∀ {o h} (𝒞 𝒟 : StrictCategory o h)
→ Type (o ⊔ h)
StrictFunctor (𝒞 , x) (𝒟 , y) = Functor 𝒞 𝒟
module _ (e : FunExtAll) where
isSetStrictFunctor : ∀ {o h} (𝒞 𝒟 : StrictCategory o h)
→ isSet (StrictFunctor 𝒞 𝒟)
isSetStrictFunctor 𝒞 𝒟 =
isSetRetractId
(isSetRetract
(isSetΣ (isSet→ e λ _ → 𝒟 .snd) λ _ → isSetImplicitΠ e λ _ → isSetImplicitΠ e (λ _ → isSet→ e λ _ → Category.is-set-hom (𝒟 .fst)))
(functorDataToΣ _ _ , hasRetractionFunctorDataToΣ _ _))
Functor.F
λ { {x = F} {y = G} → hasRetractionFromFunctorId e (𝒞 .fst) (𝒟 .fst) F G }
SCats : ∀ (o h : Level) → Category (lsuc (o ⊔ h)) (o ⊔ h)
SCats o h = record
{ 𝒞 = record
{ Ob = StrictCategory o h
; Hom = StrictFunctor
; id = λ A → idFunctor (A .fst)
; _∘_ = _∘F_
}
; is-category = record
{ identˡ = lunit-∘F e
; identʳ = runit-∘F e
; ident² = λ A → lunit-∘F e (idFunctor (A .fst))
; assoc = λ { {f = F} {g = G} {h = H} → assoc-∘F e F G H }
; sym-assoc = λ { {f = F} {g = G} {h = H} → sym (assoc-∘F e F G H) }
; is-set-hom = λ { {A = 𝒞} {B = 𝒟} → isSetStrictFunctor 𝒞 𝒟}
}
}