Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Elisabeth Stenholm, Julian KG, fernabnor and louismntnu.

Created on 2022-03-11.
Last modified on 2024-02-06.

module category-theory.precategories where
open import category-theory.composition-operations-on-binary-families-of-sets
open import category-theory.nonunital-precategories
open import category-theory.set-magmoids

open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.truncated-types
open import foundation.truncation-levels
open import foundation.universe-levels


A precategory in Homotopy Type Theory consists of:

  • a type A of objects,
  • for each pair of objects x y : A, a set of morphisms hom x y : Set, together with a composition operation _∘_ : hom y z → hom x y → hom x z such that:
  • (h ∘ g) ∘ f = h ∘ (g ∘ f) for any morphisms h : hom z w, g : hom y z and f : hom x y,
  • for each object x : A there is a morphism id_x : hom x x such that id_x ∘ f = f and g ∘ id_x = g for any morphisms f : hom x y and g : hom z x.

The reason this is called a precategory and not a category in Homotopy Type Theory is that we want to reserve that name for precategories where the identities between the objects are exactly the isomorphisms.


The predicate on composition operations on binary families of sets of being a precategory

module _
  {l1 l2 : Level} {A : UU l1}
  (hom-set : A  A  Set l2)
  (comp-hom : composition-operation-binary-family-Set hom-set)

  is-precategory-prop-composition-operation-binary-family-Set : Prop (l1  l2)
  is-precategory-prop-composition-operation-binary-family-Set =
      ( is-unital-prop-composition-operation-binary-family-Set hom-set comp-hom)
      ( is-associative-prop-composition-operation-binary-family-Set
        ( hom-set)
        ( comp-hom))

  is-precategory-composition-operation-binary-family-Set : UU (l1  l2)
  is-precategory-composition-operation-binary-family-Set =
    type-Prop is-precategory-prop-composition-operation-binary-family-Set

  is-prop-is-precategory-composition-operation-binary-family-Set :
    is-prop is-precategory-composition-operation-binary-family-Set
  is-prop-is-precategory-composition-operation-binary-family-Set =

The type of precategories

Precategory :
  (l1 l2 : Level)  UU (lsuc l1  lsuc l2)
Precategory l1 l2 =
  Σ ( UU l1)
    ( λ A 
      Σ ( A  A  Set l2)
        ( λ hom-set 
          Σ ( associative-composition-operation-binary-family-Set hom-set)
            ( λ (comp-hom , assoc-comp) 
                ( hom-set)
                ( comp-hom))))

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

  obj-Precategory : UU l1
  obj-Precategory = pr1 C

  hom-set-Precategory : (x y : obj-Precategory)  Set l2
  hom-set-Precategory = pr1 (pr2 C)

  hom-Precategory : (x y : obj-Precategory)  UU l2
  hom-Precategory x y = type-Set (hom-set-Precategory x y)

  is-set-hom-Precategory :
    (x y : obj-Precategory)  is-set (hom-Precategory x y)
  is-set-hom-Precategory x y = is-set-type-Set (hom-set-Precategory x y)

  associative-composition-operation-Precategory :
    associative-composition-operation-binary-family-Set hom-set-Precategory
  associative-composition-operation-Precategory = pr1 (pr2 (pr2 C))

  comp-hom-Precategory :
    {x y z : obj-Precategory} 
    hom-Precategory y z 
    hom-Precategory x y 
    hom-Precategory x z
  comp-hom-Precategory =
      ( hom-set-Precategory)
      ( associative-composition-operation-Precategory)

  comp-hom-Precategory' :
    {x y z : obj-Precategory} 
    hom-Precategory x y 
    hom-Precategory y z 
    hom-Precategory x z
  comp-hom-Precategory' f g = comp-hom-Precategory g f

  associative-comp-hom-Precategory :
    {x y z w : obj-Precategory}
    (h : hom-Precategory z w)
    (g : hom-Precategory y z)
    (f : hom-Precategory x y) 
    ( comp-hom-Precategory (comp-hom-Precategory h g) f) 
    ( comp-hom-Precategory h (comp-hom-Precategory g f))
  associative-comp-hom-Precategory =
      ( hom-set-Precategory)
      ( associative-composition-operation-Precategory)

  inv-associative-comp-hom-Precategory :
    {x y z w : obj-Precategory}
    (h : hom-Precategory z w)
    (g : hom-Precategory y z)
    (f : hom-Precategory x y) 
    ( comp-hom-Precategory h (comp-hom-Precategory g f)) 
    ( comp-hom-Precategory (comp-hom-Precategory h g) f)
  inv-associative-comp-hom-Precategory =
      ( hom-set-Precategory)
      ( associative-composition-operation-Precategory)

  is-unital-composition-operation-Precategory :
      ( hom-set-Precategory)
      ( comp-hom-Precategory)
  is-unital-composition-operation-Precategory = pr2 (pr2 (pr2 C))

  id-hom-Precategory : {x : obj-Precategory}  hom-Precategory x x
  id-hom-Precategory {x} = pr1 is-unital-composition-operation-Precategory x

  left-unit-law-comp-hom-Precategory :
    {x y : obj-Precategory} (f : hom-Precategory x y) 
    comp-hom-Precategory id-hom-Precategory f  f
  left-unit-law-comp-hom-Precategory =
    pr1 (pr2 is-unital-composition-operation-Precategory)

  right-unit-law-comp-hom-Precategory :
    {x y : obj-Precategory} (f : hom-Precategory x y) 
    comp-hom-Precategory f id-hom-Precategory  f
  right-unit-law-comp-hom-Precategory =
    pr2 (pr2 is-unital-composition-operation-Precategory)

