Publications, Lecture Notes and some Unpublished Notes

Publications

• Semantics of Type Theory.
  in the series Progress in Theoretical Computer Science. Basel: Birkhaeuser Verlag. XII, 298 p. (1991).

• Dependence and independence results for (impredicative) calculi of dependent types.
  Math. Struct. Comput. Sci. 2, No.1, 29-54 (1992).

• Independence of the induction principle and the axiom of choice in the pure calculus of constructions.
  Theor. Comput. Sci. 103, No.2, 395-408 (1992).

• A universality theorem for PCF with recursive types, parallel-or and $\exists$.
  Math. Struct. Comput. Sci. 4, No.1, 111-115 (1994).

• Investigations into Intensional Type Theory.
  This is a scanned version of my Habilitation Thesis from 1993. Here one can find models of intensional type theory refuting most of those judgements which trivially hold in extensional type theory but can't be proved in intensional type theory. In today's speak the most useful model (of Chapter 3) is obtained by glueing the global sections functor of the category of assemblies. pdf

• The groupoid interpretation of type theory
  with M. Hofmann
  in Sambin, Giovanni (ed.) et al., Twenty-five years of constructive type theory. Proceedings of a congress, Venice, Italy, October 19--21, 1995. Oxford: Clarendon Press. Oxf. Logic Guides. 36, 83-111 (1998). ps.gz

• Induction and recursion on the partial real line with applications to Real PCF.
  with M. Hoetzel Escardo
  Theor. Comput. Sci. 210, No.1, 121-157 (1999).

• Classical Logic, Continuation Semantics and Abstract Machines ps.gz.
  with Bernhard Reus.
  J. Funct. Program. 8, No.6, 543-572 (1998).

  We introduce a new continuation semantics inspired by a most simple double negation translation of classical to intuitionistic logic due to Krivine and Girard. From this continuation semantics we derive abstract environment machines for call-by-name lambda-calculus and Parigot's lambda-mu-calculus. Using a logical relations argument we prove the computational adequacy of these machines.

• Inductive Construction of Repletion ps.gz.
  Appl. Categ. Struct. 7, No.1-2, 185-207 (1999).

  In this paper one finds a logical (re)construction of the reflection to replete objects (as known from Synthetic Domain Theory) taking the form of an inductive definition within impredicative type theory.

• General Synthetic Domain Theory - A Logical Approach ps.gz.
  with Bernhard Reus.
  Math. Struct. Comput. Sci. 9, No.2, 177-223 (1999).

• Full Abstraction and Universality via Realisability ps.gz.
  with M. Marz and A. Rohr
  paper presented at LICS99 in Trento (1999).

  We describe realisability models for a functional core language that are fully abstract and universal, i.e. where all elements of data types appear as denotations of programs.

• Denotational Completeness Revisited ps.gz.
  paper presented at CTCS99 in Edinburgh (1999).

  We introduce a notion of Kripke Logical Relations for classical linear logic for the purpose of characterising those elements in a model which arise as interpretations of proofs.

• Impredicativity entails Untypedness ps.gz.
  with Peter Lietz
  to be published as part of the proceedings of the Trento Realizability Workshop (1999).

  We show that realizability models over a typed partial combinatory algebra (à la J. Longley) are impredicative, i.e. allow for quantification over predicates, if and only if the typed partial combinatory algebra is essentially untyped in the sense that it contains a universal type of which all other types appear as partial retracts. A consequence of our results is that the discrete separated objects of the modified realizability topos do not form a model of system F.

• Distribution Algebras and Duality .pdf.
  with M. Bunge, J. Funk and M. Jibladze.
  Advances in Mathematics 156, pp.133-156 (2000).

  The introduction, by Lawvere, of a notion of distribution on a topos E bounded over an elementary topos S, opened up a new area of research. We investigate here a lattice-theoretic notion of distribution algebra in E which is dual to that of a distribution on E. The main results of this paper are: (1) a relativized Pare-monadicity theorem relating the opposite of the category Dist-S(E) of distributions on E to the topos E under certain conditions satisfied by all Grothendieck toposes and by all essential localizations of internal presheaf toposes; (2) a characterization of distribution algebras as S-bicomplete S-atomic Heyting algebras in E and (3) an alternative (algebraic) characterization of the display locale of a distribution on E over S in terms of the frame of ideals of its corresponding distribution algebra.

