Skip to content

Instantly share code, notes, and snippets.

wosc / Vagrantfile
Created December 18, 2018 19:52
Build unison-2.51.2 deb, compatible with the MacOS binary release
View Vagrantfile
Vagrant.configure("2") do |config|
config.vm.define "default" do |default|
default.vm.hostname = "unisonbuild"
default.vm.provider "lxc" = "zeitonline/bionic64-lxc"
# = "bento/ubuntu-18.04"
AndyShiue /
Last active November 7, 2023 11:00
Cubical type theory for dummies

I think I’ve figured out most parts of the cubical type theory papers; I’m going to take a shot to explain it informally in the format of Q&As. I prefer using syntax or terminologies that fit better rather than the more standard ones.

Q: What is cubical type theory?

A: It’s a type theory giving homotopy type theory its computational meaning.

Q: What is homotopy type theory then?

A: It’s traditional type theory (which refers to Martin-Löf type theory in this Q&A) augmented with higher inductive types and the univalence axiom.