# Category Archives: Code

## Colimits in HoTT

In this post, I would want to present you two things: the small library about colimits that I formalized in Coq, a construction of the image of a function as a colimit, which is essentially a sliced version of the … 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

## Constructing the Propositional Truncation using Nonrecursive HITs

In this post, I want to talk about a construction of the propositional truncation of an arbitrary type using only non-recursive HITs. The whole construction is formalized in the new proof assistant Lean, and available on Github. I’ll write another … Continue reading

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

## Double Groupoids and Crossed Modules in HoTT

The past eight months I spent at CMU for my master thesis project. I ended up formalizing some algebraic structures used in Ronald Brown’s book “Non-Abelian Algebraic Topology”: Double groupoids with thin structure and crossed modules over groupoids. As the … Continue reading

## Splitting Idempotents, II

I ended my last post about splitting idempotents with several open questions: If we have a map , a witness of idempotency , and a coherence datum , and we use them to split as in the previous post, do … 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.