• The Michael Completion of a Topos Spread .pdf.
  with M. Bunge, J. Funk and M. Jibladze.
  to appear in the Kelly Festschrift (JPAA 2002).

  We continue the investigation of the extension into the topos realm of the concepts introduced by R.H.Fox and E.Michael in connection with topological singular coverings. In particular, we construct an analogue of the Michael completion of a spread and compare it with the analogue of the Fox completion obtained earlier by the first two named authors. Two ingredients are present in our analysis of geometric morphisms between toposes bounded over a base topos S. The first is the nature of the domain of of the morphism, which need only be assumed to be a ``definable dominance'' over S, a condition that is trivially satisfied if the latter is a Boolean topos. The Heyting algebras arising from the object of truth values in the base topos play a special role in that they classify the definable monomorhisms in those toposes. The geometric morphisms which preserve these Heyting algebras (and that are not typically complete) are said to be strongly pure. The second is the nature of the geometric morphism itself, which is assumed to be some kind of a spread. Applied to a spread, the (strongly pure, weakly entire) factorization obtained here gives what we call the ``Michael completion'' of the given spread. Whereas the Fox complete spreads over a topos E correspond to the S-valued Lawvere distributions on S and relate to the distribution algebras, the Michael complete spreads seem to correspond to some sort of ``S-additive measures'' on E whose analysis we do not pursue here. We close the paper with several other open questions and directions for future work.

• In Domain Realizability, not all Functionals on C[-1,1] are Continuous .ps.gz
  with M. Escardo
  to appear in Mathematical Logic Quarterly.

  In the internal logic of the function realizability topos (i.e. over the second Kleene algebra) it holds that all functions between complete separable metric spaces (CSMs) are continuous. The purpose of this note is to show that this is not the case anymore for the domain realizability topos (i.e. over some universal Scott domain considered as a partial combinatory algebra) though this topos still validates the proposition stating that all functions between finite dimensional spaces are continuous. In particular, we show in this note that the domain realizability topos does not validate the proposition that all functionals on C[-1,1] are continuous.

• On the non-sequential nature of the interval-domain model of real-number computation .ps.gz
  with M. Escardo and M. Hofmann
  submitted to MSCS.

  We show that real-number computations in the interval-domain environment are ``inherently parallel'' in a precise mathematical sense. We do this by reducing the weak parallel-or operation on the Sierpinski domain to computations of the addition operation on the interval domain.

• Partial Toposes .pdf
  with J. Bénabou
  TAC No. 11, 309-320 (2003).

  We introduce various notions of partial topos, i.e. "topos without a terminal object". The strongest one, called local topos is motivated by the key examples of finite trees and sheaves with compact support. Local toposes satisfy all the usual exactness properties of toposes but are neither cartesian closed nor have a subobject classifier. Examples for the weaker notions are local homeomorphisms and discrete fibrations. Finally, for partial toposes with supports we show how they can be completed to toposes via an inverse limit construction.

• Quotients of countably based spaces are not closed under sobrification pdf
  with G. Gruenhage
  appeared in MSCS (2006).

  The notion of replete object was introduced by M. Hyland and P. Taylor around 1990 within Synthetic Domain Theory (SDT) in analogy with the sober spaces as known from topology. In this little note we show that for the realizability model over Scott's graph model and Kleene's function realizability model repletion is not given by sobrification. Thus there are replete objects which are not sober. Moreover, we show that a certain equalizer construction for repletion (as considered in the early days of SDT) fails to do its job.

• Universality results for models in locally boolean domains pdf
  with T. Loew
  appeared in the Proceedings of CSL 2006.

  It is shown that the locally boolean domains (invented by Jim Laird and equivalent to observably sequential algorithms) give rise to a universal model for infinitary SPCF and also for an infinitary untyped lambda calculus. More details can be found in the Thesis of Tobias Loew.

• Domain-Theoretic Foundations of Functional Programming.
  World Scientific, 132 p. (2006). See book for further information.

• Forcing for IZF in Sheaf Toposes pdf or pdf
  to appear in a Festschrift for Mamuka Jibladze published by Georgian Mathematical Journal.

  In the 1980s Fourman and Hayashi showed how to interpret IZF in Grothendieck toposes. D.Scott has given a forcing style reformulation of this interpretation for presheaf toposes. In this paper we extend this to arbitrary Grothendieck toposes.

