```------------------------------------------------------------------------
-- The Agda standard library
--
-- Definitions of the lexicographic product of two operators.
------------------------------------------------------------------------

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

open import Algebra
open import Data.Bool using (true; false)
open import Data.Product
open import Data.Product.Relation.Binary.Pointwise.NonDependent using (Pointwise)
open import Data.Sum.Base using (inj₁; inj₂)
open import Function.Base using (_∘_)
open import Relation.Binary
open import Relation.Nullary using (¬_; does; yes; no)
import Relation.Binary.Reasoning.Setoid as SetoidReasoning

module Algebra.Construct.LexProduct
{ℓ₁ ℓ₂ ℓ₃ ℓ₄} (M : Magma ℓ₁ ℓ₂) (N : Magma ℓ₃ ℓ₄)
(_≟₁_ : Decidable (Magma._≈_ M))
where

open Magma M using (_∙_ ; ∙-cong)
renaming
( Carrier  to A
; _≈_      to _≈₁_
; _≉_      to _≉₁_
)

open Magma N using ()
renaming
( Carrier to B
; _∙_     to _◦_
; _≈_     to _≈₂_
; refl    to ≈₂-refl
)

import Algebra.Construct.LexProduct.Inner M N _≟₁_ as InnerLex

private
infix 4 _≋_
_≋_ : Rel (A × B) _
_≋_ = Pointwise _≈₁_ _≈₂_

variable
a b : A

------------------------------------------------------------------------
-- Definition
------------------------------------------------------------------------

open import Algebra.Construct.LexProduct.Base _∙_ _◦_ _≟₁_ public
renaming (lex to _⊕_)

------------------------------------------------------------------------
-- Properties
------------------------------------------------------------------------
-- Basic cases

case₁ : ∀ {a b} → (a ∙ b) ≈₁ a → (a ∙ b) ≉₁ b →
∀ x y → (a , x) ⊕ (b , y) ≋ (a , x)
case₁ ab≈a ab≉b _ _ = ab≈a , InnerLex.case₁ ab≈a ab≉b

case₂ : ∀ {a b} → (a ∙ b) ≉₁ a → (a ∙ b) ≈₁ b →
∀ x y → (a , x) ⊕ (b , y) ≋ (b , y)
case₂ ab≉a ab≈b _ _ = ab≈b , InnerLex.case₂ ab≉a ab≈b

case₃ : ∀ {a b} → (a ∙ b) ≈₁ a → (a ∙ b) ≈₁ b →
∀ x y → (a , x) ⊕ (b , y) ≋ (a , x ◦ y)
case₃ ab≈a ab≈b _ _ = ab≈a , InnerLex.case₃ ab≈a ab≈b

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

cong : Congruent₂ _≋_ _⊕_
cong (a≈b , w≈x) (c≈d , y≈z) =
∙-cong a≈b c≈d ,
InnerLex.cong a≈b c≈d w≈x y≈z

assoc : Associative _≈₁_ _∙_ → Commutative _≈₁_ _∙_ →
Selective _≈₁_ _∙_ → Associative _≈₂_ _◦_ →
Associative _≋_ _⊕_
assoc ∙-assoc ∙-comm ∙-sel ◦-assoc (a , x) (b , y) (c , z) =
∙-assoc a b c ,
InnerLex.assoc ∙-assoc ∙-comm ∙-sel ◦-assoc a b c x y z

comm : Commutative _≈₁_ _∙_ → Commutative _≈₂_ _◦_ →
Commutative _≋_ _⊕_
comm ∙-comm ◦-comm (a , x) (b , y) =
∙-comm a b ,
InnerLex.comm ∙-comm ◦-comm a b x y

zeroʳ : ∀ {e f} → RightZero _≈₁_ e _∙_ → RightZero _≈₂_ f _◦_ →
RightZero _≋_ (e , f) _⊕_
zeroʳ ze₁ ze₂ (x , a) = ze₁ x , InnerLex.zeroʳ ze₁ ze₂

identityʳ : ∀ {e f} → RightIdentity _≈₁_ e _∙_ → RightIdentity _≈₂_ f _◦_ →
RightIdentity _≋_ (e , f) _⊕_
identityʳ id₁ id₂ (x , a) = id₁ x , InnerLex.identityʳ id₁ id₂

sel : Selective _≈₁_ _∙_ → Selective _≈₂_ _◦_ → Selective _≋_ _⊕_
sel ∙-sel ◦-sel (a , x) (b , y) with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b
... | no  ab≉a | no  ab≉b  = contradiction₂ (∙-sel a b) ab≉a ab≉b
... | yes ab≈a | no  _     = inj₁ (ab≈a , ≈₂-refl)
... | no  _    | yes ab≈b  = inj₂ (ab≈b , ≈₂-refl)
... | yes ab≈a | yes ab≈b  with ◦-sel x y
...   | inj₁ xy≈x = inj₁ (ab≈a , xy≈x)
...   | inj₂ xy≈y = inj₂ (ab≈b , xy≈y)
```