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

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

    open import Algebra
    open import Data.Bool.Base using (false; true)
    open import Data.Product.Base using (_×_; _,_; swap; map; uncurry′)
    open import Function.Base using (_∘_)
    open import Level using (Level; _⊔_)
    open import Relation.Binary.Definitions using (Decidable)
    open import Relation.Nullary.Decidable using (does; yes; no)
    open import Relation.Nullary.Negation
      using (contradiction; contradiction₂)
    import Relation.Binary.Reasoning.Setoid as SetoidReasoning

    import Algebra.Construct.LexProduct.Base as Base

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

    open module M = Magma M
      renaming
      ( Carrier  to A
      ; _≈_      to _≈₁_
      ; _≉_      to _≉₁_
      )

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

    private
      variable
        a b c d : A
        w x y z : B

    ------------------------------------------------------------------------
    -- Base definition

    open Base _∙_ _◦_ _≟₁_ public
      using (innerLex)

    -- Save ourselves some typing in this file
    private
      lex = innerLex

    ------------------------------------------------------------------------
    -- Properties

    module NaturalOrder where

      -- It would be really nice if we could use
      -- `Relation.Binary.Construct.NaturalOrder.Left/Right` to prove these
      -- properties but the equalities are defined the wrong way around

      open SetoidReasoning M.setoid

      ≤∙ˡ-resp-≈ : a ∙ b ≈₁ b → a ≈₁ c → b ≈₁ d → c ∙ d ≈₁ d
      ≤∙ˡ-resp-≈ {a} {b} {c} {d} ab≈b a≈c b≈d = begin
        c ∙ d ≈⟨ ∙-cong (M.sym a≈c) (M.sym b≈d) ⟩
        a ∙ b ≈⟨ ab≈b ⟩
        b     ≈⟨ b≈d ⟩
        d     ∎

      ≤∙ʳ-resp-≈ : a ∙ b ≈₁ a → a ≈₁ c → b ≈₁ d → c ∙ d ≈₁ c
      ≤∙ʳ-resp-≈ {a} {b} {c} {d} ab≈b a≈c b≈d = begin
        c ∙ d ≈⟨ ∙-cong (M.sym a≈c) (M.sym b≈d) ⟩
        a ∙ b ≈⟨ ab≈b ⟩
        a     ≈⟨ a≈c ⟩
        c     ∎

      ≤∙ˡ-trans : Associative _≈₁_ _∙_ → (a ∙ b) ≈₁ b → (b ∙ c) ≈₁ c → (a ∙ c) ≈₁ c
      ≤∙ˡ-trans {a} {b} {c} ∙-assoc ab≈b bc≈c = begin
        a ∙ c        ≈⟨ ∙-congˡ bc≈c ⟨
        a ∙ (b ∙ c)  ≈⟨ ∙-assoc a b c ⟨
        (a ∙ b) ∙ c  ≈⟨  ∙-congʳ ab≈b ⟩
        b ∙ c        ≈⟨  bc≈c ⟩
        c            ∎

      ≰∙ˡ-trans : Commutative _≈₁_ _∙_ → (a ∙ b) ≉₁ a → (a ∙ c) ≈₁ c → (b ∙ c) ≈₁ c → (a ∙ c) ≉₁ a
      ≰∙ˡ-trans {a} {b} {c} ∙-comm ab≉a ac≈c bc≈c ac≈a = ab≉a (begin
        a ∙ b  ≈⟨ ∙-congʳ (M.trans (M.sym ac≈a) ac≈c) ⟩
        c ∙ b  ≈⟨ ∙-comm c b ⟩
        b ∙ c  ≈⟨ bc≈c ⟩
        c      ≈⟨ M.trans (M.sym ac≈c) ac≈a ⟩
        a      ∎)

      <∙ˡ-trans : Associative _≈₁_ _∙_ → Commutative _≈₁_ _∙_ →
                  (a ∙ b) ≈₁ b → (a ∙ b) ≉₁ a → (b ∙ c) ≈₁ c →
                  (a ∙ c) ≉₁ a × (a ∙ c) ≈₁ c
      <∙ˡ-trans {a} {b} {c} ∙-assoc ∙-comm ab≈b ab≉a bc≈c = ac≉a , ac≈c
        where
        ac≈c = ≤∙ˡ-trans ∙-assoc ab≈b bc≈c
        ac≉a = ≰∙ˡ-trans ∙-comm ab≉a ac≈c bc≈c

      <∙ʳ-trans : Associative _≈₁_ _∙_ → Commutative _≈₁_ _∙_ →
                  (a ∙ b) ≈₁ a → (b ∙ c) ≈₁ b → (b ∙ c) ≉₁ c →
                  (a ∙ c) ≈₁ a × (a ∙ c) ≉₁ c
      <∙ʳ-trans {a} {b} {c} assoc comm ab≈a bc≈b bc≉c = map
        (M.trans (comm a c))
        (_∘ M.trans (comm c a))
        (swap (<∙ˡ-trans assoc comm
          (M.trans (comm c b) bc≈b)
          (bc≉c ∘ M.trans (comm b c))
          (M.trans (comm b a) ab≈a)))

    ------------------------------------------------------------------------
    -- Basic properties

    open SetoidReasoning N.setoid
    open NaturalOrder

    case₁ : a ∙ b ≈₁ a → a ∙ b ≉₁ b → lex a b x y ≈₂ x
    case₁ {a} {b} ab≈a ab≉b with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b
    ... | no  ab≉a | _        = contradiction ab≈a ab≉a
    ... | yes _    | yes ab≈b = contradiction ab≈b ab≉b
    ... | yes _    | no  _    = N.refl

    case₂ : a ∙ b ≉₁ a → a ∙ b ≈₁ b → lex a b x y ≈₂ y
    case₂ {a} {b} ab≉a ab≈b with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b
    ... | yes ab≈a | _        = contradiction ab≈a ab≉a
    ... | no _     | no  ab≉b = contradiction ab≈b ab≉b
    ... | no _     | yes _    = N.refl

    case₃ : a ∙ b ≈₁ a → a ∙ b ≈₁ b → lex a b x y ≈₂ (x ◦ y)
    case₃ {a} {b} ab≈a ab≈b with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b
    ... | no  ab≉a | _        = contradiction ab≈a ab≉a
    ... | yes _    | no  ab≉b = contradiction ab≈b ab≉b
    ... | yes _    | yes _    = N.refl

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

    cong : a ≈₁ b → c ≈₁ d → w ≈₂ x → y ≈₂ z → lex a c w y ≈₂ lex b d x z
    cong {a} {b} {c} {d} a≈b c≈d w≈x y≈z
      with (a ∙ c) ≟₁ a | (a ∙ c) ≟₁ c | (b ∙ d) ≟₁ b | (b ∙ d) ≟₁ d
    ... | yes _    | yes _    | yes _    | yes _    = ◦-cong w≈x y≈z
    ... | yes _    | yes _    | no  _    | no  _    = ◦-cong w≈x y≈z
    ... | no  _    | no  _    | yes _    | yes _    = ◦-cong w≈x y≈z
    ... | no  _    | no  _    | no  _    | no  _    = ◦-cong w≈x y≈z
    ... | yes _    | no  _    | yes _    | no  _    = w≈x
    ... | no  _    | yes _    | no  _    | yes _    = y≈z
    ... | _        | yes ac≈c | _        | no bd≉d  = contradiction (≤∙ˡ-resp-≈ ac≈c a≈b c≈d) bd≉d
    ... | yes ac≈a | _        | no  bd≉b | _        = contradiction (≤∙ʳ-resp-≈ ac≈a a≈b c≈d) bd≉b
    ... | _        | no  ac≉c | _        | yes bd≈d = contradiction (≤∙ˡ-resp-≈ bd≈d (M.sym a≈b) (M.sym c≈d)) ac≉c
    ... | no  ac≉a | _        | yes bd≈b | _        = contradiction (≤∙ʳ-resp-≈ bd≈b (M.sym a≈b) (M.sym c≈d)) ac≉a

    cong₁₂ : a ≈₁ b → c ≈₁ d → lex a c x y ≈₂ lex b d x y
    cong₁₂ a≈b c≈d = cong a≈b c≈d N.refl N.refl

    cong₁ : a ≈₁ b → lex a c x y ≈₂ lex b c x y
    cong₁ a≈b = cong₁₂ a≈b M.refl

    cong₂ : b ≈₁ c → lex a b x y ≈₂ lex a c x y
    cong₂ = cong₁₂ M.refl

    -- It is possible to relax this. Instead of ∙ being selective and ◦
    -- being associative it's also possible for _◦_ to return a single
    -- idempotent element.
    assoc : Associative _≈₁_ _∙_ → Commutative _≈₁_ _∙_ →
            Selective _≈₁_ _∙_ → Associative _≈₂_ _◦_ →
            ∀ a b c x y z  → lex (a ∙ b) c (lex a b x y) z  ≈₂ lex a (b ∙ c) x (lex b c y z)
    assoc ∙-assoc ∙-comm ∙-sel ◦-assoc a b c x y z
      with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b | (b ∙ c) ≟₁ b | (b ∙ c) ≟₁ c
    ... | _        | _        | no  bc≉b | no  bc≉c = contradiction₂ (∙-sel b c) bc≉b bc≉c
    ... | no  ab≉a | no  ab≉b | _        | _        = contradiction₂ (∙-sel a b) ab≉a ab≉b
    ... | yes ab≈a | no  ab≉b | no  bc≉b | yes bc≈c = cong₁₂ ab≈a (M.sym bc≈c)
    ... | no ab≉a  | yes ab≈b | yes bc≈b | yes bc≈c = begin
      lex (a ∙ b) c y z        ≈⟨  cong₁ ab≈b ⟩
      lex b c y z              ≈⟨  case₃ bc≈b bc≈c ⟩
      y ◦ z                    ≈⟨ case₂ ab≉a ab≈b ⟨
      lex a b x (y ◦ z)        ≈⟨ cong₂ bc≈b ⟨
      lex a (b ∙ c) x (y ◦ z)  ∎
    ... | no ab≉a  | yes ab≈b | yes bc≈b | no bc≉c = begin
      lex (a ∙ b) c y z        ≈⟨  cong₁ ab≈b ⟩
      lex b c y z              ≈⟨  case₁ bc≈b bc≉c ⟩
      y                        ≈⟨ case₂ ab≉a ab≈b ⟨
      lex a b x y              ≈⟨ cong₂ bc≈b ⟨
      lex a (b ∙ c) x y        ∎
    ... | yes ab≈a | yes ab≈b | yes bc≈b | no bc≉c = begin
      lex (a ∙ b) c (x ◦ y) z  ≈⟨  cong₁ ab≈b ⟩
      lex b c (x ◦ y) z        ≈⟨  case₁ bc≈b bc≉c ⟩
      x ◦ y                    ≈⟨ case₃ ab≈a ab≈b ⟨
      lex a b x y              ≈⟨ cong₂ bc≈b ⟨
      lex a (b ∙ c) x y        ∎
    ... | yes ab≈a | yes ab≈b | yes bc≈b | yes bc≈c = begin
      lex (a ∙ b) c (x ◦ y) z  ≈⟨  cong₁ ab≈b ⟩
      lex b c (x ◦ y) z        ≈⟨  case₃ bc≈b bc≈c  ⟩
      (x ◦ y) ◦ z              ≈⟨  ◦-assoc x y z ⟩
      x ◦ (y ◦ z)              ≈⟨ case₃ ab≈a ab≈b ⟨
      lex a b x (y ◦ z)        ≈⟨ cong₂ bc≈b ⟨
      lex a (b ∙ c) x (y ◦ z)  ∎
    ... | yes ab≈a | yes ab≈b | no bc≉b | yes bc≈c = begin
      lex (a ∙ b) c (x ◦ y) z  ≈⟨  cong₁ ab≈b ⟩
      lex b c (x ◦ y) z        ≈⟨  case₂ bc≉b bc≈c ⟩
      z                        ≈⟨ case₂ bc≉b bc≈c ⟨
      lex b c x z              ≈⟨ cong₁₂ (M.trans (M.sym ab≈a) ab≈b) bc≈c ⟨
      lex a (b ∙ c) x z        ∎
    ... | yes ab≈a | no ab≉b | yes bc≈b | yes bc≈c = begin
      lex (a ∙ b) c x z        ≈⟨  cong₁₂ ab≈a (M.trans (M.sym bc≈c) bc≈b) ⟩
      lex a b x z              ≈⟨  case₁ ab≈a ab≉b ⟩
      x                        ≈⟨ case₁ ab≈a ab≉b ⟨
      lex a b x (y ◦ z)        ≈⟨ cong₂ bc≈b ⟨
      lex a (b ∙ c) x (y ◦ z)  ∎
    ... | no ab≉a | yes ab≈b | no bc≉b | yes bc≈c = begin
      lex (a ∙ b) c y z        ≈⟨  cong₁ ab≈b ⟩
      lex b c y z              ≈⟨  case₂ bc≉b bc≈c ⟩
      z                        ≈⟨ uncurry′ case₂ (<∙ˡ-trans ∙-assoc ∙-comm ab≈b ab≉a bc≈c) ⟨
      lex a c x z              ≈⟨ cong₂ bc≈c ⟨
      lex a (b ∙ c) x z        ∎
    ... | yes ab≈a | no ab≉b | yes bc≈b | no bc≉c = begin
      lex (a ∙ b) c x z        ≈⟨  cong₁ ab≈a ⟩
      lex a c x z              ≈⟨  uncurry′ case₁ (<∙ʳ-trans ∙-assoc ∙-comm ab≈a bc≈b bc≉c) ⟩
      x                        ≈⟨ case₁ ab≈a ab≉b ⟨
      lex a b x y              ≈⟨ cong₂ bc≈b ⟨
      lex a (b ∙ c) x y        ∎

    comm : Commutative _≈₁_ _∙_ → Commutative _≈₂_ _◦_ →
           ∀ a b x y → lex a b x y ≈₂ lex b a y x
    comm ∙-comm ◦-comm a b x y
      with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b | (b ∙ a) ≟₁ b | (b ∙ a) ≟₁ a
    ... | yes ab≈a | _        | _        | no  ba≉a = contradiction (M.trans (∙-comm b a) ab≈a) ba≉a
    ... | no  ab≉a | _        | _        | yes ba≈a = contradiction (M.trans (∙-comm a b) ba≈a) ab≉a
    ... | _        | yes ab≈b | no  ba≉b | _        = contradiction (M.trans (∙-comm b a) ab≈b) ba≉b
    ... | _        | no  ab≉b | yes ba≈b | _        = contradiction (M.trans (∙-comm a b) ba≈b) ab≉b
    ... | yes _    | yes _    | yes _    | yes _    = ◦-comm x y
    ... | yes _    | no  _    | no  _    | yes _    = N.refl
    ... | no  _    | yes _    | yes _    | no  _    = N.refl
    ... | no  _    | no  _    | no  _    | no  _    = ◦-comm x y

    idem : Idempotent _≈₂_ _◦_ → ∀ a b x → lex a b x x ≈₂ x
    idem ◦-idem a b x with does ((a ∙ b) ≟₁ a) | does ((a ∙ b) ≟₁ b)
    ... | false | false = ◦-idem x
    ... | false | true  = N.refl
    ... | true  | false = N.refl
    ... | true  | true  = ◦-idem x

    zeroʳ : ∀ {e f} → RightZero _≈₁_ e _∙_ → RightZero _≈₂_ f _◦_ →
            lex a e x f ≈₂ f
    zeroʳ {a} {x} {e} {f} ze₁ ze₂ with (a ∙ e) ≟₁ a | (a ∙ e) ≟₁ e
    ... | _     | no  a∙e≉e = contradiction (ze₁ a) a∙e≉e
    ... | no  _ | yes _     = N.refl
    ... | yes _ | yes _     = ze₂ x

    identityʳ : ∀ {e f} → RightIdentity _≈₁_ e _∙_ → RightIdentity _≈₂_ f _◦_ →
                lex a e x f ≈₂ x
    identityʳ {a} {x} {e} {f} id₁ id₂ with (a ∙ e) ≟₁ a | (a ∙ e) ≟₁ e
    ... | no  a∙e≉a | _     = contradiction (id₁ a) a∙e≉a
    ... | yes _     | no  _ = N.refl
    ... | yes _     | yes _ = id₂ x