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.
Alexander Gietelink Oldenziel (Oct 20 2020 at 09:53):I have two questions concerning the relation between Sequent Calculus and Type Theory
A) In a typical type theory like HoTT there are four kinds of inference rules: type formation, term introduction, term elimination, and computation rules. The last rule type has a different status than the first three so I will ignore it for now.
HoTT is based on Natural Deduction. If instead of Natural Deduction we take the Sequent calculus perspective we replace term intro rules with Right rules, and the term elimination rules with Left Rules.
What about type formation rules? Conceptually they should be term introduction rules (= Right rules in the sequent calculus) for the Universe U.
If we continue this train there should also be right rules for the Universe U? What are they?
B) The term introduction and elimination rules corresponds in categorical semantics to structure morphisms and universal properties (or the other way around depending on the polarity of the type, i.e. whether it is a (co)limit). In this way we can deduce the rules from the categorical structure.
Can we do a similar thing with sequent calculus? How do we guess the left rules?
Literature: it seems the following paper might be relevant, but it doesn't talk about categorical semantics at all
https://www.irif.fr/~emiquey/tmp/dL.pdf
Dan Doel (Oct 20 2020 at 14:45):Type formation rules are usually not the same as term formation rules for the universe. Types are introduced prior to any universes containing them. And it would be impossible to say that the universe itself (if you only have one) is a type (which it is) using judgments of its own terms, because it doesn't usually contain itself.
Anyhow, most logics just take for granted which propositions are well-formed, probably because the rules for them are pretty simple. In first-order logic they'd mostly need to talk about variable scoping, and most presentations neglect to even keep track of that. The well-formed types in dependent type theory are not so trivial, so it's more useful to present them as rules that can be checked like all the rest.
Dan Doel (Oct 20 2020 at 14:46):I have seen natural deduction presentations that do have proposition formation rules, but those were probably inspired by type theory.
Dan Doel (Oct 20 2020 at 14:50):Generally in sequent calculus, right rules correspond almost exactly to something from ND, so the left rule corresponds to whatever is the dual of that.
Dan Doel (Oct 20 2020 at 14:58):I think left rules are all eliminations, but it might depend on presentation.
Shea Levy (Oct 20 2020 at 15:02):Dan Doel said:
I think left rules are all eliminations, but it might depend on presentation.
Left rules coupled with cut make for eliminations inherently, no?
James Wood (Oct 20 2020 at 15:07):I've seen El mentioned as the eliminator for the (Tarski-style) universe, but I don't know how formal that intuition can be made. μμ̃̃ is perhaps a good framework to formalise that in.
Dan Doel (Oct 20 2020 at 15:08):I'm not sure that really makes sense. El isn't much like the other eliminators.
Dan Doel (Oct 20 2020 at 15:09):Also there are presentations of MLTT that actually have an induction principle for the universe.
James Wood (Oct 20 2020 at 15:11):I think the only real difference is that it targets types rather than terms, and in μμ̃̃ you don't have to target eliminators as much as you do in natural deduction.
Dan Doel (Oct 20 2020 at 15:12):Well, that in itself is a huge difference. It's a type formation rule, not a term rule.
James Wood (Oct 20 2020 at 15:16):But there are still computation rules between El and the constructors of the universe. For example, El (A '+ B) ↝ El A + El B, where '+ is the code for the sum type former, and + is the actual type former.
Alex Gryzlov (Oct 25 2020 at 19:25):Mike Shulman's https://mikeshulman.github.io/catlog/catlog.pdf has quite a few mentions of sequent calculi, including this passage (page 48):
... sequent calculus and natural deduction make different choices of which properties to ensure by their definitions of composition. Roughly speaking, sequent calculus chooses to make the defining equations of universal properties hold exactly (e.g. the composites of a paired morphism
<f,g> : X -> A x Bwithpi_1andpi_2are exactlyfandgrespectively); this is what the “principal case” of its cut-admissibility proof does. On the other hand, natural deduction chooses to make the naturality of universal properties hold exactly; the equality between the two distinct sequent calculus derivations above expresses the naturality of pairing<f,g> : X -> A x Bwith respect to precomposition bypi_1.