The Dedekind–MacNeille Completion is the generalized way of completing an arbitrary lattice $L$. We will call $C$ the Dedekind–MacNeille completion of $L$ (I will not go into the details of the Completion but see the comment below.) The completion includes an embedding $i: L \to C$ which preserves existing arbitrary meets and joins. The completion is universal in the sense that for any other complete lattice $C'$ and map $f: L \to C'$ that preserves arbitrary meets and joins there exists a unique map $g: C \to C'$ which preserves arbitrary meets and joins such that $f = g \circ i$. (I'm still learning category theory so please let me know if any of the above is incorrect.)

I have found an alternative completion specifically for Heyting algebras, which instead of considering the powerset of a Heyting algebra $H$ only considers the subsets of $H$ which are called complete ideals. Which are essentially ideals that additionally contain the join of any subset of the ideal, if that join exists. This completion must be equivalent to the Dedekind–MacNeille Completion by the universal property, right?

This is of interest to me because I want to peform a completion in a setting that does not have access to the powerset axiom (particularly CZF). The standard approach is to develop lattice theory for classes and give up the fact that the completion of an arbitrary lattice is provably a set. Before I pursue this I want to tie up this loose end in my mind. Because initially I was under the impression that I may be able to collect the complete ideals into a set without use of the powerset axiom, but that seems to not be the case.

4more comments