------------------------------------------------------------------------ -- The Agda standard library -- -- Some derivable properties ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} open import Algebra.Lattice.Bundles using (DistributiveLattice) module Algebra.Lattice.Properties.DistributiveLattice {dl₁ dl₂} (DL : DistributiveLattice dl₁ dl₂) where import Algebra.Lattice.Properties.Lattice as LatticeProperties open DistributiveLattice DL open import Algebra.Definitions _≈_ open import Algebra.Lattice.Structures _≈_ open import Relation.Binary.Reasoning.Setoid setoid ------------------------------------------------------------------------ -- Export properties of lattices open LatticeProperties lattice public ------------------------------------------------------------------------ -- The dual construction is also a distributive lattice. ∧-∨-isDistributiveLattice : IsDistributiveLattice _∧_ _∨_ ∧-∨-isDistributiveLattice = record { isLattice = ∧-∨-isLattice ; ∨-distrib-∧ = ∧-distrib-∨ ; ∧-distrib-∨ = ∨-distrib-∧ } ∧-∨-distributiveLattice : DistributiveLattice _ _ ∧-∨-distributiveLattice = record { isDistributiveLattice = ∧-∨-isDistributiveLattice }