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.
Ruby Khondaker (she/her) (Jul 14 2025 at 16:51):Is this the "term model" of the type theory? I've often found it psychologically easier to pretend I'm working in the term model when doing type-theoretic things, since then I have an actual concrete idea for what an arbitrary term should be - something one can obtain in a finite sequence of steps from applying the introduction and elimination rules of the types in your theory. At least, if I've understood correctly!
Mike Shulman (Jul 14 2025 at 18:00):Yes, this is the term model. But I actually think it's misleading to think too much about the term model when you're working in type theory, since type theory has much wider semantics than that. If you have the term model too much in mind you may have too limited an idea of what exists. For instance, it's true that in the term model all the objects are built from a finite sequence of steps of rules, but in a general model that isn't the case, so if you think too hard about that you may get misled.
Mike Shulman (Jul 14 2025 at 18:01):People think type theory is more "syntactic" than set theory, but it really isn't. When we write we don't think of it as a "term", we think of it as just representing an actual set, and we can do the same for the syntax of type theory.
Ruby Khondaker (she/her) (Jul 14 2025 at 20:17):Mike Shulman said:
Yes, this is the term model. But I actually think it's misleading to think too much about the term model when you're working in type theory, since type theory has much wider semantics than that. If you have the term model too much in mind you may have too limited an idea of what exists. For instance, it's true that in the term model all the objects are built from a finite sequence of steps of rules, but in a general model that isn't the case, so if you think too hard about that you may get misled.
Ooh ok, in what senses would this kind of thinking mislead you? I remember in the past being very confused because I had no intuition for what a "term" in type theory was supposed to be, whereas I had a good idea that a "set" was a collection of things. Thinking in terms of the term model gave me that intuition of what "terms" should be - so if I abandon it, I run into the same problem of not really knowing what a "term" is...
Mike Shulman (Jul 14 2025 at 20:36):When working in type theory (as opposed to on type theory, i.e. doing metatheory), I don't like to use the word "term". To me "term" suggests a syntactic object. When working in type theory I generally use words like "element" instead. Then the intution is just like for set theory: a type is a collection of things, and its elements are the things it is a collection of.
Notification Bot (Jul 14 2025 at 20:37):5 messages were moved here from #learning: questions > Continuations, parametricity, and polymorphism by Mike Shulman.
Ruby Khondaker (she/her) (Jul 14 2025 at 20:40):Hm, ok... so then, why do people use "terms" in type theory so often, as opposed to just "element"?
Vincent R.B. Blazy (Jul 14 2025 at 20:46):I like inhabitant, in type theory! Precisely to remain with type-theoretic intuition and not to get confused with set-theoretic intuition
Mike Shulman (Jul 14 2025 at 20:52):Ruby Khondaker (she/her) said:
Hm, ok... so then, why do people use "terms" in type theory so often, as opposed to just "element"?
I don't know, who are these people? (-:
Ryan Wisnesky (Jul 14 2025 at 20:53):in equational and Horn logic, initial models can be constructed from terms. the terminology is prevalent there. but once you move to more expressive logics, this property breaks down.
Mike Shulman (Jul 14 2025 at 20:55):Initial models can always be constructed from terms (meaning syntactic objects).
Mike Shulman (Jul 14 2025 at 20:56):This is the central fact of categorical logic and the syntax/semantics adjunction.
Ryan Wisnesky (Jul 14 2025 at 21:06):terms in the same signature of the theory you're starting with? How do you witness existential quantifiers (that aren't "exists unique")?
why-horn-formulas-matter-in-computer-science-initial-4rtnikvejv.pdf
Ryan Wisnesky (Jul 14 2025 at 21:08):this is could be a difference in terminology again. I'm quoting from e.g. https://link.springer.com/chapter/10.1007/3-540-15198-2_24 , which I'll try to find a free version for.
Mike Shulman (Jul 14 2025 at 21:09):Yeah, the initial model is doctrine-relative.
Mike Shulman (Jul 14 2025 at 21:10):Equational and Horn theories can be stated context-free, so it makes sense to talk about an initial model in a contextless doctrine, which is just a set. But more general type theories with contexts are in a doctrine with contexts, and so their initial models have to be categories, not sets.
Ruby Khondaker (she/her) (Jul 14 2025 at 21:27):Mike Shulman said:
Ruby Khondaker (she/her) said:
Hm, ok... so then, why do people use "terms" in type theory so often, as opposed to just "element"?
I don't know, who are these people? (-:
Hm, basically every type theory resource I've seen...?
Mike Shulman (Jul 14 2025 at 21:33):It's hard for me to comment on it without a specific reference.
Mike Shulman (Jul 14 2025 at 21:34):If they're writing about the syntax of type theory, as many people are, then of course they're going to say "term".
Mike Shulman (Jul 14 2025 at 21:35):It's possible I misinterpreted what you meant when you said
Ruby Khondaker (she/her) said:
I've often found it psychologically easier to pretend I'm working in the term model when doing type-theoretic things
If by "doing type-theoretic things" you meant "working with the syntax of type theory", then there's absolutely nothing wrong with "working in the term model", since that's really synonymous with working with syntax since the term model is built out of syntax. I thought you meant instead "doing mathematics inside a type-theoretic foundation".