category-theory.composition-operations-on-binary-families-of-sets

# Composition operations on binary families of sets

```agda
module category-theory.composition-operations-on-binary-families-of-sets where
```

<details><summary>Imports</summary>

```agda
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.identity-types
open import foundation.iterated-dependent-product-types
open import foundation.propositions
open import foundation.sets
open import foundation.strictly-involutive-identity-types
open import foundation.subtypes
open import foundation.universe-levels
```

</details>

## Idea

Given a type `A`, a
{{#concept "composition operation" Disambiguation="on binary families of sets" Agda=composition-operation-binary-family-Set}}
on a binary family of [sets](foundation-core.sets.md) `hom : A → A → Set` is a
map

```text
  _∘_ : hom y z → hom x y → hom x z
```

for every triple of elements `x y z : A`.

For such operations, we can consider
[properties](foundation-core.propositions.md) such as _associativity_ and
_unitality_.

## Definitions

### Composition operations on binary families of sets

```agda
module _
  {l1 l2 : Level} {A : UU l1} (hom-set : A → A → Set l2)
  where

  composition-operation-binary-family-Set : UU (l1 ⊔ l2)
  composition-operation-binary-family-Set =
    {x y z : A} →
    type-Set (hom-set y z) → type-Set (hom-set x y) → type-Set (hom-set x z)
```

### Associative composition operations on binary families of sets

A composition operation

```text
  _∘_ : hom y z → hom x y → hom x z
```

on a binary family of sets of morphisms is called
{{#concept "associative" Disambiguation="composition operation on a binary family of sets" Agda=is-associative-composition-operation-binary-family-Set}}
if, for every triple of composable morphisms we have

```text
  (h ∘ g) ∘ f ＝ h ∘ (g ∘ f).
```

We give a slightly nonstandard definition of associativity using the
[strictly involutive identity types](foundation.strictly-involutive-identity-types.md)
rather than the standard [identity types](foundation-core.identity-types.md).
This is because, while the strictly involutive identity types are always
[equivalent](foundation-core.equivalences.md) to the standard ones, they satisfy
the strict computation rule `inv (inv p) ≐ p` which is practical in defining the
[opposite category](category-theory.opposite-categories.md), as this also makes
the opposite construction strictly involutive: `(𝒞ᵒᵖ)ᵒᵖ ≐ 𝒞`.

```agda
module _
  {l1 l2 : Level} {A : UU l1} (hom-set : A → A → Set l2)
  where

  is-associative-composition-operation-binary-family-Set :
    composition-operation-binary-family-Set hom-set → UU (l1 ⊔ l2)
  is-associative-composition-operation-binary-family-Set comp-hom =
    {x y z w : A}
    (h : type-Set (hom-set z w))
    (g : type-Set (hom-set y z))
    (f : type-Set (hom-set x y)) →
    ( comp-hom (comp-hom h g) f ＝ⁱ comp-hom h (comp-hom g f))

  associative-composition-operation-binary-family-Set : UU (l1 ⊔ l2)
  associative-composition-operation-binary-family-Set =
    Σ ( composition-operation-binary-family-Set hom-set)
      ( is-associative-composition-operation-binary-family-Set)

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

  comp-hom-associative-composition-operation-binary-family-Set :
    composition-operation-binary-family-Set hom-set
  comp-hom-associative-composition-operation-binary-family-Set = pr1 H

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

  witness-associative-composition-operation-binary-family-Set :
    {x y z w : A}
    (h : type-Set (hom-set z w))
    (g : type-Set (hom-set y z))
    (f : type-Set (hom-set x y)) →
    ( comp-hom-associative-composition-operation-binary-family-Set
      ( comp-hom-associative-composition-operation-binary-family-Set h g) (f)) ＝
    ( comp-hom-associative-composition-operation-binary-family-Set
      ( h) (comp-hom-associative-composition-operation-binary-family-Set g f))
  witness-associative-composition-operation-binary-family-Set h g f =
    eq-involutive-eq
      ( involutive-eq-associative-composition-operation-binary-family-Set h g f)

  inv-witness-associative-composition-operation-binary-family-Set :
    {x y z w : A}
    (h : type-Set (hom-set z w))
    (g : type-Set (hom-set y z))
    (f : type-Set (hom-set x y)) →
    ( comp-hom-associative-composition-operation-binary-family-Set
      ( h) (comp-hom-associative-composition-operation-binary-family-Set g f)) ＝
    ( comp-hom-associative-composition-operation-binary-family-Set
      ( comp-hom-associative-composition-operation-binary-family-Set h g) (f))
  inv-witness-associative-composition-operation-binary-family-Set h g f =
    eq-involutive-eq
      ( invⁱ
        ( involutive-eq-associative-composition-operation-binary-family-Set
          ( h)
          ( g)
          ( f)))
```

### Unital composition operations on binary families of sets

A composition operation

```text
  _∘_ : hom y z → hom x y → hom x z
```

on a binary family of sets of morphisms is called
{{#concept "unital" Disambiguation="composition operation on a binary family of sets" Agda=is-unital-composition-operation-binary-family-Set}}
if there is a morphism `id_x : hom x x` for every element `x : A` such that

```text
  id_y ∘ f ＝ f   and f ∘ id_x = f.
```

As will be demonstrated momentarily, every composition operation on a binary
family of sets is unital in [at most one](foundation.subterminal-types.md) way.

```agda
module _
  {l1 l2 : Level} {A : UU l1} (hom-set : A → A → Set l2)
  where

  is-unital-composition-operation-binary-family-Set :
    composition-operation-binary-family-Set hom-set → UU (l1 ⊔ l2)
  is-unital-composition-operation-binary-family-Set comp-hom =
    Σ ( (x : A) → type-Set (hom-set x x))
      ( λ e →
        ( {x y : A} (f : type-Set (hom-set x y)) → comp-hom (e y) f ＝ f) ×
        ( {x y : A} (f : type-Set (hom-set x y)) → comp-hom f (e x) ＝ f))
```

## Properties

### Being associative is a property of composition operations on binary families of sets

```agda
module _
  {l1 l2 : Level} {A : UU l1}
  (hom-set : A → A → Set l2)
  (comp-hom : composition-operation-binary-family-Set hom-set)
  where
  is-prop-is-associative-composition-operation-binary-family-Set :
    is-prop
      ( is-associative-composition-operation-binary-family-Set hom-set comp-hom)
  is-prop-is-associative-composition-operation-binary-family-Set =
    is-prop-iterated-implicit-Π 4
      ( λ x y z w →
        is-prop-iterated-Π 3
          ( λ h g f →
            is-prop-equiv
              ( equiv-eq-involutive-eq)
              ( is-set-type-Set
                ( hom-set x w)
                ( comp-hom (comp-hom h g) f)
                ( comp-hom h (comp-hom g f)))))

  is-associative-prop-composition-operation-binary-family-Set : Prop (l1 ⊔ l2)
  pr1 is-associative-prop-composition-operation-binary-family-Set =
    is-associative-composition-operation-binary-family-Set hom-set comp-hom
  pr2 is-associative-prop-composition-operation-binary-family-Set =
    is-prop-is-associative-composition-operation-binary-family-Set
```

### Being unital is a property of composition operations on binary families of sets

**Proof:** 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} {A : UU l1}
  (hom-set : A → A → Set l2)
  (comp-hom : composition-operation-binary-family-Set hom-set)
  where

  abstract
    all-elements-equal-is-unital-composition-operation-binary-family-Set :
      all-elements-equal
        ( is-unital-composition-operation-binary-family-Set hom-set comp-hom)
    all-elements-equal-is-unital-composition-operation-binary-family-Set
      ( e , left-unit-law-e , right-unit-law-e)
      ( e' , left-unit-law-e' , right-unit-law-e') =
      eq-type-subtype
        ( λ x →
          product-Prop
            ( implicit-Π-Prop A
              ( λ a →
                implicit-Π-Prop A
                ( λ b →
                  Π-Prop
                    ( type-Set (hom-set a b))
                    ( λ f' → Id-Prop (hom-set a b) (comp-hom (x b) f') f'))))
            ( implicit-Π-Prop A
              ( λ a →
                implicit-Π-Prop A
                ( λ b →
                  Π-Prop
                    ( type-Set (hom-set a b))
                    ( λ f' → Id-Prop (hom-set a b) (comp-hom f' (x a)) f')))))
        ( eq-htpy
          ( λ x → inv (left-unit-law-e' (e x)) ∙ right-unit-law-e (e' x)))

  abstract
    is-prop-is-unital-composition-operation-binary-family-Set :
      is-prop
        ( is-unital-composition-operation-binary-family-Set hom-set comp-hom)
    is-prop-is-unital-composition-operation-binary-family-Set =
      is-prop-all-elements-equal
        all-elements-equal-is-unital-composition-operation-binary-family-Set

  is-unital-prop-composition-operation-binary-family-Set : Prop (l1 ⊔ l2)
  pr1 is-unital-prop-composition-operation-binary-family-Set =
    is-unital-composition-operation-binary-family-Set hom-set comp-hom
  pr2 is-unital-prop-composition-operation-binary-family-Set =
    is-prop-is-unital-composition-operation-binary-family-Set
```

## See also

- [Set-magmoids](category-theory.set-magmoids.md) capture the structure of
  composition operations on binary families of sets.
- [Precategories](category-theory.precategories.md) are the structure of an
  associative and unital composition operation on a binary families of sets.
- [Nonunital precategories](category-theory.nonunital-precategories.md) are the
  structure of an associative composition operation on a binary families of
  sets.