Category Archives: Uncategorized

The cumulative hierarchy of sets (guest post by Jeremy Ledent)

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

Posted in Uncategorized | 2 Comments

Homotopical Patch Theory

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

Posted in Uncategorized | 4 Comments

Homotopy Theory in Homotopy Type Theory: Introduction

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

Posted in Applications, Higher Inductive Types, Homotopy Theory, Uncategorized, Univalence | 3 Comments

On Heterogeneous Equality

(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

Posted in Uncategorized | 19 Comments

Abstract Types with Isomorphic Types

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

Posted in Programming, Uncategorized | 8 Comments

The Simplex Category

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

Posted in Uncategorized | Leave a comment

HoTT Updates

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.

Posted in Uncategorized | Leave a comment