------------------------------------------------------------------------
-- The Agda standard library
--
-- Definitions of 'raw' bundles
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Algebra.Lattice.Bundles.Raw where
 
open import Algebra.Core using (Op₂)
open import Algebra.Bundles.Raw using (RawMagma)
open import Level using (suc; _⊔_)
open import Relation.Binary.Core using (Rel)
 
record RawLattice c ℓ : Set (suc (c ⊔ ℓ)) where
  infixr  _∧_
  infixr  _∨_
  infix   _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∧_     : Op₂ Carrier
    _∨_     : Op₂ Carrier
 
  ∨-rawMagma : RawMagma c ℓ
  ∨-rawMagma = record { _≈_ = _≈_; _∙_ = _∨_ }
 
  ∧-rawMagma : RawMagma c ℓ
  ∧-rawMagma = record { _≈_ = _≈_; _∙_ = _∧_ }
 
  open RawMagma ∨-rawMagma public
    using (_≉_)