#Contents# * table of contents {:toc} ## Definition ## A __Heyting algebra__ is a [[distributive lattice]] $(L, \leq, \bot, \vee, \top, \wedge)$ with * a function $\implies: L \times L to L$ * a family of dependent terms $$a:L, b:L \vdash (b \to a) \wedge a \leq b$$ * a family of dependent terms $$a:L, b:L \vdash a \leq b \to (a \wedge b)$$ representing the carteisan closed condition for the lattice. ## See also ## * [[distributive lattice]] * [[locally Heyting-algebraic 2-poset]] * [[Heyting dagger 2-poset]]