    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Algebraic properties of sums (disjoint unions)
    ------------------------------------------------------------------------

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

    module Data.Sum.Algebra where

    open import Algebra.Bundles
      using (Magma; Semigroup; Monoid; CommutativeMonoid)
    open import Algebra.Definitions
      using (Associative; LeftIdentity; RightIdentity; Identity)
    open import Algebra.Structures
      using (IsMagma; IsSemigroup; IsMonoid; IsCommutativeMonoid)
    open import Data.Empty.Polymorphic using (⊥)
    open import Data.Product.Base using (_,_)
    open import Data.Sum.Base using (_⊎_; inj₁; inj₂; map; [_,_]; swap; assocʳ; assocˡ)
    open import Data.Sum.Properties using (swap-involutive)
    open import Data.Unit.Polymorphic.Base using (⊤; tt)
    open import Function.Base using (id; _∘_)
    open import Function.Properties.Inverse using (↔-isEquivalence)
    open import Function.Bundles using (_↔_; Inverse; mk↔ₛ′)
    open import Level using (Level; suc)
    open import Relation.Binary.PropositionalEquality.Core
      using (_≡_; refl; cong; cong′)

    import Function.Definitions as FuncDef

    ------------------------------------------------------------------------
    -- Setup

    private
      variable
        a b c d : Level
        A B C D : Set a

      ♯ : {B : ⊥ {a} → Set b} → (w : ⊥) → B w
      ♯ ()

    ------------------------------------------------------------------------
    -- Algebraic properties

    ⊎-cong : A ↔ B → C ↔ D → (A ⊎ C) ↔ (B ⊎ D)
    ⊎-cong i j = mk↔ₛ′ (map I.to J.to) (map I.from J.from)
      [ cong inj₁ ∘ I.strictlyInverseˡ , cong inj₂ ∘ J.strictlyInverseˡ ]
      [ cong inj₁ ∘ I.strictlyInverseʳ , cong inj₂ ∘ J.strictlyInverseʳ ]
      where module I = Inverse i; module J = Inverse j

    -- ⊎ is commutative.
    -- We don't use Commutative because it isn't polymorphic enough.
    ⊎-comm : (A : Set a) (B : Set b) → (A ⊎ B) ↔ (B ⊎ A)
    ⊎-comm _ _ = mk↔ₛ′ swap swap swap-involutive swap-involutive

    module _ (ℓ : Level) where

      -- ⊎ is associative
      ⊎-assoc : Associative {ℓ = ℓ} _↔_ _⊎_
      ⊎-assoc _ _ _ = mk↔ₛ′ assocʳ assocˡ
        [ cong′ , [ cong′ , cong′ ] ] [ [ cong′ , cong′ ] , cong′ ]

      -- ⊥ is an identity for ⊎
      ⊎-identityˡ : LeftIdentity {ℓ = ℓ} _↔_ ⊥ _⊎_
      ⊎-identityˡ A = mk↔ₛ′ [ ♯ , id ] inj₂ cong′ [ ♯ , cong′ ]

      ⊎-identityʳ : RightIdentity {ℓ = ℓ} _↔_ ⊥ _⊎_
      ⊎-identityʳ _ = mk↔ₛ′ [ id , ♯ ] inj₁ cong′ [ cong′ , ♯ ]

      ⊎-identity : Identity _↔_ ⊥ _⊎_
      ⊎-identity = ⊎-identityˡ , ⊎-identityʳ

    ------------------------------------------------------------------------
    -- Algebraic structures

      ⊎-isMagma : IsMagma {ℓ = ℓ} _↔_ _⊎_
      ⊎-isMagma = record
        { isEquivalence = ↔-isEquivalence
        ; ∙-cong        = ⊎-cong
        }

      ⊎-isSemigroup : IsSemigroup _↔_ _⊎_
      ⊎-isSemigroup = record
        { isMagma = ⊎-isMagma
        ; assoc   = ⊎-assoc
        }

      ⊎-isMonoid : IsMonoid _↔_ _⊎_ ⊥
      ⊎-isMonoid = record
        { isSemigroup = ⊎-isSemigroup
        ; identity    = ⊎-identityˡ , ⊎-identityʳ
        }

      ⊎-isCommutativeMonoid : IsCommutativeMonoid _↔_ _⊎_ ⊥
      ⊎-isCommutativeMonoid = record
        { isMonoid = ⊎-isMonoid
        ; comm     = ⊎-comm
        }

    ------------------------------------------------------------------------
    -- Algebraic bundles

      ⊎-magma : Magma (suc ℓ) ℓ
      ⊎-magma = record
        { isMagma = ⊎-isMagma
        }

      ⊎-semigroup : Semigroup (suc ℓ) ℓ
      ⊎-semigroup = record
        { isSemigroup = ⊎-isSemigroup
        }

      ⊎-monoid : Monoid (suc ℓ) ℓ
      ⊎-monoid = record
        { isMonoid = ⊎-isMonoid
        }

      ⊎-commutativeMonoid : CommutativeMonoid (suc ℓ) ℓ
      ⊎-commutativeMonoid = record
        { isCommutativeMonoid = ⊎-isCommutativeMonoid
        }