Category Archives: Uncategorized
Last call for submissions INTERNATIONAL CONFERENCE AND SUMMER SCHOOL ON HOMOTOPY TYPE THEORY 12-17 August 2019 Carnegie Mellon University, Pittsburgh USA https://hott.github.io/HoTT-2019 Submission of talks and registration are open for the International Homotopy Type Theory conference (HoTT 2019), to be … 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
I recently completed my master’s thesis under the supervision of Steve Awodey and Jonas Frey. A copy can be found here. Known impredicative encodings of various inductive types in System F, such as the type of natural numbers do not … Continue reading
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
From June 4 — 10, 2017, there will be a workshop on homotopy type theory as one of the AMS’s Mathematical Research Communities (MRCs).
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
Many of us working on homotopy type theory believe that it will be a better framework for doing math, and in particular computer-checked math, than set theory or classical higher-order logic or non-univalent type theory. One reason we believe this … 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
Here’s a cute little example of programming in HoTT that I worked out for a recent talk. Abstract Types One of the main ideas used to structure large programs is abstract types. You give a specification for a component, and … 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