Investigations on graph-theoretical constructions in Homotopy type theory

{-# OPTIONS --without-K --exact-split #-}

module foundations.MonoidType where
  open import foundations.TransportLemmas
  open import foundations.EquivalenceType
  open import foundations.HomotopyType
  open import foundations.FunExtAxiom
  open import foundations.HLevelTypes

Monoids

A monoid is a algebraic structure on a set with a distinguished object, called the unit, and an associative binary operation, the multiplication. The multiplication must obey certain properties described below.

  record
    Monoid {ℓ : Level}
      : Type (lsuc ℓ)
      where
    constructor monoid
    field
      M   : Type ℓ       -- The carrier
      e   : M            -- Unit element (at least one element, this one)
      _⊕_ : M → M → M    -- Operation

      M-is-set : isSet M   -- the carrier is a set

      -- axioms:
      l-unit : (x : M) → (e ⊕ x) ≡ x
      r-unit : (x : M) → (x ⊕ e) ≡ x
      assoc  : (x y z : M) → (x ⊕ (y ⊕ z)) ≡ ((x ⊕ y) ⊕ z)

Latest changes

(2022-12-28)(57c278b4) Last updated: 2021-09-16 15:00:00 by jonathan.cubides
(2022-07-06)(d3a4a8cf) minors by jonathan.cubides
(2022-01-26)(4aef326b) [ reports ] added some revisions by jonathan.cubides
(2021-12-20)(049db6a8) Added code of cubical experiments. by jonathan.cubides
(2021-12-20)(961730c9) [ html ] regular update by jonathan.cubides
(2021-12-20)(e0ef9faa) Fixed compilation and format, remove hidden parts by jonathan.cubides
(2021-12-20)(5120e5d1) Added cubical experiment to the master by jonathan.cubides
(2021-12-17)(828fdd0a) More revisions added for CPP by jonathan.cubides
(2021-12-15)(0d6a99d8) Fixed some broken links and descriptions by jonathan.cubides
(2021-12-15)(662a1f2d) [ .gitignore ] add by jonathan.cubides
(2021-12-15)(0630ce66) Minor fixes by jonathan.cubides
(2021-12-13)(04f10eba) Fixed a lot of details by jonathan.cubides
(2021-12-10)(24195c9f) [ .gitignore ] ignore .zip and arxiv related files by jonathan.cubides
(2021-12-09)(538d2859) minor fixes before dinner by jonathan.cubides
(2021-12-09)(36a1a69f) [ planar.pdf ] w.i.p revisions to share on arxiv first by jonathan.cubides