You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Is there a modern name for what Lambek and Scott call "intuitionistic type theory" (the internal language of topoi) in their book Introduction to higher order categorical logic? Today, I guess "intuitionistic type theory" tends to refer to Martin-Löf's dependent type theory instead.
Lambek and Scott's "intuitionistic type theory" has the type constructors "product" and "power object", and basic types for the terminal object, the NNO, and the subobject classifier, but it doesn't contain dependent types offhand.
I would handwavingly call that HOL (higher order logic)...
Thanks! I really like this name. But I would keep the adjective "intuitionistic". :-)
Yes, "IHOL" is quite common.
Thanks!
But how, then, would you talk about theories? Is "theory in intuitionistic higher-order logic" alright or is this the kind of situation in which one uses the word "doctrine" (theory in the doctrine of intuitionistic higher-order logic)?
I think either would be fine.
Thanks!