• Krivine's Classical Realizability from a Categorical Perspective pdf
  submitted to Mathematical Structures in Computer Science

  In this paper we show how Krivine's Classical Realizability fits into the categorical approach to realizability as suggested by M. Hyland et.al. and as described in J. van Oosten's book (2009). It is not induced by a partial combinatory algebra but rather by a filtered order pca in the sense of Hofstra and van Oosten.
  Moreover, we give a precise characterisation when classical realizability coincides with Cohen forcing.

• Relative Completeness for Logics of Functional Programs pdf
  with B. Reus, Proceedings of CSL 2011

  In this paper we consider extensions of D. Scott's LCF which allow one to prove all true sentences holding in the Scott and the effective Scott model of PCF, respectively. We identify an effectively axiomatizable core to which we add the full first order theory of Baire space and full first order arithmetic, respectively, for achieving our goals.

  Finally we discuss how similar results may be obtained for other models of PCF like observably sequential algorithms or more refined games models.

• Realizability Models refuting Ishihara's Boundedness Principle pdf
  with P. Lietz

  This paper aims at giving a more readable account of a result in P. Lietz's Thesis which has received some attention among Bishop style constructivists. It is shown that in various realizability models of (extensional) Martin-Löf type theory Ishihara's Boundedness Principle for Numbers fails.

• A Model of Type Theory in Simplicial Sets pdf

  We give an introduction to Voevodsky's Homotopy Type Theory and present an alternative construction of a universe validating the Univalence Axiom.

• How Intensional is Homotopy Type Theory? pdf

  We give a simplified version of some model constructions of my Habilitation Thesis and discuss to which extent we can construct the groupoid model in type theory. Apparently, as first observed by Steve Awodey, one needs function extensionality for this purpose. We argue further that univalence boils down to function extensionality as long as one does not consider universes.

• A Classical Realizability Model arising from a Stable Model of Lambda Calculus pdf

  We consider classical realizability models arising from canonical domain models of lambda calculus with control. Using a theorem of A. Pitts we identify the subset of proof-like objects in such models. When starting from the canonical model in Scott domains the ensuing classical realizability model is equivalent to Set but when starting from the canonical model in stable domain theory the ensuing classical realizability topos is not of the Grothendieck kind and thus, in particular, not a forcing model. But we show that it validates the Countable Axiom of Choice using an argument which is an adaptation of an argument of Berger and Oliva in a different setting.

• Computability in Basic Quantum Mechanics pdf
  with E. Neumann and M. Pape

  We investigate to which extent the spaces used in basic quantum mechanics based on Hilbert space admit admissible reprsentations in the sense of Weihrauch's TTE and whether some interesting functions on them are computable in the sense of TTE. This is achieved by showing that they are definable in the internal languge of the so-called Kleene-Vesley topos and that the spaces of interest are S-extensional (where S is the Sierpinski space) which is tantamount to admitting an admissible representation. In particular, this way we prove that the spectral theorem for (bounded) self adjoint operators is actually computable. On the way we identify the natural topology induced by these representations on states, observables and spectral valuations (our replacement for projector-valued measures).

• Triposes as a Generalization of Localic Geometric Morphisms pdf
  with J. Frey (has appeared in the issue of MSCS devoted to the memory of Martin Hofmann)

  We show a generalized notion of tripos (due to A. Pitts) can be understood as a generalization of localic geometric morphisms. We show that non-equivalent triposes over the category of sets may induce the same topos. We leave it as an open question whether this is also the case also for the more restrictive class of traditional triposes as introduced in Hyland, Johnstone and Pitts seminal paper from 1980.

• An essential local geometric morphism which is not locally connected though its inverse image part defines an exponential ideal pdf
  with R. Garner

  Alas, it is not hyperconnected and thus leaves open the question raised by Lawvere and Menni in their 2015 TAC paper.

Theses of some of my Students

• B. Reus (PhD Thesis, 1995)
  "Program Verification in Synthetic Domain Theory" pdf.

  this Thesis was supervised by Martin Wirsing at LMU Munich. I had the pleasure to be an inofficial co-supervisor. Since Bernhard and I discussed a lot his research on SDT his Thesis is listed here. It was the starting point of some joyful cooperation of Bernhard and me.
  In his Thesis he gives an axiomatisation of SDT à la Scott within the extended calculus of constructions extended by a few axioms capturing the essence of SDT à la Scott. The whole development has been formally checked in the proof assistent LEGO thus constituting one of the major case studies in computer-assisted formalization of constructive mathematics.

