```------------------------------------------------------------------------
-- The Agda standard library
--
-- Algebraic properties of products
------------------------------------------------------------------------

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

module Data.Product.Algebra where

open import Algebra
open import Data.Bool.Base using (true; false)
open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
open import Data.Product
open import Data.Product.Properties
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
open import Data.Sum.Algebra
open import Data.Unit.Polymorphic using (⊤; tt)
open import Function.Base using (_∘′_)
open import Function.Bundles using (_↔_; Inverse; mk↔′)
open import Function.Properties.Inverse using (↔-isEquivalence)
open import Level using (Level; suc)
open import Relation.Binary.PropositionalEquality.Core

import Function.Definitions as FuncDef

------------------------------------------------------------------------

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

module _ {A : Set a} {B : Set b} where
open FuncDef {A = A} {B} _≡_ _≡_

------------------------------------------------------------------------
-- Properties of Σ

-- Σ is associative
Σ-assoc : {B : A → Set b} {C : (a : A) → B a → Set c} →
Σ (Σ A B) (uncurry C) ↔ Σ A (λ a → Σ (B a) (C a))
Σ-assoc = mk↔′ assocʳ assocˡ cong′ cong′

-- Σ is associative, alternate formulation
Σ-assoc-alt : {B : A → Set b} {C : Σ A B → Set c} →
Σ (Σ A B) C ↔ Σ A (λ a → Σ (B a) (curry C a))
Σ-assoc-alt = mk↔′ assocʳ-curried assocˡ-curried cong′ cong′

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

-- × is a congruence
×-cong : A ↔ B → C ↔ D → (A × C) ↔ (B × D)
×-cong i j = mk↔′ (map I.to J.to) (map I.from J.from)
(λ {(a , b) → cong₂ _,_ (I.inverseˡ a) (J.inverseˡ b)})
(λ {(a , b) → cong₂ _,_ (I.inverseʳ a) (J.inverseʳ b)})
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′

-- ⊤ is the identity for ×
×-identityˡ : LeftIdentity {ℓ = ℓ} _↔_ ⊤ _×_
×-identityˡ _ = mk↔′ proj₂ (tt ,_) cong′ cong′

×-identityʳ : RightIdentity {ℓ = ℓ} _↔_ ⊤ _×_
×-identityʳ _ = mk↔′ proj₁ (_, tt) cong′ cong′

×-identity : Identity _↔_ ⊤ _×_
×-identity = ×-identityˡ , ×-identityʳ

-- ⊥ is the zero for ×
×-zeroˡ : LeftZero {ℓ = ℓ} _↔_ ⊥ _×_
×-zeroˡ A = mk↔′ proj₁ ⊥-elim ⊥-elim λ ()

×-zeroʳ : RightZero {ℓ = ℓ} _↔_ ⊥ _×_
×-zeroʳ A = mk↔′ proj₂ ⊥-elim ⊥-elim λ ()

×-zero : Zero _↔_ ⊥ _×_
×-zero = ×-zeroˡ , ×-zeroʳ

-- × distributes over ⊎
×-distribˡ-⊎ : _DistributesOverˡ_ {ℓ = ℓ} _↔_ _×_ _⊎_
×-distribˡ-⊎ _ _ _ = mk↔′
(uncurry λ x → [ inj₁ ∘′ (x ,_) , inj₂ ∘′ (x ,_) ]′)
[ map₂ inj₁ , map₂ inj₂ ]′
Sum.[ cong′ , cong′ ]
(uncurry λ _ → Sum.[ cong′ , cong′ ])

×-distribʳ-⊎ : _DistributesOverʳ_ {ℓ = ℓ} _↔_ _×_ _⊎_
×-distribʳ-⊎ _ _ _ = mk↔′
(uncurry [ curry inj₁ , curry inj₂ ]′)
[ map₁ inj₁ , map₁ inj₂ ]′
Sum.[ cong′ , cong′ ]
(uncurry Sum.[ (λ _ → cong′) , (λ _ → cong′) ])

×-distrib-⊎ : _DistributesOver_ {ℓ = ℓ} _↔_ _×_ _⊎_
×-distrib-⊎ = ×-distribˡ-⊎ , ×-distribʳ-⊎

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

⊎-×-isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _↔_ _⊎_ _×_ ⊥ ⊤
⊎-×-isSemiringWithoutAnnihilatingZero = record
{ +-isCommutativeMonoid = ⊎-isCommutativeMonoid ℓ
; *-cong                = ×-cong
; *-assoc               = ×-assoc
; *-identity            = ×-identity
; distrib               = ×-distrib-⊎
}

⊎-×-isSemiring : IsSemiring _↔_ _⊎_ _×_ ⊥ ⊤
⊎-×-isSemiring = record
{ isSemiringWithoutAnnihilatingZero = ⊎-×-isSemiringWithoutAnnihilatingZero
; zero                              = ×-zero
}

⊎-×-isCommutativeSemiring : IsCommutativeSemiring _↔_ _⊎_ _×_ ⊥ ⊤
⊎-×-isCommutativeSemiring = record
{ isSemiring = ⊎-×-isSemiring
; *-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
}

×-⊎-commutativeSemiring : CommutativeSemiring (suc ℓ) ℓ
×-⊎-commutativeSemiring = record
{ isCommutativeSemiring = ⊎-×-isCommutativeSemiring
}
```