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

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

module Algebra.Lattice.Construct.LiftedChoice where

open import Algebra
  using (Op₂; IsSelectiveMagma; Associative; Commutative)
open import Algebra.Lattice.Structures using (IsSemilattice)
open import Algebra.Construct.LiftedChoice using (Lift; isBand; comm)
open import Relation.Binary.Core using (Rel; _Preserves_⟶_)
open import Relation.Binary.Structures using (IsEquivalence)
open import Level using (Level)

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

------------------------------------------------------------------------
-- Structures

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

  open IsSelectiveMagma ∙-isSelectiveMagma renaming (sel to ∙-sel)

  private
    _◦_ = Lift _≈_ _∙_ ∙-sel f

  isSemilattice : Associative _≈_ _∙_ → Commutative _≈_ _∙_ →
                  IsSemilattice _≈′_ _◦_
  isSemilattice ∙-assoc ∙-comm = record
    { isBand = isBand ∙-isSelectiveMagma f-injective f-cong ≈′-isEquivalence ∙-assoc
    ; comm   = comm   ∙-isSelectiveMagma (λ {x} → f-injective {x}) ∙-comm
    }