------------------------------------------------------------------------ -- 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 7 _∧_ infixr 6 _∨_ infix 4 _≈_ 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 (_≉_)