Publications, Lecture Notes and some Unpublished Notes
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
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.
- 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).
- 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
- 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
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
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).
for further information.
- Forcing for IZF in Sheaf Toposes 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
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 Untyped 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.
Theses of some of my Students
- B. Reus (PhD Thesis, 1995)
"Program Verification in Synthetic Domain Theory" pdf.gz.
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 Awb,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.
(PhD Thesis, 2004)
"From Constructive Mathematics to Computable Analysis
via the Realizability Interpretation" pdf.gz.
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.gz.
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
- J. Frey (Diploma Thesis, 2007)
"A Universal Characterisation of the Tripos-to-Topos
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.
- Allgemeine Algebra für Informatiker und
Wirtschaftsinformatiker (in German language)ps.gz.
- Logik für Informatiker (in German language)ps.gz.
- Logik II (mainly in German language).
Parts of a course on Computability Theory
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
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.
- Fibred Categories à la Bénabou pdf.
Revised notes of a course on fibred categories given at a spring school
in Munich 1999. It introduces the main concepts of the Theory of Fibred
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.
- 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
- 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
- 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 ps.gz.
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.gz.
- 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
- Sheaf Models for CZF refuting Power Set and Full Separation pdf.gz.
- 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
Besides validating the slogan in the title it is currently used for developing
homotopy theory in a synthetic way within intensional type theory.