------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of a min operator derived from a spec over a total
-- preorder.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Construct.NaturalChoice.Base using (MinOperator)
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.Construct.NaturalChoice.MinOp minOp
open import Algebra.Lattice.Bundles using (Semilattice)
open import Algebra.Lattice.Structures _≈_
------------------------------------------------------------------------
-- Structures
⊓-isSemilattice : IsSemilattice _⊓_
⊓-isSemilattice = record
{ isBand = ⊓-isBand
; comm = ⊓-comm
}
------------------------------------------------------------------------
-- Bundles
⊓-semilattice : Semilattice _ _
⊓-semilattice = record
{ isSemilattice = ⊓-isSemilattice
}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4