• M. Marz (PhD Thesis, 2000)
  "A Fully Abstract Model for Sequential Computation" ps.gz.

  where he constructs a relational fully abstract model, the so--called sequential domains, for a functional language SFL with recursive types and all call-by-name and call-by-value type formers.

• G. Belger (Diploma Thesis, 2000)
  "The combinatory algebras U and A_wb,eff are not equivalent" ps.gz.

  showing that the two combinatory algebras mentioned in the title are not equivalent though they both give rise to universal realizability models of the prototypical functional language PCF. Whereas in the former model all PCF types are projective already type 2 is not projective in the latter model.

• A. Rohr (PhD Thesis, 2002)
  "A Universal Realizability Model for Sequential Computation" pdf.

  where he constructs a realizability model for a (call-by-name) sequential language FPC (with recursive types) that is universal in the sense that every object of the model arises as interpretation of some FPC program. Moreover, the constructed model is logically fully abstract in the sense of J. Longley, i.e. correctness statements about FPC programs hold in the model if and only if they are realized by an FPC program.

• P. Lietz (PhD Thesis, 2004)
  "From Constructive Mathematics to Computable Analysis via the Realizability Interpretation" pdf.

  where he shows (among other things) how function realizability (combined with truth) can be used for systematically turning results of constructive mathematics into corresponding results of computable analysis (in particular, of Weihrauch's Type Two Effectivity Approach).

• I. Battenfeld (Diploma Thesis, 2004)
  "A Category of Topological Predomains" ps.gz.

  where he gives explicit proofs for various claims made by A. Simpson in a paper from 2003. In particular, it is shown that the category of quotients of countably based spaces is equivalent to the extensional per's over the Scott/Plotkin graph model.

• T. Loew (PhD Thesis, 2006)
  "Locally Boolean Domains and Universal Models for Infinitary Sequential Languages" pdf.

  where he gives a detailed account of J. Laird's locally boolean domains and shows that they give rise to universal models for infinitary SPCF and an infinitary CPS target language. The latter is an infinitary untyped lambda calculus with an untrappable error element and the universal model for it is the least locally boolean domain D isomorphic to the domain of all maps from the countable product of D to the Sierpinski domain with just two elements.

• J. Frey (Diploma Thesis, 2007)
  "A Universal Characterisation of the Tripos-to-Topos Construction" pdf.

  where he shows that the tripos-to-topos construction is an appropriately lax left adjoint to te functor sending a topos to its subobject fibration.

• J. Weinberger (Master Thesis, 2016)
  "The Cubical Model of Type Theory" pdf.

  where he gives a purely categorical account of the model of cubical type theory as developed by Cohen, Coquand, Huber and Mörtberg in 2015.

Lecture Notes

• Allgemeine Algebra für Informatiker und Wirtschaftsinformatiker (in German language)ps.gz.

• Logik für Informatiker (in German language)ps.gz.

• Mathematik für Informatiker (in German language)pdf.

• Logik II (mainly in German language).

  Parts of a course on Computability Theory (pdf), Incompleteness of Formal Systems (pdf) and Basic Proof Theory (pdf)

• Einführung in die Axiomatische Mengenlehre (in German language)pdf.

  part of an introductory course in Mathematical Logic

• Introduction to Constructive Logic and Mathematics pdf

  lecture notes of a course I gave in winter term 2000/01

• Realizability pdf.

  lecture notes of a course I gave in winter term 2004/05

• Mathematical Foundations of Functional Programming

  lecture notes of a course I gave in winter term 2001/02

• Category Theory and Categorical Logic pdf.

  lecture notes for courses in summer term 2003 and winter term 2003/04

• Categorical Models of Constructive Logic pdf.

  Lecture notes of a course I gave in January '03 when invited by the group Logique de la Programmation in Luminy (Marseille). After introducing the notion of tripos (posetal hyperdoctrines for higher order constructive logic) we study the examples of Heyting-valued sets and realizability triposes and describe how triposes give rise to toposes.

• Fibered Categories à la Bénabou pdf.

  Revised notes of a course on fibered categories given at a spring school in Munich 1999. It introduces the main concepts of the Theory of Fibered Categories as developed by J. Bénabou for the purpose of "Category Theory over an Arbitrary Base (with pullbacks)". In particular we provide a fibrational explanation of geometric morphisms à la J.-L. Moens of which a preliminary version can be found in the Diploma Thesis of my student Peter Lietz.

• Distributors at Work pdf.

  Lecture notes of a course given by Jean Bénabou in June 2000 at TU Darmstadt about Distributors and Generalized Fibrations. Despite the introductory character of these lectures in the second half one finds quite a few elementary but not so well-known observations and facts (e.g. on the correspondence between distributors and comma/cocomma categories). The final section, in particular, contains a sketch of the theory of generalised fibrations starting from the fact that arbitrary functors to a category B correspond to normalised lax functors from the opposite of B to the bicategory Dist of distributors. The lecture notes are approved by the author.

Unpublished Notes

• A Fibrational View of Geometric Morphisms pdf.

  Here you can find some "meditations" about geometric morphisms as fibrations as pioneered by J.-L. Moens and on Bénabou's notion of partial topos.

• Lifting Grothendieck Universes pdf
  with M. Hofmann

  In this note we show how a Grothendieck universe can be "lifted" to a type theoretic universe within every topos of presheaves.

• A Topos for Computable Analysis ps.gz.

  In this short note I introduced a "topos for computable analysis" where maps are computable but act on types which in general contain non-computable elements. This is the situation considered e.g. by Pour-El and Richards in their well-known book. This topos was introduced independently at the same time by Dana Scott under the name "relative realizability topos" and studied in great detail by his student Lars Birkedal in his Thesis.

• LQD is Definable pdf
  with M. Jibladze

  In this short note we prove that for a bounded geometric morphism from E to S the fibration of maps which are locally quotients of discrete maps is a definable subfibration of the fundamental fibration of E.

• A Semantic Version of the Diller-Nahm Variant of Gödel's Dialectica Interpretation pdf.

  In this note we describe two triposes arising from the Diller-Nahm variant of Gödel's Dialectica interpretation and discuss its relation to the effective topos and the modified realizability topos. In an appendix we give a short description of related work by Birkedal and Rosolini.

• A Relational Characterisation of Syntactic Definability in Models of System F ps.gz.

  In this paper we extend Jung and Tiuryn's notion of Kripke logical relation for Henkin models of simply typed lambda calculus to categorical models of system F (polymorphic lambda calculus). We show that the syntactically definable elements of syntactic types are precisely the generalised elements invariant under all Kripke logical relations.

• Universes in Toposes pdf.

  In this note we discuss a notion of universes for elementary toposes which allows one to define sequences of sets by recursion, i.e. a concept which added to higher order arithmetic makes available the mathematically relevant part of the set-theoretic axiom of replacement. Though in general universes need not exist (as e.g. in the free topos with NNO) they do exist in realizability and sheaf toposes provided we assume a Grothendieck universe in the underlying category of sets.

• Realizability Models for CZF + Negation of Powerset Axiom pdf.

  In this note we show that V = (W A:U) A gives rise to a model of CZF validating the negation of the Powerset Axiom when U is interpreted as the type of modest sets within the category of assemblies over a (sufficiently small) partial combinatory algebra. In particular, for the first Kleene algebra (number realizability) the ensuing model validates the Axiom of Subcountability claiming that every set can be enumerated by a set of natural numbers. Finally we discuss the problems arising when trying to refute also the unrestricted Separation Scheme which when added to CZF (according to results of M. Rathjen) gives rise to a system of the same strength as 2nd order number theory.

• Shoenfield = Gödel o Krivine pdf.

  In this note together with Ulrich Kohlenbach we show that Shoenfield's functional interpretation for classical arithmetic (PA) can be obtained as a certain negative interpretation followed by Gödel's functional (Dialectica) interpretation. This negative translation is inspired by Krivine's negative translation for classical second order logic (inserting a negation in front of every prime formula) and was used by Streicher and Reus for the purpose of deriving Krivine's machine for call-by-name lambda calculus. Here we motivate it as an optimization of Kuroda's negative translation.

• The World's Simplest Proof of Moens's Lemma pdf.

  In this little note we give the simplest possible proof of Moens' Lemma characterizing those fibrations which arise as the Artin glueing of a finite limit preserving functor between categories with finite limits as fibrations of finite limit categories satisfying a fibrational version of Lawvere's extensivity property.

• Zawadowski's Cartesian Bifibrations pdf.

  We show that Marek Zawadowski's Cartesian Bifibrations coincide with Moens fibrations, i.e. fibrations of finite limit categories (over a base with finite limits) which has internal sums that are stable and disjoint.

• Semantics of Type Theory Formulated in Terms of Representability pdf.

  In this little note we discuss in which sense Awodey's recent "Natural Semantics of Type Theory" can be understood from a fibrational point of view recalling work by Giraud from the end of 1960s and work by Bénabou from around 2001/02. We describe a splitting of the fundamental fibration of a finite limit category as orginating from their work which we think is an attractive alternative to Awodey's account or rather provides an even more conceptual underpinning.

• Choice Sequences vs. Formal Topology pdf.

  This is the manuscript underlying my talk at Formal Topology 2015 where I describe the alternatives mentioned in the title. They are two different strategies dealing with the absence of non-effective objects in minimalist constructive mathematics. We believe that it is too cumbersome to develop basic analysis in a point-free way. Therefore, we prefer choice sequences. But we outline how a result of M. Fourman can be used for modelling the illusion(?) of points in a gros topos over separable locales with the open cover topology.

• The Witnessing Property fails for the Chambery Topos and a variant of it is not 2-valued pdf.

  Since the Chambery topos validates countable choice and Δ(2) is infinite its internal logic validates the proposition that there is a 1-1 map from the natural numbers into Δ(2). But this existential statement is not witnessed by a global element since we show that there is no monomorphism embedding the natural numbers objects of the Chambery topos into Δ(2). Finally, we show that when restricting proof-like terms to effective ones the ensuing classical realizability topos is not 2-valued.

• Observations on Fibered Toposes pdf.

  We show that a fibered topos has internal sums iff the fibration is a logical functor between toposes. From this it follows using an observation of Peter Johnstone that a topos is cocomplete iff freely adding small sums to it gives rise to a topos.

Recent Talks

• Categorical Intuitions Underlying Semantic Normalisation Proofs pdf.

  Abstract for a talk at a workshop on NbE in Aarhus 1998.

• A Universal Model for Infinitary CPS in Locally Boolean Domains ps.gz.

  Invited talk for CTCS'04 (August'04, Copenhaguen) based on joint work with my student Tobias Loew.

  It is shown how Dana Scott's inverse limit construction for models of untyped lambda calculus (from 1969) gives rise to a universal model for an infinitary CPS target language when preformed in the category of Locally Boolean Domains recently devised by Jim Laird as a purly denotational account of Curien-Lamarche games.

  A Realizability Model for CZF validating the Negation of the Powerset Axiom pdf.

  Invited talk for the meeting « Constructivisme et extraction de programmes » (Marseille, November'04) on occasion of a Honorary Doctorate given to Per Martin-Löf by the Université de la Méditerranée.

  We explain how to construct realizability models for IZF and CZF based on a method devised by Peter Aczel end of the 1970ies : if U is a (type-theoretic) universe then V = (WA:U) A gives rise to a model for CZF when interpreting logic via propositions-as-types. The latter validates the Axiom of Choice (in Martin-Löf type theory) which is intrinsic for showing that V validates the Collection and Subset Collection Axiom of CZF.

  In this talk we investigate what happens if logic is interpreted in a proof-irrelevant universe Prop of propositional types in which case AC does not holds anymore in general. We discuss principles (holding in realizability and sheaf models) that nevertheless allow one to show that V = (WA:U) A validates Collection and Subset Collection. This way we obtain a type-theoretic reformulation of Joyal and Moerdijk's Algebraic Set Theory (from 1995).

  Moreover, we show that when interpreting the universe U as the modest sets in a realizability model then the ensuing model V = (WA:U) A of CZF validates the negation of the Powerset Axiom. In case of number realizability V even validates the principle that all sets are subcountable, i.e. can be enumerated by a subset of the natural numbers.

  Identity Types and Weak Omega-Groupoids pdf.

  Talks in Uppsala (Nov. 2006) at a meeting on ``Identity Types - Topological and Categorical Structure''.

  In this talk we give a review of Identity types in Martin-Löf's Intensional Type Theory (ITT), recall our model in modified assemblies from 1993 and the groupoid model from 1994 (together with M. Hofmann). We argue why types in ITT should be considered as (internal) weak higher dimensional groupoids and discuss recent work of M. Warren implementing this idea, namely that Kan complexes and fibrations within the topos of simplicial sets give rise to a model of ITT where not all identity proofs are propositionally equal.

  Sheaf Models for CZF refuting Power Set and Full Separation pdf.

  Talk in Oberwolfach (April 2008) (joint work with Alex Simpson)

  We construct models for CZF refuting both the power set axiom and the full separation scheme in certain sheaf models, namely sheaves w.r.t. the countable cover topology on locally cartesian closed pretoposes with countable stable and disjoint sums.

  Fibered View of Geometric Morphisms pdf.

  Talk in Paris (June 2011) at the occasion of a Workshop in honour of Jean Bénabou

  We give a survey of work by Bénabou and Moens from the 1980s explaining in which sense geometric morphisms correspond to fibrations. At the end we describe how this allows one to view triposes as generalised localic geometric morphisms.

  Krivine's Classical Realizability from a Categorical Perspective pdf.

  invited talk in Marseille (July 2011) at TACL 2011

  After recalling Krivine's classical realizability we introduce the notion of an abstract Krivine structure (aks) and characterise those which correspond to Cohen forcing. We further show how every aks can be turned into a filtered order pca (in the sense of Hofstra and van Oosten) giving rise to a tripos which induces a Classical Realizability Topos by the well known tripos-to-topos construction. Finally we sketch how forcing can be done within classical realizability and how this 2 step construction can be contracted into one single classical realizability construction.

  Computability Theory for Quantum Theory pdf.

  talk at Logic Seminar Univ. Utrecht in July 2012.

  It is shown how Hilbert lattice, states and observables fit into function realizability corresponding to Weihrauch's Type Two Effectivity.

  Isomorphic Types are Equal! pdf.

  invited talk at MAP11 in Leiden (November 2011)

  This slogan is wrong in set-theoretic and type-theoretic foundations of mathematics. But it is consistent with Martin-Löf's intensional type theory. This was first observed to hold in the groupoid model of type theory. In this talk we present a model based on simplicial sets. We finish with a type-theoretic formulation of Voevodsky's Univalence Axiom which holds in this model. Besides validating the slogan in the title it is currently used for developing homotopy theory in a synthetic way within intensional type theory.

  Various Ways of Splitting Fibrations and Equality of Objects pdf.

  talk at Workshop on HoTT at DMV Tagung 2015 in Hamburg.

  We describe various ways of splitting fibrations as needed for semantics of type theory and discuss the role of equality of objects.

  Can one split dictoses? pdf.

  talk at the HoTT meeting at Max Planck Institute in Bonn in February 2016.

  Dictoses are a notion of model for Calculus of Constructions introduced by Thomas Ehrhard in the late 1980s. We describe how we are coming close to split dictoses in order to obtain models where syntax can actually be interpreted. The final obstacle also arises when trying so solve the problem for non-impredicative universes!

  How Unique are Ground Models? pdf.

  talk in Lyon at CHOCOLA meeting on 20. September 2018

  We reformulate tripos in terms of their associated constant object functors, i.e. as weakened localic geometric morphisms. We discuss whether for toposes induced by triposes ov the category of sets these triposes are unique up to equivalence. For a slightly weaker notion of tripos we answer the question negatively already for the category of sets itself.

  Simplicial Sets within Cubical Sets pdf.

  talk in Paris at PPS seminar on 27. September 2018

  We show how one can speak inside cubical sets about simplical sets thus providing a constructive treatment of the simplicial set model for HoTT.

  A "Geometric" View of Triposes pdf.

  talk at Xmas Seminar of Univ. Leicester Theory Group 15. December 2020

  We reformulate the notion of tripos due to Hyland, Johnstone and Pitts as a weakening of the notion of a localic geometric morphism.

  Precohesive Toposes over Arbitrary Base Toposes pdf.

  talk at a workshop on 19. Nov. 2021 at occasion of F. Marmolejo's 60th Birthday

  We explain why these are precisely the locally connnected geometric morphisms that are also local and hyperconnected. Locally connected means inverse image preserving dependent function spaces. At the end we discuss Menni's question whether it suffices to just require preservation of ordinary function spaces. We don't think so because the answer is negative if one drops the assumption of hyperconnectedness as shown in a recent paper with R. Garner. But, alas, for Menni's original question we still lack a counterexample. Still we believe the answer is negative since apparently preservation of dependent function spaces does not follow from preservation of ordinary function spaces unless we have classical logic available.

Some Unpublished Source Texts on Fibered Categories by Jean Bénabou and the Theses of Celeyrette and Moens FibCatTexts

---

Back to my homepage .