Joyal representation theorem for Heyting algebras
The classic Stone representation theorem states that every Boolean algebra embeds into the Boolean algebra of subsets of a set. We formalize the analogous Joyal representation theorem:
Theorem: Every Heyting algebra embeds into the Heyting algebra of lower sets of a partial order.
The theorem generalizes the Stone representation theorem and implies the Kripke completeness of intuitionistic propositional logic. (We do not formalize these facts.)
The formalization was done by Steve Awodey, Andrej Bauer and Mario Carneiro during the trimester Program “Prospects of Formal Mathematics“ at the Hausdorff Research Institute for Mathematics, funded by the Deutsche Forschungsgemeinschaft under Germany ́s Excellence Strategy – EXC-2047/1 – 390685813.