Is there a coordinated pair of names for the Boolean algebra arising as the double-negation retract of a Heyting algebra H, and that arising as the completion of H to a Boolean algebra? I've been thinking of them as the interior and exterior Boolean algebras of H, but if there's a pair of names already in use, either specifically for this situation or for a situation that this is an instance of, established notation would be preferable provided it isn't too much longer than interior and exterior. Actually I only care about complete Heyting algebras, in fact profinite distributive lattices, in case that makes any difference. The Boolean algebra completing a profinite distributive lattice is clearly a CABA; unless I'm overlooking something it looks like the double-negation retract should be the powerset of the set of maximal filters of H and so a CABA too. If so, is there some principle that shows that both Boolean algebras have to be CABAs without a separate argument for each, assuming H is profinite? A quick skim through the Handbook of Boolean Algebras, Sikorski, and the Elephant, didn't turn up anything, but these things are easy to miss when you don't have Google to search them. While I'm on the question of names, here's a really elementary question I don't know the answer to. How acceptable is it to write \sum_J:C^J\to C instead of Colim:C^J\to C when J is not discrete? Is \sum always understood to connote discrete sum or is the usage \sum_J excusable? Seems like context should make the meaning clear when J is a category. Vaughan Pratt