Logical systems I: Internal calculi

This is the first of a series of papers on a categorical approach to the logical systems. Its aim is to set forth the necessary foundations for more advanced concepts. The paper shows how the internal models of various lambda calculi arise in any 2-category with a notion of discreteness. We generalise to a 2-categorical setting two famous theorems: one saying that under some mild conditions, an object is internally complete iff it is internally cocomplete; and another saying that an object of a sufficiently cocomplete 2-category cannot be internally (co)complete unless it is degenerated. The first of the theorems specialises to a well-known fact from order theory, and also provides non-trivial results about posets and categories in constructive mathematics. Second of the theorems gives a powerful generalisation of Freyd's Theorem and sheds more light on the difficulty of finding fibrational models for higher polymorphism. As a simple corollary of this theorem, we obtain a variant of Freyd's Theorem for the categories internal to any tensored category. There is also a hidden objective of the paper — reading it backwards should provide a gentle introduction to the 2-categorical concepts through internal categories.