diff --git a/CHANGELOG.md b/CHANGELOG.md
index b1625a1861..246c68f108 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -772,6 +772,11 @@ Deprecated names
 New modules
 -----------
 
+* Algebraic structures when freely adding an identity element:
+```
+  Algebra.Construct.Add.Identity
+```
+
 * Operations for module-like algebraic structures:
   ```
   Algebra.Module.Core
@@ -942,6 +947,11 @@ New modules
 Other minor changes
 -------------------
 
+* Added new proof to `Data.Maybe.Properties`
+```agda
+    <∣>-idem : Idempotent _<∣>_
+```
+
 * The module `Algebra` now publicly re-exports the contents of
   `Algebra.Structures.Biased`.
 
@@ -1939,4 +1949,4 @@ This is a full list of proofs that have changed form to use irrelevant instance
   ```agda
   Inverse⇒Injection : Inverse S T → Injection S T
   ↔⇒↣ : A ↔ B → A ↣ B
-  ```
\ No newline at end of file
+  ```
diff --git a/src/Algebra/Construct/Add/Identity.agda b/src/Algebra/Construct/Add/Identity.agda
new file mode 100644
index 0000000000..51c536cdaa
--- /dev/null
+++ b/src/Algebra/Construct/Add/Identity.agda
@@ -0,0 +1,103 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definition of algebraic structures we get from freely adding an
+-- identity element
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Algebra.Construct.Add.Identity where
+
+open import Algebra.Bundles
+open import Algebra.Core using (Op₂)
+open import Algebra.Definitions
+open import Algebra.Structures
+open import Relation.Binary.Construct.Add.Point.Equality renaming (_≈∙_ to lift≈)
+open import Data.Product using (_,_)
+open import Level using (Level; _⊔_)
+open import Relation.Binary.Core
+open import Relation.Binary.Definitions
+open import Relation.Binary.Structures
+open import Relation.Nullary.Construct.Add.Point
+
+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
diff --git a/src/Data/Maybe/Properties.agda b/src/Data/Maybe/Properties.agda
index 2df06d3f88..018e364899 100644
--- a/src/Data/Maybe/Properties.agda
+++ b/src/Data/Maybe/Properties.agda
@@ -114,6 +114,10 @@ module _ {A : Set a} where
   <∣>-identity : Identity nothing _<∣>_
   <∣>-identity = <∣>-identityˡ , <∣>-identityʳ
 
+  <∣>-idem : Idempotent _<∣>_
+  <∣>-idem (just x) = refl
+  <∣>-idem nothing = refl
+
 module _ (A : Set a) where
 
   open Structures {A = Maybe A} _≡_