Strict categories

Content created by Fredrik Bakke.

Created on 2023-10-20.
Last modified on 2024-03-11.

module category-theory.strict-categories where

Imports

open import category-theory.categories
open import category-theory.composition-operations-on-binary-families-of-sets
open import category-theory.isomorphisms-in-precategories
open import category-theory.nonunital-precategories
open import category-theory.precategories
open import category-theory.preunivalent-categories

open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.universe-levels

Idea

A strict category^¶ is a precategory for which the type of objects form a set. Such categories are the set-theoretic analogue to (univalent) categories, and have the disadvantages that strict categorical constructions may generally fail to be invariant under equivalences, and that the (essentially surjective/fully-faithful)-factorization system on functors requires the axiom of choice.

Definitions

The predicate on precategories of being a strict category

module _
  {l1 l2 : Level} (C : Precategory l1 l2)
  where

  is-strict-category-prop-Precategory : Prop l1
  is-strict-category-prop-Precategory =
    is-set-Prop (obj-Precategory C)

  is-strict-category-Precategory : UU l1
  is-strict-category-Precategory =
    type-Prop is-strict-category-prop-Precategory

The predicate on preunivalent categories of being a strict category

module _
  {l1 l2 : Level} (C : Preunivalent-Category l1 l2)
  where

  is-strict-category-prop-Preunivalent-Category : Prop l1
  is-strict-category-prop-Preunivalent-Category =
    is-strict-category-prop-Precategory (precategory-Preunivalent-Category C)

  is-strict-category-Preunivalent-Category : UU l1
  is-strict-category-Preunivalent-Category =
    type-Prop is-strict-category-prop-Preunivalent-Category

The predicate on categories of being a strict category

We note that (univalent) categories that are strict form a very restricted class of strict categories where every isomorphism-set is a proposition. Such a category is called gaunt.

module _
  {l1 l2 : Level} (C : Category l1 l2)
  where

  is-strict-category-prop-Category : Prop l1
  is-strict-category-prop-Category =
    is-strict-category-prop-Precategory (precategory-Category C)

  is-strict-category-Category : UU l1
  is-strict-category-Category = type-Prop is-strict-category-prop-Category

The type of strict categories

Strict-Category : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
Strict-Category l1 l2 = Σ (Precategory l1 l2) is-strict-category-Precategory

module _
  {l1 l2 : Level} (C : Strict-Category l1 l2)
  where

  precategory-Strict-Category : Precategory l1 l2
  precategory-Strict-Category = pr1 C

  obj-Strict-Category : UU l1
  obj-Strict-Category = obj-Precategory precategory-Strict-Category

  is-set-obj-Strict-Category : is-set obj-Strict-Category
  is-set-obj-Strict-Category = pr2 C

  hom-set-Strict-Category : obj-Strict-Category → obj-Strict-Category → Set l2
  hom-set-Strict-Category = hom-set-Precategory precategory-Strict-Category

  hom-Strict-Category : obj-Strict-Category → obj-Strict-Category → UU l2
  hom-Strict-Category = hom-Precategory precategory-Strict-Category

  is-set-hom-Strict-Category :
    (x y : obj-Strict-Category) → is-set (hom-Strict-Category x y)
  is-set-hom-Strict-Category =
    is-set-hom-Precategory precategory-Strict-Category

  comp-hom-Strict-Category :
    {x y z : obj-Strict-Category} →
    hom-Strict-Category y z → hom-Strict-Category x y → hom-Strict-Category x z
  comp-hom-Strict-Category = comp-hom-Precategory precategory-Strict-Category

  associative-comp-hom-Strict-Category :
    {x y z w : obj-Strict-Category}
    (h : hom-Strict-Category z w)
    (g : hom-Strict-Category y z)
    (f : hom-Strict-Category x y) →
    comp-hom-Strict-Category (comp-hom-Strict-Category h g) f ＝
    comp-hom-Strict-Category h (comp-hom-Strict-Category g f)
  associative-comp-hom-Strict-Category =
    associative-comp-hom-Precategory precategory-Strict-Category

  associative-composition-operation-Strict-Category :
    associative-composition-operation-binary-family-Set hom-set-Strict-Category
  associative-composition-operation-Strict-Category =
    associative-composition-operation-Precategory precategory-Strict-Category

  id-hom-Strict-Category : {x : obj-Strict-Category} → hom-Strict-Category x x
  id-hom-Strict-Category = id-hom-Precategory precategory-Strict-Category

  left-unit-law-comp-hom-Strict-Category :
    {x y : obj-Strict-Category} (f : hom-Strict-Category x y) →
    comp-hom-Strict-Category id-hom-Strict-Category f ＝ f
  left-unit-law-comp-hom-Strict-Category =
    left-unit-law-comp-hom-Precategory precategory-Strict-Category

  right-unit-law-comp-hom-Strict-Category :
    {x y : obj-Strict-Category} (f : hom-Strict-Category x y) →
    comp-hom-Strict-Category f id-hom-Strict-Category ＝ f
  right-unit-law-comp-hom-Strict-Category =
    right-unit-law-comp-hom-Precategory precategory-Strict-Category

  is-unital-composition-operation-Strict-Category :
    is-unital-composition-operation-binary-family-Set
      hom-set-Strict-Category
      comp-hom-Strict-Category
  is-unital-composition-operation-Strict-Category =
    is-unital-composition-operation-Precategory precategory-Strict-Category

  is-strict-category-Strict-Category :
    is-strict-category-Precategory precategory-Strict-Category
  is-strict-category-Strict-Category = pr2 C

