Let \(T\) be a base type theory. We work in \(T\). Then the function \(X\mapsto \mathord {\textnormal {\textsf {m}}}_{X}:\mathord {\textnormal {\textsf {SubTop}}}\rightarrow \mathord {\textnormal {\textsf {LAM}}}\) is an equivalence.
Let \(T\) be a base type theory. We work in \(T\). Then the function \(X\mapsto \mathord {\textnormal {\textsf {m}}}_{X}:\mathord {\textnormal {\textsf {SubTop}}}\rightarrow \mathord {\textnormal {\textsf {LAM}}}\) is an equivalence.