Cubical Agda: a cold Introduction

Tesla (Yinsen) Ice Zhang, [CC BY-NC-ND 4.0]


I'm planning to write a series of introduction to the Cubical Type Theory, using the Agda proof assistant. My motivation was that existing Cubical Type Theory (and Cubical Agda) tutorials are all impossible to read unless you know Homotopy Type Theory. However, I still believe it's possible to learn Cubical Type Theory without HoTT background -- the only thing we need is someone who knows Cubical to write an introduction.

I have participated the summer school of HoTT 2019, and have solved most of my confusions in the Cubical methods lectures by Anders Mortberg. I feel like it's time for me to be the Cubical person, to write a really readable introduction to the Cubical Type Theory.

As this introduction is "not HoTT", it should be "cold". Thus "cold introduction".


  • Non-cubical Agda (Vanilla Agda) experience

  • Lambda calculus basic concepts, such as currying

  • Primary school geometry (lines, squares, cubes)


Path and Intervals

Squares and Diagonals

Inductive Types with Path Constructors

Open Squares can be Capped

Ld Nclusion - η-rules and codata


This and the original version of this blog are licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.