# Nonunital precategories

```agda
module category-theory.nonunital-precategories where
```

<details><summary>Imports</summary>

```agda
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
```

</details>

## Idea

A {{#concept "nonunital precategory" Agda=Nonunital-Precategory}} is a
[precategory](category-theory.precategories.md) that may not have identity
morphisms. In other words, it is an associative
[composition operation on binary families of sets](category-theory.composition-operations-on-binary-families-of-sets.md).
Such a structure may also be referred to as a _semiprecategory_.

Perhaps surprisingly, there is [at most one](foundation.subterminal-types.md)
way to equip nonunital precategories with identity morphisms, so precategories
form a [subtype](foundation-core.subtypes.md) of nonunital precategories.

## Definition

### The type of nonunital precategories

```agda
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

```agda
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

```agda
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

```agda
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.`

```agda
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

```agda
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)
```

## Comments

As discussed in [Semicategories](https://ncatlab.org/nlab/show/semicategory) at
$n$Lab, it seems that a nonunital precategory should be the underlying nonunital
precategory of a [category](category-theory.categories.md) if and only if the
projection map

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

is an [equivalence](foundation-core.equivalences.md).

We can also define one notion of "isomorphism" as those morphisms that induce
equivalences of hom-[sets](foundation-core.sets.md) by pre- and postcomposition.

## External links

- [Semicategories](https://ncatlab.org/nlab/show/semicategory) at $n$Lab
- [Semigroupoid](https://en.wikipedia.org/wiki/Semigroupoid) at Wikipedia
- [semigroupoid](https://www.wikidata.org/wiki/Q4164581) at Wikidata