Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
starting this article based upon a suggestion by Mike Shulman on the discussion thread for extensional type theory, that from now on “extensional” should only be used for definitionally extensional type theories on the nLab
Anonymous
Is cubical type theory with equality reflection a thing? I mean, I suppose one could write it down, but has anyone done it?
The authors of A Cubical Language for Bishop Sets briefly mentioned the possibility of adding an equality reflection rule to their cubical type theory in section 8.2 of their article.
Added list of set-level intensional type theories, taken from extensional type theory.
1 to 5 of 5