Cubical Agda: a cold Introduction
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)
This and the original version of this blog are licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.