Unital binary operations
Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke, Victor Blanchi and favonia.
Created on 2022-06-10.
Last modified on 2023-09-12.
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
Recent changes
- 2023-09-12. Egbert Rijke. Factoring out whiskering (#756).
- 2023-09-10. Fredrik Bakke. Rename
inv-con
andcon-inv
toleft/right-transpose-eq-concat
(#730). - 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).
- 2023-06-08. Fredrik Bakke. Examples of modalities and various fixes (#639).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644).