------------------------------------------------------------------------ -- 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