    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Definition of algebraic structures we get from freely adding an
    -- identity element
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Algebra.Construct.Add.Identity where

    open import Algebra.Bundles using (Semigroup; Monoid)
    open import Algebra.Core using (Op₂)
    open import Algebra.Definitions
      using (Congruent₂; Associative; LeftIdentity; RightIdentity; Identity)
    open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
    open import Data.Product.Base using (_,_)
    open import Level using (Level; _⊔_)
    open import Relation.Binary.Construct.Add.Point.Equality renaming (_≈∙_ to lift≈)
    open import Relation.Binary.Core using (Rel)
    open import Relation.Binary.Definitions using (Reflexive)
    open import Relation.Binary.Structures using (IsEquivalence)
    open import Relation.Nullary.Construct.Add.Point using (Pointed; [_]; ∙)

    private
      variable
        a ℓ : Level
        A : Set a

    liftOp : Op₂ A → Op₂ (Pointed A)
    liftOp op [ p ] [ q ] = [ op p q ]
    liftOp _  [ p ] ∙     = [ p ]
    liftOp _  ∙     [ q ] = [ q ]
    liftOp _  ∙     ∙     = ∙

    module _ {_≈_ : Rel A ℓ} {op : Op₂ A} (refl-≈ : Reflexive _≈_) where
      private
        _≈∙_ = lift≈ _≈_
        op∙ = liftOp op

        lift-≈ : ∀ {x y : A} → x ≈ y → [ x ] ≈∙ [ y ]
        lift-≈ = [_]

      cong₂ : Congruent₂ _≈_ op → Congruent₂ _≈∙_ (op∙)
      cong₂ R-cong [ eq-l ] [ eq-r ] = lift-≈ (R-cong eq-l eq-r)
      cong₂ R-cong [ eq   ] ∙≈∙      = lift-≈ eq
      cong₂ R-cong ∙≈∙      [ eq   ] = lift-≈ eq
      cong₂ R-cong ∙≈∙      ∙≈∙      = ≈∙-refl _≈_ refl-≈

      assoc : Associative _≈_ op → Associative _≈∙_ (op∙)
      assoc assoc [ p ] [ q ] [ r ] = lift-≈ (assoc p q r)
      assoc _     [ p ] [ q ] ∙     = ≈∙-refl _≈_ refl-≈
      assoc _     [ p ] ∙     [ r ] = ≈∙-refl _≈_ refl-≈
      assoc _     [ p ] ∙     ∙     = ≈∙-refl _≈_ refl-≈
      assoc _     ∙     [ r ] [ q ] = ≈∙-refl _≈_ refl-≈
      assoc _     ∙     [ q ] ∙     = ≈∙-refl _≈_ refl-≈
      assoc _     ∙     ∙     [ r ] = ≈∙-refl _≈_ refl-≈
      assoc _     ∙     ∙     ∙     = ≈∙-refl _≈_ refl-≈

      identityˡ : LeftIdentity _≈∙_ ∙ (op∙)
      identityˡ [ p ] = ≈∙-refl _≈_ refl-≈
      identityˡ ∙     = ≈∙-refl _≈_ refl-≈

      identityʳ : RightIdentity _≈∙_ ∙ (op∙)
      identityʳ [ p ] = ≈∙-refl _≈_ refl-≈
      identityʳ ∙     = ≈∙-refl _≈_ refl-≈

      identity : Identity _≈∙_ ∙ (op∙)
      identity = identityˡ , identityʳ

    module _ {_≈_ : Rel A ℓ} {op : Op₂ A} where
      private
        _≈∙_ = lift≈ _≈_
        op∙ = liftOp op

      isMagma : IsMagma _≈_ op → IsMagma _≈∙_ op∙
      isMagma M =
        record
        { isEquivalence = ≈∙-isEquivalence _≈_ M.isEquivalence
        ; ∙-cong        = cong₂ M.refl M.∙-cong
        } where module M = IsMagma M

      isSemigroup : IsSemigroup _≈_ op → IsSemigroup _≈∙_ op∙
      isSemigroup S = record
        { isMagma = isMagma S.isMagma
        ; assoc   = assoc S.refl S.assoc
        } where module S = IsSemigroup S

      isMonoid : IsSemigroup _≈_ op → IsMonoid _≈∙_ op∙ ∙
      isMonoid S = record
        { isSemigroup = isSemigroup S
        ; identity    = identity S.refl
        } where module S = IsSemigroup S

    semigroup : Semigroup a (a ⊔ ℓ) → Semigroup a (a ⊔ ℓ)
    semigroup S = record
      { Carrier = Pointed S.Carrier
      ; isSemigroup = isSemigroup S.isSemigroup
      } where module S = Semigroup S

    monoid : Semigroup a (a ⊔ ℓ) → Monoid a (a ⊔ ℓ)
    monoid S = record
      { isMonoid = isMonoid S.isSemigroup
      } where module S = Semigroup S