The underlying nonunital precategory of a strict category

module _
  {l1 l2 : Level} (C : Strict-Category l1 l2)
  where

  nonunital-precategory-Strict-Category : Nonunital-Precategory l1 l2
  nonunital-precategory-Strict-Category =
    nonunital-precategory-Precategory (precategory-Strict-Category C)

The underlying preunivalent category of a strict category

module _
  {l1 l2 : Level} (C : Strict-Category l1 l2)
  where

  abstract
    is-preunivalent-Strict-Category :
      is-preunivalent-Precategory (precategory-Strict-Category C)
    is-preunivalent-Strict-Category x y =
      is-emb-is-injective
        ( is-set-type-subtype
          ( is-iso-prop-Precategory (precategory-Strict-Category C))
          ( is-set-hom-Strict-Category C x y))
        ( λ _ → eq-is-prop (is-set-obj-Strict-Category C x y))

  preunivalent-category-Strict-Category : Preunivalent-Category l1 l2
  pr1 preunivalent-category-Strict-Category = precategory-Strict-Category C
  pr2 preunivalent-category-Strict-Category = is-preunivalent-Strict-Category

The total hom-set of a strict category

module _
  {l1 l2 : Level} (C : Strict-Category l1 l2)
  where

  total-hom-Strict-Category : UU (l1 ⊔ l2)
  total-hom-Strict-Category =
    total-hom-Precategory (precategory-Strict-Category C)

  obj-total-hom-Strict-Category :
    total-hom-Strict-Category → obj-Strict-Category C × obj-Strict-Category C
  obj-total-hom-Strict-Category =
    obj-total-hom-Precategory (precategory-Strict-Category C)

  is-set-total-hom-Strict-Category :
    is-set total-hom-Strict-Category
  is-set-total-hom-Strict-Category =
    is-trunc-total-hom-is-trunc-obj-Precategory
      ( precategory-Strict-Category C)
      ( is-set-obj-Strict-Category C)

  total-hom-set-Strict-Category : Set (l1 ⊔ l2)
  total-hom-set-Strict-Category =
    total-hom-truncated-type-is-trunc-obj-Precategory
      ( precategory-Strict-Category C)
      ( is-set-obj-Strict-Category C)

Equalities induce morphisms

module _
  {l1 l2 : Level} (C : Strict-Category l1 l2)
  where

  hom-eq-Strict-Category :
    (x y : obj-Strict-Category C) → x ＝ y → hom-Strict-Category C x y
  hom-eq-Strict-Category = hom-eq-Precategory (precategory-Strict-Category C)

  hom-inv-eq-Strict-Category :
    (x y : obj-Strict-Category C) → x ＝ y → hom-Strict-Category C y x
  hom-inv-eq-Strict-Category =
    hom-inv-eq-Precategory (precategory-Strict-Category C)

Pre- and postcomposition by a morphism

precomp-hom-Strict-Category :
  {l1 l2 : Level} (C : Strict-Category l1 l2) {x y : obj-Strict-Category C}
  (f : hom-Strict-Category C x y) (z : obj-Strict-Category C) →
  hom-Strict-Category C y z → hom-Strict-Category C x z
precomp-hom-Strict-Category C =
  precomp-hom-Precategory (precategory-Strict-Category C)

postcomp-hom-Strict-Category :
  {l1 l2 : Level} (C : Strict-Category l1 l2) {x y : obj-Strict-Category C}
  (f : hom-Strict-Category C x y) (z : obj-Strict-Category C) →
  hom-Strict-Category C z x → hom-Strict-Category C z y
postcomp-hom-Strict-Category C =
  postcomp-hom-Precategory (precategory-Strict-Category C)