# Unital binary operations

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke, Victor Blanchi and favonia.

Created on 2022-06-10.

module foundation.unital-binary-operations where

Imports
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.whiskering-homotopies


## Idea

A binary operation of type A → A → A is unital if there is a unit of type A that satisfies both the left and right unit laws. Furthermore, a binary operation is coherently unital if the proofs of the left and right unit laws agree on the case where both arguments of the operation are the unit.

## Definitions

### Unit laws

module _
{l : Level} {A : UU l} (μ : A → A → A) (e : A)
where

left-unit-law : UU l
left-unit-law = (x : A) → μ e x ＝ x

right-unit-law : UU l
right-unit-law = (x : A) → μ x e ＝ x

coh-unit-laws : left-unit-law → right-unit-law → UU l
coh-unit-laws α β = (α e ＝ β e)

unit-laws : UU l
unit-laws = left-unit-law × right-unit-law

coherent-unit-laws : UU l
coherent-unit-laws =
Σ left-unit-law (λ α → Σ right-unit-law (coh-unit-laws α))


### Unital binary operations

is-unital : {l : Level} {A : UU l} (μ : A → A → A) → UU l
is-unital {A = A} μ = Σ A (unit-laws μ)


### Coherently unital binary operations

is-coherently-unital : {l : Level} {A : UU l} (μ : A → A → A) → UU l
is-coherently-unital {A = A} μ = Σ A (coherent-unit-laws μ)


## Properties

### The unit laws for an operation μ with unit e can be upgraded to coherent unit laws

module _
{l : Level} {A : UU l} (μ : A → A → A) {e : A}
where

coherent-unit-laws-unit-laws : unit-laws μ e → coherent-unit-laws μ e
pr1 (coherent-unit-laws-unit-laws (pair H K)) = H
pr1 (pr2 (coherent-unit-laws-unit-laws (pair H K))) x =
( inv (ap (μ x) (K e))) ∙ (( ap (μ x) (H e)) ∙ (K x))
pr2 (pr2 (coherent-unit-laws-unit-laws (pair H K))) =
left-transpose-eq-concat
( ap (μ e) (K e))
( H e)
( (ap (μ e) (H e)) ∙ (K e))
( ( inv-nat-htpy-id (H) (K e)) ∙
( ap (concat' (μ e (μ e e)) (K e)) (coh-htpy-id (H) e)))

module _
{l : Level} {A : UU l} {μ : A → A → A}
where

is-coherently-unital-is-unital : is-unital μ → is-coherently-unital μ
pr1 (is-coherently-unital-is-unital (pair e H)) = e
pr2 (is-coherently-unital-is-unital (pair e H)) =
coherent-unit-laws-unit-laws μ H