Synthetic topos theory
[004L] Exercise

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.