# Category Archives: Univalence

## A new class of models for the univalence axiom

First of all, in case anyone missed it, Chris Kapulkin recently wrote a guest post at the n-category cafe summarizing the current state of the art regarding “homotopy type theory as the internal language of higher categories”. I’ve just posted … Continue reading

## Not every weakly constant function is conditionally constant

As discussed at length on the mailing list some time ago, there are several different things that one might mean by saying that a function is “constant”. Here is my preferred terminology: is constant if we have such that for … Continue reading

## Splitting Idempotents

A few days ago Martin Escardo asked me “Do idempotents split in HoTT”? This post is an answer to that question.

## Higher inductive-recursive univalence and type-directed definitions

In chapter 2 of the HoTT book, we prove theorems (or, in a couple of cases, assert axioms) characterizing the equality types of all the standard type formers. For instance, we have and (that’s function extensionality) and (that’s univalence). However, … Continue reading

## Eilenberg-MacLane Spaces in HoTT

For those of you who have been waiting with bated breath to find out what happened to your favorite characters after the end of Chapter 8 of the HoTT book, there is now a new installment: Eilenberg-MacLane Spaces in Homotopy Type Theory Dan … Continue reading

## Another proof that univalence implies function extensionality

The fact, due to Voevodsky, that univalence implies function extensionality, has always been a bit mysterious to me—the proofs that I have seen have all seemed a bit non-obvious, and I have trouble re-inventing or explaining them. Moreover, there are … Continue reading

## The HoTT Book

This posting is the official announcement of The HoTT Book, or more formally: Homotopy Type Theory: Univalent Foundations of Mathematics The Univalent Foundations Program, Institute for Advanced Study The book is the result of an amazing collaboration between virtually everyone involved … Continue reading

## Universe n is not an n-Type

Joint work with Christian Sattler Some time ago, at the UF Program in Princeton, I presented a proof that Universe n is not an n-type. We have now formalized that proof in Agda and want to present it here. One … Continue reading

## 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

## Isomorphism implies equality

Thierry Coquand and I have proved that, for a large class of algebraic structures, isomorphism implies equality (assuming univalence). A class of algebraic structures Structures in this class consist of a type, some operations on this type, and propositional axioms … Continue reading

## Modeling Univalence in Inverse Diagrams

I have just posted the following preprint, which presents new set-theoretic models of univalence in categories of simplicial diagrams over inverse categories (or, more generally, diagrams over inverse categories starting from any existing model of univalence). The univalence axiom for … Continue reading

## Modeling Univalence in Subtoposes

In my recent post at the n-Category Café, I described a notion of “higher modality” in type theory, which semantically ought to represent a left-exact-reflective sub–category of an -topos — once we can prove that homotopy type theory has models … Continue reading

## 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

## Oberwolfach Report

Richard Garner has now completed and posted the report from the Oberwolfach meeting.

## Function Extensionality from Univalence

Andrej Bauer and Peter Lumsdaine have worked out a proof of Function Extensionality from Univalence that is somewhat different from Vladimir Voevodsky’s original. In it, they identify and employ a very useful consequence of Univalence: induction along weak-equivalences. Andrej has … Continue reading