------------------------------------------------------------------------
-- 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
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
    }