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.
Jem (May 10 2020 at 21:38):I'm trying to work through some of the basic stuff in dependent type theory - although I'm comfortable practically with working with dependent types, I've not worked through the gap between the rules for the theory and things which you would assume when doing proofs in the theory.
In particular, suppose we have that , , and , for some sort of judgement. What facts or assumptions are typically needed to derive ? Is it then a derivable rule, or just an admissible rule?
Nathanael Arkor (May 10 2020 at 22:11):That depends on how the type theory is set up, but it'll be typically be admissible if you allow variables to be projected from anywhere in the context. You would usually have to add an exchange rule for it to be derivable.
Thibaut Benjamin (May 11 2020 at 10:01):It is usually the case that this rule is admissible, but there is no obligation for it. Think about simple type theory, this rule may not even be admissible if you work for instance in linear logic. The dependent type theories I know currently have this rule as admissible, but I believe many people are trying to design dependent type theories that don't satisfy this (I don't know how far they've gone though). It is still not completely clear to me at the moment how weakening and exchange interact precisely, but I think you could have weakening without exchange or exchange without weakening, provided the right rules.
sarahzrf (May 11 2020 at 14:06):linear logic generally satisfies exchange—it's "ordered logic" that doesnt
Thibaut Benjamin (May 11 2020 at 14:20):thanks; I am still a bit confused with the names in the logic side. I am more comfortable with the naming in the multicategory side (multicategory/symmetric multicategory/cartesian multicategory)