------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of a min operator derived from a spec over a total
-- preorder.
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
open import Algebra.Bundles
open import Algebra.Lattice.Bundles
open import Algebra.Construct.NaturalChoice.Base
open import Relation.Binary.Bundles using (TotalPreorder)
 
module Algebra.Lattice.Construct.NaturalChoice.MinOp
  {a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂} (minOp : MinOperator O) where
 
open TotalPreorder O
open MinOperator minOp
 
open import Algebra.Lattice.Structures _≈_
open import Algebra.Construct.NaturalChoice.MinOp minOp
 
------------------------------------------------------------------------
-- Structures
 
⊓-isSemilattice : IsSemilattice _⊓_
⊓-isSemilattice = record
  { isBand = ⊓-isBand
  ; comm   = ⊓-comm
  }
 
------------------------------------------------------------------------
-- Bundles
 
⊓-semilattice : Semilattice _ _
⊓-semilattice = record
  { isSemilattice = ⊓-isSemilattice
  }