# Nonunital precategories

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-10-20.

module category-theory.nonunital-precategories where

Imports
open import category-theory.composition-operations-on-binary-families-of-sets
open import category-theory.set-magmoids

open import foundation.cartesian-product-types
open import foundation.dependent-pair-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 nonunital precategory is a precategory that may not have identity morphisms. In other words, it is an associative composition operation on binary families of sets. Such a structure may also be referred to as a semiprecategory.

Perhaps surprisingly, there is at most one way to equip nonunital precategories with identity morphisms, so precategories form a subtype of nonunital precategories.

## Definition

### The type of nonunital precategories

Nonunital-Precategory :
(l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
Nonunital-Precategory l1 l2 =
Σ ( UU l1)
( λ A →
Σ ( A → A → Set l2)
( associative-composition-operation-binary-family-Set))

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

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

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

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

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

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

comp-hom-Nonunital-Precategory :
{x y z : obj-Nonunital-Precategory} →
hom-Nonunital-Precategory y z →
hom-Nonunital-Precategory x y →
hom-Nonunital-Precategory x z
comp-hom-Nonunital-Precategory =
comp-hom-associative-composition-operation-binary-family-Set
( hom-set-Nonunital-Precategory)
( associative-composition-operation-Nonunital-Precategory)

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

associative-comp-hom-Nonunital-Precategory :
{x y z w : obj-Nonunital-Precategory}
(h : hom-Nonunital-Precategory z w)
(g : hom-Nonunital-Precategory y z)
(f : hom-Nonunital-Precategory x y) →
comp-hom-Nonunital-Precategory (comp-hom-Nonunital-Precategory h g) f ＝
comp-hom-Nonunital-Precategory h (comp-hom-Nonunital-Precategory g f)
associative-comp-hom-Nonunital-Precategory =
witness-associative-composition-operation-binary-family-Set
( hom-set-Nonunital-Precategory)
( associative-composition-operation-Nonunital-Precategory)

involutive-eq-associative-comp-hom-Nonunital-Precategory :
{x y z w : obj-Nonunital-Precategory}
(h : hom-Nonunital-Precategory z w)
(g : hom-Nonunital-Precategory y z)
(f : hom-Nonunital-Precategory x y) →
comp-hom-Nonunital-Precategory (comp-hom-Nonunital-Precategory h g) f ＝ⁱ
comp-hom-Nonunital-Precategory h (comp-hom-Nonunital-Precategory g f)
involutive-eq-associative-comp-hom-Nonunital-Precategory =
involutive-eq-associative-composition-operation-binary-family-Set
( hom-set-Nonunital-Precategory)
( associative-composition-operation-Nonunital-Precategory)


### The underlying set-magmoid of a nonunital precategory

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

set-magmoid-Nonunital-Precategory : Set-Magmoid l1 l2
pr1 set-magmoid-Nonunital-Precategory = obj-Nonunital-Precategory C
pr1 (pr2 set-magmoid-Nonunital-Precategory) = hom-set-Nonunital-Precategory C
pr2 (pr2 set-magmoid-Nonunital-Precategory) = comp-hom-Nonunital-Precategory C


### The total hom-type of a nonunital precategory

total-hom-Nonunital-Precategory :
{l1 l2 : Level} (C : Nonunital-Precategory l1 l2) → UU (l1 ⊔ l2)
total-hom-Nonunital-Precategory C =
Σ ( obj-Nonunital-Precategory C)
( λ x → Σ (obj-Nonunital-Precategory C) (hom-Nonunital-Precategory C x))

obj-total-hom-Nonunital-Precategory :
{l1 l2 : Level} (C : Nonunital-Precategory l1 l2) →
total-hom-Nonunital-Precategory C →
obj-Nonunital-Precategory C × obj-Nonunital-Precategory C
pr1 (obj-total-hom-Nonunital-Precategory C (x , y , f)) = x
pr2 (obj-total-hom-Nonunital-Precategory C (x , y , f)) = y


### Pre- and postcomposition by a morphism

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

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

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


### The predicate on nonunital precategories of being unital

Proof: To show that unitality is a proposition, suppose e e' : (x : A) → hom-set x x are both right and left units with regard to composition. It is enough to show that e ＝ e' since the right and left unit laws are propositions (because all hom-types are sets). By function extensionality, it is enough to show that e x ＝ e' x for all x : A. But by the unit laws we have the following chain of equalities: e x ＝ (e' x) ∘ (e x) ＝ e' x.

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

is-unital-Nonunital-Precategory : UU (l1 ⊔ l2)
is-unital-Nonunital-Precategory =
is-unital-composition-operation-binary-family-Set
( hom-set-Nonunital-Precategory C)
( comp-hom-Nonunital-Precategory C)

is-prop-is-unital-Nonunital-Precategory :
is-prop
( is-unital-composition-operation-binary-family-Set
( hom-set-Nonunital-Precategory C)
( comp-hom-Nonunital-Precategory C))
is-prop-is-unital-Nonunital-Precategory =
is-prop-is-unital-composition-operation-binary-family-Set
( hom-set-Nonunital-Precategory C)
( comp-hom-Nonunital-Precategory C)

is-unital-prop-Nonunital-Precategory : Prop (l1 ⊔ l2)
is-unital-prop-Nonunital-Precategory =
is-unital-prop-composition-operation-binary-family-Set
( hom-set-Nonunital-Precategory C)
( comp-hom-Nonunital-Precategory C)


## Properties

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

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

is-trunc-total-hom-is-trunc-obj-Nonunital-Precategory :
is-trunc (succ-𝕋 (succ-𝕋 k)) (obj-Nonunital-Precategory C) →
is-trunc (succ-𝕋 (succ-𝕋 k)) (total-hom-Nonunital-Precategory C)
is-trunc-total-hom-is-trunc-obj-Nonunital-Precategory =
is-trunc-total-hom-is-trunc-obj-Set-Magmoid
( set-magmoid-Nonunital-Precategory C)

total-hom-truncated-type-is-trunc-obj-Nonunital-Precategory :
is-trunc (succ-𝕋 (succ-𝕋 k)) (obj-Nonunital-Precategory C) →
Truncated-Type (l1 ⊔ l2) (succ-𝕋 (succ-𝕋 k))
total-hom-truncated-type-is-trunc-obj-Nonunital-Precategory =
total-hom-truncated-type-is-trunc-obj-Set-Magmoid
( set-magmoid-Nonunital-Precategory C)


  pr1 : (Σ (a : A) Σ (f : hom a a) (is-neutral f)) → A