This is a living document. Everything in this document is made in good faith of being accurate, but like I just said; we don't yet know everything about what's going on.
On March 29th, 2024, a backdoor was discovered in xz-utils, a suite of software that
| Vagrant.configure("2") do |config| | |
| config.vm.define "default" do |default| | |
| default.vm.hostname = "unisonbuild" | |
| default.vm.provider "lxc" | |
| default.vm.box = "zeitonline/bionic64-lxc" | |
| # default.vm.box = "bento/ubuntu-18.04" | |
| end | |
| end |
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.
