# Composition operations on binary families of sets

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-10-20.

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

Imports
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


## Idea

Given a type A, a composition operation on a binary family of sets hom : A → A → Set is a map

  _∘_ : 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 such as associativity and unitality.

## Definitions

### Composition operations on binary families of sets

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

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


on a binary family of sets of morphisms is called associative if, for every triple of composable morphisms we have

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


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

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

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


on a binary family of sets of morphisms is called unital if there is a morphism id_x : hom x x for every element x : A such that

  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 way.

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

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.

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