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

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

    open import Algebra.Core using (Op₂)
    open import Data.Bool.Base using (true; false)
    open import Data.Product.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)

    module Algebra.Construct.LexProduct.Base
      {a b ℓ} {A : Set a} {B : Set b}
      (_∙_ : Op₂ A) (_◦_ : Op₂ B)
      {_≈₁_ : Rel A ℓ} (_≟₁_ : Decidable _≈₁_)
      where

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

    -- In order to get the first component to be definitionally equal to
    -- `a ∙ b` and to simplify some of the proofs we first define an inner
    -- operator that only calculates the second component of product.

    innerLex : A → A → B → B → B
    innerLex a b x y with does ((a ∙ b) ≟₁ a) | does ((a ∙ b) ≟₁ b)
    ... | true  | false = x
    ... | false | true  = y
    ... |     _ |     _ = x ◦ y

    -- The full lexicographic choice operator can then be simply defined
    -- in terms of the inner one.

    lex : Op₂ (A × B)
    lex (a , x) (b , y) = (a ∙ b , innerLex a b x y)