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.
I am taking the liberty of renaming the entry from “left division” to “left division in modal type theory”. (Since “left division” has a standard meaning in non-commutative algebra, which is not what is meant here. )
Similarly, where the entry requested a link for “[[rules]]
” I made it more specifically read “inference rules”, as there are other kinds of rules in mathematics. (For the time being this link is redirecting to sequent calculus, but that may change once somebody has the energy to split off an article dedicated to inference rules).
What’s the origin of the notion of “left division in type theory”? Nuyts (2020) suggests (on p. 133) that it goes way back to Pfenning 2001 and then Abel 2006, 2008.
1 to 3 of 3