#Contents# * table of contents {:toc} ## Definition ## A __distributive lattice__ is a [[lattice]] $(L, \leq, \bot, \vee, \top, \wedge)$ with * a family of dependent terms $$a:L, b:L, c: L \vdash a \wedge (b \vee c) = (a \wedge b) \vee (a \wedge c)$$ representing the distributive property for the lattice. ## See also ## * [[lattice]] * [[sigma-frame]] * [[Heyting algebra]] * [[coherent dagger 2-poset]] ## References ## * Alex Simpson, [Measure, randomness and sublocales](https://www.sciencedirect.com/science/article/pii/S0168007211001874).