# Precategories

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

Created on 2022-03-11.

module category-theory.precategories where

Imports
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.strictly-involutive-identity-types
open import foundation.truncated-types
open import foundation.truncation-levels
open import foundation.universe-levels


## Idea

A precategory 𝒞 in Homotopy Type Theory is the structure of an associative and unital composition operation on a binary familiy of sets.

This means a precategory consists of:

• Objects. A type Ob 𝒞 of objects.
• Morphisms. For each pair of objects x y : Ob 𝒞, a set of morphisms hom 𝒞 x y : Set.
• Composition. For every triple of objects x y z : Ob 𝒞 there is a composition operation on morphisms
  _∘_ : hom 𝒞 y z → hom 𝒞 x y → hom 𝒞 x z.

• Associativity. For every triple of composable morphisms, we have
  (h ∘ g) ∘ f ＝ h ∘ (g ∘ f).

• Identity morphisms. For every object x : Ob 𝒞, there is a distinguished identity morphism id_x : hom 𝒞 x x.
• Unitality. The identity morphisms are two-sided units for the composition operation, meaning that for every f : hom 𝒞 x y we have
  id_y ∘ f ＝ f   and   f ∘ id_x ＝ f.


Note. The reason this is called a precategory and not a category in Homotopy Type Theory is that we reserve that name for precategories where the identity types of the type of objects are characterized by the isomorphism sets.

## Definitions

### 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)
where

is-precategory-prop-composition-operation-binary-family-Set : Prop (l1 ⊔ l2)
is-precategory-prop-composition-operation-binary-family-Set =
product-Prop
( 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 =
is-prop-type-Prop
is-precategory-prop-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) →
is-unital-composition-operation-binary-family-Set
( hom-set)
( comp-hom))))

make-Precategory :
{ l1 l2 : Level}
( obj : UU l1)
( hom-set : obj → obj → Set l2)
( _∘_ : composition-operation-binary-family-Set hom-set)
( id : (x : obj) → type-Set (hom-set x x))
( assoc-comp-hom :
{ x y z w : obj} →
( h : type-Set (hom-set z w))
( g : type-Set (hom-set y z))
( f : type-Set (hom-set x y)) →
( (h ∘ g) ∘ f ＝ h ∘ (g ∘ f)))
( left-unit-comp-hom :
{ x y : obj} (f : type-Set (hom-set x y)) → id y ∘ f ＝ f)
( right-unit-comp-hom :
{ x y : obj} (f : type-Set (hom-set x y)) → f ∘ id x ＝ f) →
Precategory l1 l2
make-Precategory
obj hom-set _∘_ id assoc-comp-hom left-unit-comp-hom right-unit-comp-hom =
( ( obj) ,
( hom-set) ,
( _∘_ , (λ h g f → involutive-eq-eq (assoc-comp-hom h g f))) ,
( id) ,
( left-unit-comp-hom) ,
( right-unit-comp-hom))

{-# INLINE make-Precategory #-}

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

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 =
comp-hom-associative-composition-operation-binary-family-Set
( 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

involutive-eq-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))
involutive-eq-associative-comp-hom-Precategory =
involutive-eq-associative-composition-operation-binary-family-Set
( hom-set-Precategory)
( associative-composition-operation-Precategory)

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 =
witness-associative-composition-operation-binary-family-Set
( hom-set-Precategory)
( associative-composition-operation-Precategory)

is-unital-composition-operation-Precategory :
is-unital-composition-operation-binary-family-Set
( 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)
where

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)
where

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)
where

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)
where

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


## Properties

### 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)
where

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 =
is-trunc-total-hom-is-trunc-obj-Nonunital-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 =
total-hom-truncated-type-is-trunc-obj-Nonunital-Precategory
( nonunital-precategory-Precategory C)