Abstract
We describe a non-extensional variant of Martin-Löf type theory which we
call two-dimensional type theory, and equip it with a sound and complete
semantics valued in 2-categories.
Users
Please
log in to take part in the discussion (add own reviews or comments).