It is a basic fact that in a category with finite limits the following are equivalent

Each object $X$ has a (membership relation to a)

**power object**$PX\times X\hookleftarrow\ni_X$ subject to the universal property that every relation $Y\times X\hookleftarrow R$ is a pullback of the membership relation along a unique**characteristic morphism**$Y\times X\xrightarrow{f\times\mathrm{id}_X}PX\times X$.The category is

**cartesian closed**and has a**subobject classifier**$\Omega\hookleftarrow\top$ subject to the universal property that every monomorphism $Y\hookleftarrow m$ is a pullback of the subobject classifier along a unique**characteristic morphism**$Y\to\Omega$.

In the internal language of the category with finite limits, the notions in 2. correspond to **function types** and a **universe type**. I am looking for a reference for what type 1. corresponds to, and a proof of the equivalence of 1. and 2. using the internal language.

Lecture notes on Topoi and Quasitopoi(which is the only textbook I've found that doesn't relegate the proof to an exercise), but I was hoping the internal language formulation already exists in the literature somewhere. $\endgroup$ – Vladimir Sotirov Jul 20 '16 at 16:48