------------------------------------------------------------------------
-- The Agda standard library
--
-- Instances of algebraic lattice structures where the carrier is ⊤.
-- In mathematics, this is usually called 0.
--
-- From monoids up, these are are zero-objects – i.e, both the initial
-- and the terminal object in the relevant category.
-- For structures without an identity element, we can't necessarily
-- produce a homomorphism out of 0, because there is an instance of such
-- a structure with an empty Carrier.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Level using (Level)
module Algebra.Lattice.Construct.Zero {c ℓ : Level} where
open import Algebra.Lattice.Bundles using (Semilattice)
open import Data.Unit.Polymorphic using (⊤)
------------------------------------------------------------------------
-- Bundles
semilattice : Semilattice c ℓ
semilattice = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
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