Logical systems. I: Internal calculi. (Q326587)

The article is the first in a series of three, the others not yet published at the time of writing this review. The purpose of these articles is to lay down a 2-categorical approach to logical systems. This paper, after introducing the necessary preliminaries, poses and answers two questions: {\parindent=0.7cm\begin{itemize}\item[(1)] what properties a 2-category must possess to allow establishing the connection among \(\lambda\)-calculus, logic, and categorical constructions which is usually referred to as the Curry-Howard isomorphism? \item[(2)] what can be gained by those properties? \end{itemize}} The key notion to answer the former question is \textit{discreteness}, Definition 1.2 in the paper. By cleverly using this notion, the author extends the definition of fibred/internal connectives and polymorphism to an arbitrary 2-category with a notion of discreteness. Also, the concept of internally closed connectives is analysed and an appropriate extension of the naive approach is proposed and justified. Then, a 2-functor realising any finitely complete 2-category \(\mathbb{C}\) with a notion of discreteness in the 2-category of the categories internal to discrete \(\mathbb{C}\)-objects is constructed so that the functor preserves internal connectives and polymorphic objects. This realisation maps \(\mathbb{C}\) to a full 2-subcategory if and only if the discrete objects are dense; it has a left adjoint if and only if \(\mathbb{C}\) has codescent objects of discrete truncated cosimplicial diagrams. Although very technical, these results generalise the more usual fibrational definitions when considered in the world of enriched categories. Another contribution of the paper is that it shows that, when a 2-category is sufficiently rich, then its objects cannot have all the internal products unless degenerate. This result generalises Freyd's theorem for categories internal to any tensored category. Finally, it is proved that an object in a Cartesian 2-category is linearly complete if and only if it is linearly cocomplete. A direct consequence is that a category internal to a locally Cartesian closed category, which is worth reminding, allows to interpret dependent type theory, is internally complete if and only if it is internally cocomplete. Despite the abundance of unavoidable technical concepts and proofs, this long and difficult article contains results, like the generalisation of Freyd's theorem, which are worth alone the reading. And the overall picture which emerges provides a satisfying answer to the second question posed in the introduction.