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