    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Choosing between elements based on the result of applying a function
    ------------------------------------------------------------------------

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

    open import Algebra

    module Algebra.Construct.LiftedChoice where

    open import Algebra.Consequences.Base using (sel⇒idem)
    open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′)
    open import Data.Product.Base using (_×_; _,_)
    open import Function.Base using (const; _$_)
    open import Level using (Level; _⊔_)
    open import Relation.Binary.Core using (Rel; _⇒_; _Preserves_⟶_)
    open import Relation.Nullary using (¬_; yes; no)
    open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
    open import Relation.Binary.Structures using (IsEquivalence)
    open import Relation.Unary using (Pred)

    import Relation.Binary.Reasoning.Setoid as ≈-Reasoning

    private
      variable
        a b p ℓ : Level
        A : Set a
        B : Set b

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

    module _ (_≈_ : Rel B ℓ) (_•_ : Op₂ B) where

      Lift : Selective _≈_ _•_ → (A → B) → Op₂ A
      Lift ∙-sel f x y = [ const x , const y ]′ $ ∙-sel (f x) (f y)

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

    module _ {_≈_ : Rel B ℓ} {_∙_ : Op₂ B}
             (∙-isSelectiveMagma : IsSelectiveMagma _≈_ _∙_) where

      private module M = IsSelectiveMagma ∙-isSelectiveMagma
      open M hiding (sel; isMagma)
      open ≈-Reasoning setoid

      module _ (f : A → B) where

        private
          _◦_ = Lift _≈_ _∙_ M.sel f

        sel-≡ : Selective _≡_ _◦_
        sel-≡ x y with M.sel (f x) (f y)
        ... | inj₁ _ = inj₁ ≡.refl
        ... | inj₂ _ = inj₂ ≡.refl

        distrib : ∀ x y → ((f x) ∙ (f y)) ≈ f (x ◦ y)
        distrib x y with M.sel (f x) (f y)
        ... | inj₁ fx∙fy≈fx = fx∙fy≈fx
        ... | inj₂ fx∙fy≈fy = fx∙fy≈fy

      module _ (f : A → B) {_≈′_ : Rel A ℓ}
               (≈-reflexive : _≡_ ⇒ _≈′_) where

        private
          _◦_ = Lift _≈_ _∙_ M.sel f

        sel : Selective _≈′_ _◦_
        sel x y = Sum.map ≈-reflexive ≈-reflexive (sel-≡ f x y)

        idem : Idempotent _≈′_ _◦_
        idem = sel⇒idem _≈′_ sel

      module _ {f : A → B} {_≈′_ : Rel A ℓ}
               (f-injective : ∀ {x y} → f x ≈ f y → x ≈′ y)
               where

        private
          _◦_ = Lift _≈_ _∙_ M.sel f

        cong : f Preserves _≈′_ ⟶ _≈_ → Congruent₂ _≈′_ _◦_
        cong f-cong {x} {y} {u} {v} x≈y u≈v
          with M.sel (f x) (f u) | M.sel (f y) (f v)
        ... | inj₁ fx∙fu≈fx | inj₁ fy∙fv≈fy = x≈y
        ... | inj₂ fx∙fu≈fu | inj₂ fy∙fv≈fv = u≈v
        ... | inj₁ fx∙fu≈fx | inj₂ fy∙fv≈fv = f-injective (begin
          f x       ≈⟨ sym fx∙fu≈fx ⟩
          f x ∙ f u ≈⟨ ∙-cong (f-cong x≈y) (f-cong u≈v) ⟩
          f y ∙ f v ≈⟨ fy∙fv≈fv ⟩
          f v       ∎)
        ... | inj₂ fx∙fu≈fu | inj₁ fy∙fv≈fy = f-injective (begin
          f u       ≈⟨ sym fx∙fu≈fu ⟩
          f x ∙ f u ≈⟨ ∙-cong (f-cong x≈y) (f-cong u≈v) ⟩
          f y ∙ f v ≈⟨ fy∙fv≈fy ⟩
          f y       ∎)

        assoc : Associative _≈_ _∙_ → Associative _≈′_ _◦_
        assoc ∙-assoc x y z = f-injective (begin
          f ((x ◦ y) ◦ z)   ≈⟨ distrib f (x ◦ y) z ⟨
          f (x ◦ y) ∙ f z   ≈⟨ ∙-congʳ (distrib f x y) ⟨
          (f x ∙ f y) ∙ f z ≈⟨  ∙-assoc (f x) (f y) (f z) ⟩
          f x ∙ (f y ∙ f z) ≈⟨  ∙-congˡ (distrib f y z) ⟩
          f x ∙ f (y ◦ z)   ≈⟨  distrib f x (y ◦ z) ⟩
          f (x ◦ (y ◦ z))   ∎)

        comm : Commutative _≈_ _∙_ → Commutative _≈′_ _◦_
        comm ∙-comm x y = f-injective (begin
          f (x ◦ y) ≈⟨ distrib f x y ⟨
          f x ∙ f y ≈⟨  ∙-comm (f x) (f y) ⟩
          f y ∙ f x ≈⟨  distrib f y x ⟩
          f (y ◦ x) ∎)

    ------------------------------------------------------------------------
    -- Algebraic structures

      module _ {_≈′_ : Rel A ℓ} {f : A → B}
               (f-injective : ∀ {x y} → f x ≈ f y → x ≈′ y)
               (f-cong : f Preserves _≈′_ ⟶ _≈_)
               (≈′-isEquivalence : IsEquivalence _≈′_)
               where

        private
          module E = IsEquivalence ≈′-isEquivalence
          _◦_ = Lift _≈_ _∙_ M.sel f

        isMagma : IsMagma _≈′_ _◦_
        isMagma = record
          { isEquivalence = ≈′-isEquivalence
          ; ∙-cong        = cong (λ {x} → f-injective {x}) f-cong
          }

        isSemigroup : Associative _≈_ _∙_ → IsSemigroup _≈′_ _◦_
        isSemigroup ∙-assoc = record
          { isMagma = isMagma
          ; assoc   = assoc (λ {x} → f-injective {x}) ∙-assoc
          }

        isBand : Associative _≈_ _∙_ → IsBand _≈′_ _◦_
        isBand ∙-assoc = record
          { isSemigroup = isSemigroup ∙-assoc
          ; idem        = idem f E.reflexive
          }

        isSelectiveMagma : IsSelectiveMagma _≈′_ _◦_
        isSelectiveMagma = record
          { isMagma = isMagma
          ; sel     = sel f E.reflexive
          }

    ------------------------------------------------------------------------
    -- Other properties

      module _ {P : Pred A p} (f : A → B) where

        private
          _◦_ = Lift _≈_ _∙_ M.sel f

        preservesᵒ : (∀ {x y} → P x → (f x ∙ f y) ≈ f y → P y) →
                     (∀ {x y} → P y → (f x ∙ f y) ≈ f x → P x) →
                     ∀ x y → P x ⊎ P y → P (x ◦ y)
        preservesᵒ left right x y (inj₁ px) with M.sel (f x) (f y)
        ... | inj₁ _        = px
        ... | inj₂ fx∙fy≈fx = left px fx∙fy≈fx
        preservesᵒ left right x y (inj₂ py) with M.sel (f x) (f y)
        ... | inj₁ fx∙fy≈fy = right py fx∙fy≈fy
        ... | inj₂ _        = py

        preservesʳ : (∀ {x y} → P y → (f x ∙ f y) ≈ f x → P x) →
                     ∀ x {y} → P y → P (x ◦ y)
        preservesʳ right x {y} Py with M.sel (f x) (f y)
        ... | inj₁ fx∙fy≈fx = right Py fx∙fy≈fx
        ... | inj₂ fx∙fy≈fy = Py

        preservesᵇ : ∀ {x y} → P x → P y → P (x ◦ y)
        preservesᵇ {x} {y} Px Py with M.sel (f x) (f y)
        ... | inj₁ _ = Px
        ... | inj₂ _ = Py

        forcesᵇ : (∀ {x y} → P x → (f x ∙ f y) ≈ f x → P y) →
                  (∀ {x y} → P y → (f x ∙ f y) ≈ f y → P x) →
                  ∀ x y → P (x ◦ y) → P x × P y
        forcesᵇ presˡ presʳ x y P[x∙y] with M.sel (f x) (f y)
        ... | inj₁ fx∙fy≈fx = P[x∙y] , presˡ P[x∙y] fx∙fy≈fx
        ... | inj₂ fx∙fy≈fy = presʳ P[x∙y] fx∙fy≈fy , P[x∙y]