Category Archives: Uncategorized

The 2nd International Conference on Homotopy Type Theory (HoTT 2023) will be held Monday 22nd May – Thursday 25th May 2023 at Carnegie Mellon University, Pittsburgh (USA).  Abstracts of no more than 2 pages should be submitted via Easychair, see the submissions … Continue reading →

Since being introduced to HoTT around 3 years ago, I have, like so many others before me, developed a healthy(?) obsession with the Brunerie number (i.e. the number such that , as defined in Guillaume Brunerie’s PhD thesis). Over the … Continue reading →

Video and lecture notes are now available for a series of talks that took place last month at the Logic and Higher Structures workshop at CIRM-Luminy with the following abstract: Many introductions to homotopy type theory and the univalence axiom … Continue reading →

The Department of Mathematics at Johns Hopkins University solicits applications for one two-year postdoctoral fellowship beginning Summer 2021 (with some flexibility in the start and end dates). The position is funded by the Army Research Office (ARO) through the Multidisciplinary … Continue reading →

When attempting to prove a theorem, not discussed in this post, I tried to give a certain set the structure of a group. After failing repeatedly, my proof attempts led me to consider a miniature version of the problem: can … Continue reading →

The Department of Mathematics at Johns Hopkins University solicits applications for one two-year postdoctoral fellowship beginning Summer 2021 (with some flexibility in the start and end dates). The position is funded by the Air Force Office of Scientific Research (AFOSR) … Continue reading →

Erik Palmgren, professor of Mathematical Logic at Stockholm University, passed away unexpectedly in November 2019. This conference will be an online workshop to remember and celebrate Erik’s life and work. There will be talks by Erik’s friends and colleagues, as … Continue reading →

I am going to teach HoTT/UF with Agda at the Midlands Graduate School in April, and I produced lecture notes that I thought may be of wider use and so I am advertising them here. The source files I used … Continue reading →

Last year I wrote a post about cubicaltt on this blog. Since then there have been a lot of exciting developments in the world of cubes. In particular there are now two cubical proof assistants that are currently being developed … Continue reading →

As some of you might remember, back in 2015 at the meeting of the german mathematical society in Hamburg, Urs Schreiber presented three problems or “exercises” as he called it back then. There is a page about that on the … Continue reading →

I have often seen competent mathematicians and logicians, outside our circle, making technically erroneous comments about the univalence axiom, in conversations, in talks, and even in public material, in journals or the web. For some time I was a bit … Continue reading →

https://www.ias.edu/news/2017/vladimir-voevodsky

Some months ago I gave a series of hands-on lectures on cubicaltt at Inria Sophia Antipolis that can be found at: https://github.com/mortberg/cubicaltt/tree/master/lectures The lectures cover the main features of the system and don’t assume any prior knowledge of Homotopy Type … Continue reading →

This post is to announce a new article that I recently uploaded to the arxiv: https://arxiv.org/abs/1701.07538 The main result of that article is a type theoretic replacement construction in a univalent universe that is closed under pushouts. Recall that in … Continue reading →

Almost at the top of the HoTT website are the words: “Homotopy Type Theory refers to a new interpretation of Martin-Löf’s system of intensional, constructive type theory into abstract homotopy theory.  ” I think it is time to change these words … Continue reading →

The intent of this post is to address certain misconceptions that I’ve noticed regarding the HoTT Book and its role in relation to HoTT. (At least, I consider them misconceptions.) Overall, I think the HoTT Book project has been successful … Continue reading →

In section 10.5 of the HoTT book, the cumulative hierarchy V is defined as a rather non-standard higher inductive type. We can then define a membership relation ∈ on this type, such that (V, ∈) satisfies most of the axioms … Continue reading →

This week at ICFP, Carlo will talk about our paper: Homotopical Patch Theory Carlo Angiuli, Ed Morehouse, Dan Licata, Robert Harper Homotopy type theory is an extension of Martin-Loef type theory, based on a correspondence with homotopy theory and higher category … Continue reading →

(guest post by Jesse McKeown) A short narative of a brief confusion, leading to yet-another-reason-to-think-about-univalence, after which the Author exposes his vaguer thinking to derision. The Back-story In the comments to Abstract Types with Isomorphic Types, Dan Licata mentioned O(bservational)TT, … Continue reading →

I recently had occasion to define the simplex category inside of type theory. For some reason, I decided to use an inductive definition of each type of simplicial operators , rather than defining them as order-preserving maps of finite totally … Continue reading →

Many updates have been made to the various other pages on the site: Code, Events, Links, People, References.  For example, there are several new items on models of the Univalence Axiom on the References page.

From a homotopical perspective, Coq’s built-in sort Prop is like an undecided voter, wooed by both the extensional and the intensional parties. Sometimes it leans one way, sometimes the other, at times flirting with inconsistency.

It’s amazing what you can find in the HoTT repository these days! I was browsing it the other week, looking up something quite different, when I came across a theorem in Funext.v (originally by Voevodsky) which answers, in a surprising … Continue reading →

I have adapted some basic HoTT theorems and proofs to prose form, in an attempt to better understand the results and their proofs. The Coq proof scripts often obscure details of the exposition, like the choice of fibration in an induction tactic, … Continue reading →

This post is to alert the members of the HoTT community to some exciting recent developments over at the n-Category Cafe. First, some background. Some of us (perhaps many) believe that HoTT should eventually be able to function as the … Continue reading →

From a homotopy theorist’s point of view, identity types and their connection to homotopy theory are perfectly natural: they are “path objects” in the category of types. However, from a type theorist’s point of view, they are somewhat more mysterious. … Continue reading →