Motivating examples - Githubissues

mikeshulman / narya

A proof assistant for higher-dimensional type theory

GNU General Public License v3.0

146 stars 9 forks source link

Motivating examples #21

Open jfaure opened 2 months ago

jfaure commented 2 months ago

It would be valuable to demonstrate (even if not currently working):

Why OTT > MLTT, perhaps show how to leverage funext | transport | eliminate an observational equality in a setting that challenges MLTT
How OTT compares to Cubical (avoids book-keeping with pathtypes etc?)
What higher OTT unlocks
The README adjectives: 'Multi-Modal, Multi-Directional, Higher/Parametric/Displayed'
Where might OTT end up when narya releases: limitations and further directions to explore

mikeshulman commented 2 months ago

Right now, my priority is making the implementation work. For now, you can look at the slides and article available under the paper "Internal parametricity, without an interval" on my web site.