    ------------------------------------------------------------------------
    -- 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 = ⊤ ; _≈_ = λ _ _ → ⊤ }