Cosmoi of Internal Categories

An internal full subcategory of a cartesian closed category $\mathcal {A}$, is shown to give rise to a structure on the 2-category $Cat(\mathcal {A})$ of categories in $\mathcal {A}$ which introduces the notion of size into the analysis of categories in $\mathcal {A}$ and allows proofs by transcendental arguments. The relationship to the currently popular study of locally internal categories is examined. Internal full subcategories of locally presentable categories (in the sense of Gabriel-Ulmer) are studied in detail. An algorithm is developed for their construction and this is applied to the categories of double categories, triple categories, and so on.