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.



Constructive lattice completion
Joseph Van Name’s answer is correct for the general case. However, the OP indicated in comments that they are interested in the case where $L$ is a Heyting algebra, and then it turns out that the Dedekind–MacNeille completion *can* be constructed by taking the set of complete ideals of $L$ ordered by inclusion. (I’m frankly quite surprised, since for Heyting algebras, typically ideals are broken, and what works are filters. But here it seems to be the opposite.)


Using the notation in Joseph Van Name’s answer, it suffices to show that if $I\subseteq L$ is a complete ideal, and $a\in{\downarrow\uparrow}I$, then $a\in I$. Now, if $c\in L$ is any element such that $a\land b\le c$ for all $b\in I$, then $a\to c\in{\uparrow}I$, hence $a\le a\to c$, i.e., $a\le c$. Thus, we have established
$$a=\bigvee\{a\land b:b\in I\}=\bigvee\{b\in I:b\le a\}.$$
Since $I$ is a complete ideal, it follows that $a\in I$.


It is also easy to check that the Dedekind–MacNeille completion of $L$ is a Heyting algebra, with relative pseudocomplement operation (extending that of $L$) defined for complete ideals $I$, $J$ by
$$I\to J=\{a\in L:I\cap{\downarrow}a\subseteq J\}.$$
In particular, $I\to J$ is itself a complete ideal: if $a=\bigvee\_ia\_i$ with $a\_i\in I\to J$, and $b\in I\cap{\downarrow}a$, then $b\land a\_i\in J$ for each $i$, and $b=\bigvee\_i(b\land a\_i)$, hence $b\in J$.


