ABSTRACT. A major turning point in constructive mathematics was Bishop’s publication of Foundations of Constructive Analysis in 1967. The early 1970s saw the development of several foundational frameworks for constructive mathematics that were to no small extent galvanized by Bishop’s work, notably Myhill’s Constructive Set Theory, Feferman’s Explicit Mathematics and Martin-Löf’s Type Theory. Myhill wanted to single out principles undergirding Bishop’s mathematics with the additional aim of making “the process of formalization completely trivial, as it is in the classical case”. Albeit constructivism and set theory are sometimes depicted as antipodes, Peter Aczel showed that Myhill’s intuitionistic set theory has a canonical interpretation in Martin-Löf type theory. He also found several new set-theoretic principles (especially choice principles) validated by this interpretation.

This talk will describe the set theory resulting from Aczel’s interpretation in MLTT. It will also consider how the interpretation panes out when the interpreting theory is taken to be homotopy type theory, and what kind of set theory one obtains if one allows certain omniscience principles (as Bishop called them) to reign.

ABSTRACT. Since around 1998, Peter Aczel became deeply interested in understanding and relating the different ways in which logic can be treated in type theory (such as the propositionsas-types paradigm or the propositions-as-elements-of-Prop idea). The motivation came from multiple angles, including experience with computer-assisted proof-checking, the typetheoretic intepretation of Constructive Set Theory, developments in Categorical Logic, and the desire to understand better fully impredicative logical systems.

This work eventually led to the proof of numerous important results and the introduction of Russell-Prawitz modalities and of logic-enriched type theories. In this talk, I will survey this part of Peter Aczel’s research and its influence on subsequent developments, such as Homotopy Type Theory.

ABSTRACT. We compare two semantics for type theory: comprehension categories, which closely follow the syntax and intricacies of type theory, and path categories, which are relatively simple structures that take inspiration from homotopy theory. Both are only semantics in a weak way because they only specify substitutions up to isomorphism. However, it is known that the class of comprehension categories enjoys coherence: we can turn comprehension categories into actual models by ‘splitting’ them. We show that this can also be done for path categories by proving an equivalence between path categories and certain comprehension categories.

ABSTRACT. In categorical logic, indexed preorders are an interpretation of many-sorted predicate logic. In view that many-sorted predicate logic is a (extremely) truncated version of dependent type theory, we consider an adaptation of the inductive axioms of identity types in the setting of indexed preorders, called identity objects. This Martin-Löf notion of equality turns out, perhaps as expected, to be equivalent to Lawvere's equality as extracted by Maietti and Rosolini in the notion of elementary doctrines. This allows us to render Pasquali's 'elementary completion' result as saying that its underlying equivalence relations construction is a right-biadjoint completion of suitable indexed preorders with respect to identity objects.

We produce an analogue of this result for the PERs construction, the partial equivalence relations version of the equivalence relations construction, which serves as a key factor of the tripos-to-topos construction as well as of the PER model in programming language semantics. More specifically, we consider a suitable variation of the notion of identity objects, called partial identity objects, and show that the PERs construction is a right-biadjoint completion of suitable indexed preorders with respect to partial identity objects.

ABSTRACT. The goal of this work is to give examples of partial combinatory algebras in cartesian restriction categories of groupoids with a view to constructing realizability models of intensional type theory.

ABSTRACT. We describe a directed homotopy type theory with semantics in 1-categories. We build on Martin-Löf type theory, adding annotations that we call orientations -- to capture co-, contra-, and isovariance -- and a hom type former -- to capture the directed identities.