# Constructive and category-theoretic foundations of mathematics

Project leader

Co-Investigators

Funding source

Swedish Research Council - Vetenskapsrådet (VR) |

Project Details

Description

The research programme has as a long term goal to develop constructive systems and methods of logic, especiallly in model theory and category theory, for the use in metamathematics, and as foundational systems for mathematics. The present part of the project concentrates on two (related) topics: Develop constructive model theory with respect to set models by exploiting existing topos-theoretic completeness theorems and machinery. The primary approach is closely tied to the constructive redevelopment of topology in terms of point-free spaces in the form of locales. A long-standing research topic in locale theory is the sense and extent to which point set reasoning can be applied with respect to locales. In our setting, this opens up the possibility that the constructive logician can reason about models in the same way as the classical model theorist, as long as certain restrictions are observed. We aim to investigate this approach. We propose to develop the general theory of dependent type theories and their algebraic semantics. Syntactically, a type theory is specified by a dependent signature with bindings; over this, a well-ordered family of rules, expressed in the raw syntax over the signature (expressions that are syntactically well-formed, but not necessarily well-typed). The semantic counterparts are given by well-ordered cell complex presentations of suitable extensions of the essentially algebraic theory of categories with attributes. We expect to apply this framework on models of homotopy type theory.