Consider lambda calculus as an equational theory. We start with beta-equality, and maybe also eta-equality, and then add additional [sets of] equations to form congruences. The set of congruences is closed under finite intersection and arbitrary union: it is a complete lattice.

The lattice of lambda theories is a well-studied structure. I will survey some known results regarding the lattice, and discuss some lattices of theories of extensions of lambda-calculus.

References: "Applying universal algebra to lambda calculus" by G Manzontetto and A. Salibra.