Why cubical type theory, and why cubical Agda?
The discussion in this thread is going to be a bit technical in several fronts. Sorry.
I was meaning to write this for a while, but this discussion motivated me to write this now:
https://mathstodon.xyz/@agdakx@types.pl/109479087194839726
1/
There are two dimensions to various forms of type theory.
(1) Several type theories "compute" (e.g. Goedel's system T, various Martin-Loef type theories, calculus of (inductive) constructions, and more).
(2) Several type theories serve as languages to talk about mathematical objects we care about (e.g. 1-toposes, infinity-toposes).
2/
A good example of (2) is the Mitchell-Bénabou language of an elementary topos, developed in the early 1970's.
This is a kind of type theory specifically developed to talk about objects and morphisms of elementary toposes.
The things we wanted to talk about came first, and then a language was developed to talk about them.
3/
It was soon noticed that such a language is necessarily intuitionistic. Not because people wanted to fulfil 2/(1) above to "compute", but instead because this is the nature of toposes, independently of whether we want to compute with them or not.
Even if your meta-theory is classical, the Mitchell-Bénabou language of an elementary toposes is necessarily intuitionistic.
4/
This is not a philosophical choice. It is a mathematical necessity. It is unavoidable.
5/
Then, more recently, Voevodsky wanted to formalize his way of thinking about mathematical objects, based on homotopy theory, using computers.
After some experimentation, and based on knowledge of many others, he came across type theory.
In particular, he formulated the univalence axiom in order to capture certain ideas in homotopy theory.
And he gave a model of univalence in simplicial sets.
6/
Making a long story short, eventually the HoTT book was written.
There a Martin-Loef type theory is presented, with some additional axioms and constructions, such as univalence and higher-inductive types.
7/
Although Martin-Loef type theories were conceived to capture a notion of computation ("propositions as types" and "proofs as programs"), its extension with univalence was not.
In fact, originally Voevodsky said that his project was going to use choice and excluded middle, both of which are incompatible with computation (by 2017 in a meeting in the Newton Institute he had changed his mind).
8/
@MartinEscardo
(Tangentially, do you have a link handy on choice and LEM being incompatible with computation? Or is it just so obvious that I reveal the depths of my ignorance just by asking? 😁)
@ceoln Would saying that with excluded middle you can solve the Halting Problem convince you? If not I can say more.
