Category Archives: Programming

The HoTT Game

What is the HoTT Game? The Homotopy Type Theory (HoTT) Game is a project written by mathematicians for mathematicians interested in HoTT and no experience in proof verification, with the aim of introducing cubical agda as a tool for trying … Continue reading

Posted in Code, Programming, Publicity, Uncategorized | 12 Comments

Combinatorial Species and Finite Sets in HoTT

(Post by Brent Yorgey) My dissertation was on the topic of combinatorial species, and specifically on the idea of using species as a foundation for thinking about generalized notions of algebraic data types. (Species are sort of dual to containers; … Continue reading

The Lean Theorem Prover

Lean is a new player in the field of proof assistants for Homotopy Type Theory. It is being developed by Leonardo de Moura working at Microsoft Research, and it is still under active development for the foreseeable future. The code … Continue reading

Posted in Code, Higher Inductive Types, Programming | 48 Comments

Modules for Modalities

As defined in chapter 7 of the book, a modality is an operation on types that behaves somewhat like the n-truncation. Specifically, it consists of a collection of types, called the modal ones, together with a way to turn any … Continue reading

Posted in Code, Programming | 19 Comments

A Formalized Interpreter

I’d like to announce a result that might be interesting: an interpreter for a very small dependent type system in Coq, assuming uniqueness of identity proofs (UIP). Because it assumes UIP, it’s not immediately compatible with HoTT, but it seems … Continue reading

Posted in Code, Foundations, Programming | 77 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 | 9 Comments

Canonicity for 2-Dimensional Type Theory

A consequence of the univalence axiom is that isomorphic types are equivalent (propositionally equal), and therefore interchangable in any context (by the identity eliminaiton rule J). Type isomorphisms arise frequently in dependently typed programming, where types are often refined to … Continue reading

Posted in Foundations, Programming, Univalence | 8 Comments