# Internal language type of power objects

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

1. 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$.

2. 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.

• Have you looked at Lambek & Scott's Introduction to higher-order categorical logic? Jun 1 '16 at 17:12
• @Andrej They do answer my first question: power type is the function type with codomain the subobject classifier. But they don't answer my second, unless I've misunderstood Sections 11 in Part II, where they show that the subcategory of functions in the allegory of relations generated from a type theory with power objects is cartesian closed. Furthermore, they disappointingly leave the actual checking of the universal properties to the reader, which is what I want to see done in the internal language, not just the definitions. Jul 20 '16 at 16:45
• I am tempted to write up the internal logic proof myself based on the categorical proof in Oswald Wyler's 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. Jul 20 '16 at 16:48