Category Theory
Zulip Server
Archive

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.

Stream: theory: type theory & logic

Topic: "Intuitionistic type theory"

Leopold Schlicht (May 03 2021 at 14:03):

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.

Kenji Maillard (May 03 2021 at 14:08):

I would handwavingly call that HOL (higher order logic)...

Leopold Schlicht (May 03 2021 at 14:35):

Thanks! I really like this name. But I would keep the adjective "intuitionistic". :-)

Mike Shulman (May 03 2021 at 14:42):

Yes, "IHOL" is quite common.

Leopold Schlicht (May 03 2021 at 15:15):

Thanks!

Leopold Schlicht (May 04 2021 at 16:11):

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)?

Mike Shulman (May 04 2021 at 17:27):

I think either would be fine.

Leopold Schlicht (May 04 2021 at 17:35):

Thanks!