The underlying nonunital precategory of a precategory

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

  nonunital-precategory-Precategory : Nonunital-Precategory l1 l2
  pr1 nonunital-precategory-Precategory = obj-Precategory C
  pr1 (pr2 nonunital-precategory-Precategory) = hom-set-Precategory C
  pr2 (pr2 nonunital-precategory-Precategory) =
    associative-composition-operation-Precategory C

The underlying set-magmoid of a precategory

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

  set-magmoid-Precategory : Set-Magmoid l1 l2
  set-magmoid-Precategory =
    set-magmoid-Nonunital-Precategory (nonunital-precategory-Precategory C)

The total hom-type of a precategory

total-hom-Precategory :
  {l1 l2 : Level} (C : Precategory l1 l2)  UU (l1  l2)
total-hom-Precategory C =
  total-hom-Nonunital-Precategory (nonunital-precategory-Precategory C)

obj-total-hom-Precategory :
  {l1 l2 : Level} (C : Precategory l1 l2) 
  total-hom-Precategory C  obj-Precategory C × obj-Precategory C
obj-total-hom-Precategory C =
  obj-total-hom-Nonunital-Precategory (nonunital-precategory-Precategory C)

Equalities induce morphisms

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

  hom-eq-Precategory :
    (x y : obj-Precategory C)  x  y  hom-Precategory C x y
  hom-eq-Precategory x .x refl = id-hom-Precategory C

  hom-inv-eq-Precategory :
    (x y : obj-Precategory C)  x  y  hom-Precategory C y x
  hom-inv-eq-Precategory x y = hom-eq-Precategory y x  inv

Pre- and postcomposition by a morphism

module _
  {l1 l2 : Level} (C : Precategory l1 l2)
  {x y : obj-Precategory C}
  (f : hom-Precategory C x y)
  (z : obj-Precategory C)

  precomp-hom-Precategory : hom-Precategory C y z  hom-Precategory C x z
  precomp-hom-Precategory g = comp-hom-Precategory C g f

  postcomp-hom-Precategory : hom-Precategory C z x  hom-Precategory C z y
  postcomp-hom-Precategory = comp-hom-Precategory C f


If the objects of a precategory are k-truncated for nonnegative k, the total hom-type is k-truncated

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

  is-trunc-total-hom-is-trunc-obj-Precategory :
    is-trunc (succ-𝕋 (succ-𝕋 k)) (obj-Precategory C) 
    is-trunc (succ-𝕋 (succ-𝕋 k)) (total-hom-Precategory C)
  is-trunc-total-hom-is-trunc-obj-Precategory =
      ( nonunital-precategory-Precategory C)

  total-hom-truncated-type-is-trunc-obj-Precategory :
    is-trunc (succ-𝕋 (succ-𝕋 k)) (obj-Precategory C) 
    Truncated-Type (l1  l2) (succ-𝕋 (succ-𝕋 k))
  total-hom-truncated-type-is-trunc-obj-Precategory =
      ( nonunital-precategory-Precategory C)

See also

Recent changes