3 ms·
The same thing as far as I see.
by Kutta 10y ago
The same thing as far as I see.
- Chinjut 10y agoI concur.
- AnimalMuppet 10y agoSo when you said, "at the lowest level it's a collection of typing and computation rules which one can apply successively to do proofs and constructions", That was what Chinjut meant by "Homotopy Type Theory axiomatizes weak omega groupoids; it gives you formal rules you can manipulate to reason about weak omega groupoids"? That is, those lowest-level rules don't assume weak omega groupoids; they turn out to define weak omega groupoids?