We apply some tools developed in categorical logic to give an abstract description of constructions used to formalize constructive mathematics in foundations based on intensional type theory. The key concept we employ is that of a Lawvere hyperdoctrine for which we describe a notion of quotient completion. That notion includes the exact completion on a category with weak finite limits as an instance as well as examples from type theory that fall apart from this.

We analyse the category-theoretical structures involved with the notion of continuity within the framework of formal topology. We compare the category of basic pairs to other categories of “spaces” by means of canonically determined functors and show how the definition of continuity is determined in a certain, canonical sense. Finally, we prove a standard adjunction between the algebraic approach to spaces and the category of topological spaces.

The standard presentation of topological spaces relies heavily on (naïve) set theory: a topology consists of a set of subsets of a set (of points). And many of the high-level tools of set theory are required to achieve just the basic results about topological spaces. Concentrating on the mathematical structures, category theory offers the possibility to look synthetically at the structure of continuous transformations between topological spaces addressing specifically how the fundamental notions of point and open come about. As a (...) byproduct of this, one may look at the different approaches to topology from an external perspective and compare them in a unified way. Technically, the category of sober topological spaces can be seen as consisting of (co)algebraic structures in the exact completion of the elementary category of sets and relations. Moreover, the same abstract construction of taking the exact completion, when applied to the category of topological spaces and continuous functions produces an extension of it which is cartesian closed. In other words, there is one general mathematical construction that, when applied to a very elementary category, generates the category of topological spaces and continuous functions, and when applied to that category produces a very suitable category where to deal with all sorts functions spaces. Yet, via such free constructions it is possible to give a new meaning to Marshall Stone’s dictum: “always topologize” as the category of sets and relations is the most natural way to give structure to logic and the category of topological spaces and continuous functions is obtained from it by a good mix of free – i.e. syntactic – constructions. (shrink)

Plotkin suggested using a polymorphic dual intuitionistic/linear type theory as a metalanguage for parametric polymorphism and recursion. In recent work the first two authors and R.L. Petersen have defined a notion of parametric LAPL-structure, which are models of image, in which one can reason using parametricity and, for example, solve a large class of domain equations, as suggested by Plotkin.In this paper, we show how an interpretation of a strict version of Bierman, Pitts and Russo’s language image into synthetic domain (...) theory presented by Simpson and Rosolini gives rise to a parametric LAPL-structure. This adds to the evidence that the notion of LAPL-structure is a general notion, suitable for treating many different parametric models, and it provides formal proofs of consequences of parametricity expected to hold for the interpretation. Finally, we show how these results, in combination with Rosolini and Simpson’s computational adequacy result, can be used to prove consequences of parametricity for image. In particular, we show that one can solve domain equations in image up to ground contextual equivalence. (shrink)