nLab realizability

Idea

The idea of realizability is a way of making the Brouwer-Heyting-Kolmogorov interpretation of constructivism and intuitionistic mathematics precise. It is related to the propositions as types paradigm. For instance, constructively a proof of an existential quantification $\underset{x\in X}{\exists} \phi(x)$ consists of constructing a specific $x \in X$ and a proof of $\phi(x)$, which “realizes” the truth of the statement, whence the name (see e.g. Streicher 07, section 1, Vermeeren 09, section 1 for introductions to the rough idea, or Bauer 05, page 12 and def. 4.7 for an actual definition).

Realizability of univalence in homotopy type theory

One possible way to find a computational interpretation for univalence in homotopy type theory is to interpret it in using realizability. Stekelburg provides a univalent universe of modest Kan complexes.

Simplicial homotopy theory can be developed in an extensive locally cartesian closed category $A$. Such categories are also called Heyting bialgebras?. The category $A$ has a class of small maps which has a bundle of small assemblies. This provides an internal Heyting bialgebra? $S$ which we can use as a target for simplicial `sets'. There is a (Kan-) model structure on these simplicial sets.

Within $S$ we can define a universe $M$ and show that it is fibrant. This universe is even univalent.

Now, the category of assemblies in number realizability provides such a Heyting bialgebra. The modest sets, a small internally complete full subcategory, provide the univalent universe. Note that modest sets are an impredicative universe. It models the calculus of constructions.

Related entries

• realizability topos

• realizability model

• realizability interpretation

• effective topos, Kleene-Vesley topos

• propositional axiom of choice

• Lifschitz realizability

computability

	type I computability	type II computability
typical domain	natural numbers $\mathbb{N}$	Baire space of infinite sequences $\mathbb{B} = \mathbb{N}^{\mathbb{N}}$
computable functions	partial recursive function	computable function (analysis)
type of computable mathematics	recursive mathematics	computable analysis, Type Two Theory of Effectivity
type of realizability	number realizability	function realizability
partial combinatory algebra	Kleene's first partial combinatory algebra	Kleene's second partial combinatory algebra

References

Realizability originates with the interpretation of intuitionistic number theory, later developed as Heyting arithmetic, in

• Stephen Kleene, On the interpretation of intuitionistic number theory Journal of Symbolic Logic, 10:109–124, 1945. link

A historical survey of realizability (including categorical realizability) is in

• Jaap van Oosten, Realizability: An Historical Essay, 2000 (link, pdf)

A quick survey is in

• Stijn Vermeeren, Realizability Toposes, 2009 (pdf)

being a summary of

• Martin Hyland, The effective topos, in The L.E.J. Brouwer Centenary

  Symposium (A. S. Toelstra and D. van Dalen, eds.), North-Holland Publishing Company, 1982, pp. 165–216

A modern textbook account is

• Jaap van Oosten, Realizability: an introduction to its categorical side, Studies in Logic and the Foundations of Mathematics, vol. 152, Elsevier, 2008 (preface pdf)

Lecture notes include

• Thomas Streicher, Realizability (2007/08) (pdf)

and

• Andrej Bauer, Realizability as connection between constructive and computable mathematics, in T. Grubba, P. Hertling, H. Tsuiki, and Klaus Weihrauch, (eds.) CCA 2005 - Second International Conference on Computability and Complexity in Analysis, August 25-29,2005, Kyoto, Japan, ser. Informatik Berichte, , vol. 326-7/2005. FernUniversität Hagen, Germany, 2005, pp. 378–379. (pdf)

based on

• Andrej Bauer, The Realizability Approach to

  Computable Analysis and Topology_, PhD thesis CMU (2000) (pdf)

• Peter Lietz, From Constructive Mathematics to Computable Analysis via the Realizability Interpretation (pdf.gz)

For realizability of univalent universes:

• Wouter Stekelenburg, Realizability of Univalence: Modest Kan complexes, arXiv

See also

• Steven Awodey, Andrej Bauer, Sheaf toposes for realizability (pdf)

• Wouter Pieter Stekelenburg, Realizability Categories, PhD thesis, Utrecht 2013 (arXiv:1301.2134)

• Martin Hyland, Variations on realizability: realizing the propositional axiom of choice, Mathematical Structures in Computer Science, Volume 12, Issue 3, June 2002, pp. 295 - 317 (doi:10.1017/S0960129502003651, pdf)