{-# OPTIONS --cubical --safe #-}
module Algebra where

open import Prelude

module _ {โ„“} (๐‘† : Type โ„“) where
  record Magma : Type โ„“ where
    infixl 6 _โˆ™_
    field
      _โˆ™_    : ๐‘† โ†’ ๐‘† โ†’ ๐‘†

    infix 4 _โŠ†_
    _โŠ†_ : ๐‘† โ†’ ๐‘† โ†’ Type _
    x โŠ† y = โˆƒ z ร— y โ‰ก x โˆ™ z

  record UnitalMagma : Type โ„“ where
    infixl 6 _โˆ™_
    field
      _โˆ™_    : ๐‘† โ†’ ๐‘† โ†’ ๐‘†
      ฮต      : ๐‘†

    magma : Magma
    magma = record { _โˆ™_ = _โˆ™_ }

    open Magma magma using (_โŠ†_) public

  record  Semigroup : Type โ„“ where
    infixl 6 _โˆ™_
    field
      _โˆ™_    : ๐‘† โ†’ ๐‘† โ†’ ๐‘†
      assoc  : โˆ€ x y z โ†’ (x โˆ™ y) โˆ™ z โ‰ก x โˆ™ (y โˆ™ z)

    magma : Magma
    magma = record { _โˆ™_ = _โˆ™_ }

    open Magma magma using (_โŠ†_) public

    โŠ†-trans : โˆ€ x y z โ†’ x โŠ† y โ†’ y โŠ† z โ†’ x โŠ† z
    โŠ†-trans x y z xโŠ†y yโŠ†z .fst = xโŠ†y .fst โˆ™ yโŠ†z .fst
    โŠ†-trans x y z xโŠ†y yโŠ†z .snd = yโŠ†z .snd โจพ cong (_โˆ™ _) (xโŠ†y .snd) โจพ assoc x _ _

  record  Monoid : Type โ„“ where
    infixl 6 _โˆ™_
    field
      _โˆ™_    : ๐‘† โ†’ ๐‘† โ†’ ๐‘†
      ฮต      : ๐‘†
      assoc  : โˆ€ x y z โ†’ (x โˆ™ y) โˆ™ z โ‰ก x โˆ™ (y โˆ™ z)
      ฮตโˆ™     : โˆ€ x โ†’ ฮต โˆ™ x โ‰ก x
      โˆ™ฮต     : โˆ€ x โ†’ x โˆ™ ฮต โ‰ก x

    semigroup : Semigroup
    semigroup = record
      { _โˆ™_ = _โˆ™_; assoc = assoc }

    unitalMagma : UnitalMagma
    unitalMagma = record
      { _โˆ™_ = _โˆ™_; ฮต = ฮต }

    open Semigroup semigroup using (_โŠ†_; โŠ†-trans) public

    -- โŠ†-refl : โˆ€ x โ†’ x โŠ† x
    -- โŠ†-refl x .fst = ฮต
    -- โŠ†-refl x .snd = sym (โˆ™ฮต _)

  record CommutativeMonoid : Type โ„“ where
    field
      monoid : Monoid
    open Monoid monoid public
    field
      comm : โˆ€ x y โ†’ x โˆ™ y โ‰ก y โˆ™ x

  record Semilattice : Type โ„“ where
    field
      commutativeMonoid : CommutativeMonoid
    open CommutativeMonoid commutativeMonoid public
    field
      idem : โˆ€ x โ†’ x โˆ™ x โ‰ก x