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

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

open import Algebra.Bundles using (Magma)
open import Algebra.Definitions
open import Data.Bool.Base using (true; false)
open import Data.Product.Base using (_×_; _,_)
open import Data.Product.Relation.Binary.Pointwise.NonDependent using (Pointwise)
open import Data.Sum.Base using (inj₁; inj₂; map)
open import Function.Base using (_∘_)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Nullary.Decidable.Core using (does; yes; no)
open import Relation.Nullary.Negation.Core using (¬_; contradiction; contradiction₂)
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning

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  _≋_
  _≋_ : 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  = map (ab≈a ,_) (ab≈b ,_) (◦-sel x y)