Category Archives: Uncategorized

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

Univalence versus Extraction

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.

Posted in Uncategorized | 18 Comments

Strong functional extensionality from weak

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

Posted in Uncategorized | 5 Comments

HoTT in prose

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

Posted in Uncategorized | 13 Comments