A RetroSearch Logo

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Search Query:

Showing content from https://agda.github.io/agda-stdlib/master/Algebra.Lattice.Construct.NaturalChoice.MaxOp.html below:

Algebra.Lattice.Construct.NaturalChoice.MaxOp

Algebra.Lattice.Construct.NaturalChoice.MaxOp
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of a max operator derived from a spec over a total
-- preorder.
------------------------------------------------------------------------

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

open import Algebra.Construct.NaturalChoice.Base
  using (MaxOperator; MaxOp⇒MinOp)
open import Relation.Binary.Bundles using (TotalPreorder)

module Algebra.Lattice.Construct.NaturalChoice.MaxOp
  {a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂} (maxOp : MaxOperator O)
  where

import Algebra.Lattice.Construct.NaturalChoice.MinOp as MinOp

private
  module Min = MinOp (MaxOp⇒MinOp maxOp)

open Min public
  using ()
  renaming
  ( ⊓-isSemilattice           to  ⊔-isSemilattice
  ; ⊓-semilattice             to  ⊔-semilattice
  )

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