Cubical Agda: a cold Introduction
Motivation
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".
Prerequisites
Non-cubical Agda (Vanilla Agda) experience
Lambda calculus basic concepts, such as currying
Primary school geometry (lines, squares, cubes)
Episodes
❒ Path and Intervals
❒ Squares and Diagonals
❒ Inductive Types with Path Constructors
❒ Open Squares can be Capped
❒ Ld Nclusion - η-rules and codata
License
This and the original version of this blog are licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.