Remember Me
Or use your Academic/Social account:


Or use your Academic/Social account:


You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.


Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message


Verify Password:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Kraus, Nicolai (2015)
Languages: English
Types: Unknown
Homotopy type theory (HoTT) is a branch of mathematics that combines and benefits from a variety of fields, most importantly homotopy theory, higher dimensional category theory, and, of course, type theory. We present several original results in homotopy type theory which are related to the truncation level of types, a concept due to Voevodsky. \ud \ud To begin, we give a few simple criteria for determining whether a type is 0-truncated (a set), inspired by a well-known theorem by Hedberg, and these criteria are then generalised to arbitrary n. This naturally leads to a discussion of functions that are weakly constant, i.e. map any two inputs to equal outputs. \ud A weakly constant function does in general not factor through the propositional truncation of its domain, something that one could expect if the function really did not depend on its input. However, the factorisation is always possible for weakly constant endofunctions, which makes it possible to define a propositional notion of anonymous existence. We additionally find a few other non-trivial special cases in which the factorisation works. Further, we present a couple of constructions which are only possible with the judgmental computation rule for the truncation. Among these is an invertibility puzzle that seemingly inverts the canonical map from Nat to the truncation of Nat, which is perhaps surprising as the latter type is equivalent to the unit type.\ud \ud A further result is the construction of strict n-types in Martin-Lof type theory with a hierarchy of univalent universes (and without higher inductive types), and a proof that the universe U(n) is not n-truncated. This solves a hitherto open problem of the 2012/13 special year program on Univalent Foundations at the Institute for Advanced Study (Princeton).\ud \ud The main result of this thesis is a generalised universal property of the propositional truncation, using a construction of coherently constant functions. We show that the type of such coherently constant functions between types A and B, which can be seen as the type of natural transformations between two diagrams over the simplex category without degeneracies (i.e. finite non-empty sets and strictly increasing functions), is equivalent to the type of functions with the truncation of A as domain and B as codomain. In the general case, the definition of natural transformations between such diagrams requires an infinite tower of conditions, which exists if the type theory has Reedy limits of diagrams over the ordinal omega. If B is an n-type for some given finite n, (non-trivial) Reedy limits are unnecessary, allowing us to construct functions from the truncation of A to B in homotopy type theory without further assumptions.\ud To obtain these results, we develop some theory on equality diagrams, especially equality semi-simplicial types. In particular, we show that the semi-simplicial equality type over any type satisfies the Kan condition, which can be seen as the simplicial version of the fundamental result by Lumsdaine, and by van den Berg and Garner, that types are weak omega-groupoids.\ud \ud Finally, we present some results related to formalisations of infinite structures that seem to be impossible to express internally. To give an example, we show how the simplex category can be implemented so that the categorical laws hold strictly. In the presence of very dependent types, we speculate that this makes the Reedy approach for the famous open problem of defining semi-simplicial types work.
  • The results below are discovered through our pilot algorithms. Let us know how we are doing!

    • Martín Escardó and Paulo Oliva. Searchable sets, Dubuc-Penon compactness, omniscience principles, and the drinker paradox. Computability in Europe 2010, Abstract and Handout Booklet. 2010, pp. 168- 177 (cited on p. 5).
    • Martín Escardó. Constructive decidability of classical continuity. Mathematical Structures in Computer Science FirstView, February 2015, pp. 1-12. issn: 1469-8072 (cited on p. 5).
    • Draft paper. March 2015 (cited on p. 5).
    • Andrey Kolmogorov. Zur Deutung der intuitionistischen Logik. Mathematische Zeitschrift 35, 1932, pp. 58-65 (cited on p. 18).
    • Jacob Lurie. Higher topos theory. Vol. 170. Annals of Mathematics Studies. Princeton, NJ: Princeton University Press, 2009. isbn: 978- 0-691-14049-0; 0-691-14049-9 (cited on p. 117).
    • Matt Oliveri. A formalized interpreter. Blog post at homotopytypetheory.org. 19th August 2014 (cited on pp. 117, 170).
    • Erik Palmgren. Proof-relevance of families of setoids and identity in type theory. Arch. Math. Log. 51.1-2, 2012, pp. 35-47 (cited on p. 48).
  • No related research data.
  • No similar publications.
  • BioEntity Site Name

Share - Bookmark

Cite this article