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.
Nathanael Arkor (Apr 17 2020 at 16:07):I have a question about the (extensional) MLTT ~ LCCCs result of Seely and Clairambault–Dybjer. As I understand it, Seely's original paper has a flaw in that substitution in types may not be interpreted correctly by pullback, as pullbacks are not strict. This was later rectified in several ways, culminating in Clairambault–Dybjer's proof of biequivalence. Let's consider for a moment finitely complete categories, which correspond to MLTT without Pi types. Every finitely complete category is equivalent to a strict finitely complete category (in which pullbacks are strictly associative), by a result of Freyd–Scedrov. If the only issue with Seely's proof is this nonassociativity of pullbacks (Hoffman mentions an issue with Sigma types, but as far as I can tell, these are related), then can't we just consider strict finitely complete categories, which are equivalent to arbitrary finitely complete categories, and get a correct proof of sound and complete equivalence by Seely's result? When we work in the internal language, we just care about things up to equivalence in any case.
This is surely not the case, but I don't know where the flaw in my reasoning lies. Could someone enlighten me?
Cody Roux (Apr 17 2020 at 16:09):I'm also curious about this. More generally clarifying the obstruction.
Kenji Maillard (Apr 17 2020 at 17:24):I don't know the result by Freyd-Scedrov (would be interested if you have a reference), but can you directly transport the LCCC structure along that finite-limit-strictifying equivalence ?
Nathanael Arkor (Apr 17 2020 at 17:30):The reference is Categories, Allegories 1.4(10)1. The finite limit structure should be preserved by the equivalence, by virtue of it being an equivalence, if that's what you mean? As for the closed structure, that's a question I'm happy to leave for later, though I would have hoped it was a similar story.
Dan Doel (Apr 17 2020 at 17:31):Exponentials aren't finite limits in general.
Nathanael Arkor (Apr 17 2020 at 17:32):@Dan Doel: to clarify, by "similar story" I meant that I hoped that there was a coherence result for cartesian-closed categories that was relevant, not that you could use finite limits to describe the closed structure.
Dan Doel (Apr 17 2020 at 17:33):Ah, yeah. Is there a similar theorem for small-complete categories or something?
Nathanael Arkor (Apr 17 2020 at 17:40):It's not discussed there, at least (though I would hope so).
Mike Shulman (Apr 17 2020 at 23:29):I don't have a copy of cats+alls with me. Are the pullbacks associative for pasting in both directions simultaneously? That's roughly what would be needed for Sigma-types. And is the specified pullback of a diagonal again a diagonal? That's roughly what would be needed for identity types. For Pi-types one would need a particular Beck-Chevalley isomorphism to be an identity.
Nathanael Arkor (Apr 17 2020 at 23:36):image.png
This is the lemma about pullbacks. What do you mean by "both directions simultaneously"?
Nathanael Arkor (Apr 17 2020 at 23:37):There doesn't appear to be a statement regarding the diagonal, so one would have to check this.
Mike Shulman (Apr 17 2020 at 23:38):The question is whether the vertical pasting of canonical pullbacks is also again a canonical pullback. This would follow from the lemma if the transpose of a canonical pullback is again a canonical pullback. Also, are they functorial on identities, i.e. is a square with identities on the top and bottom a canonical pullback?
Mike Shulman (Apr 17 2020 at 23:38):Is the construction simple enough that you could copy it for us here?
Nathanael Arkor (Apr 17 2020 at 23:41):The question is whether the vertical pasting of canonical pullbacks is also again a canonical pullback. This would follow from the lemma if the transpose of a canonical pullback is again a canonical pullback.
Ah, I see :+1:
Nathanael Arkor (Apr 17 2020 at 23:42):Mike Shulman said:
Is the construction simple enough that you could copy it for us here?
Unfortunately, it spans several pages.
Nathanael Arkor (Apr 17 2020 at 23:43):As far as I can tell, it doesn't resolve your other questions either, and it's not clear to me without working through the construction (which it's a little late for right now).
Mike Shulman (Apr 17 2020 at 23:44):Ok, well at least this gives you a place to start figuring out the answer. (-:
Nathanael Arkor (Apr 17 2020 at 23:44):They use a theory of -tables, which is entirely alien to me.
Nathanael Arkor (Apr 17 2020 at 23:44):@Mike Shulman: if this construction was strict in the senses you describe, would this imply Seely's result is strong enough for an internal language correspondence?
Mike Shulman (Apr 17 2020 at 23:45):It's not outside the realm of possibility that this construction might be an alternative solution to the coherence problem and that type theorists just weren't aware of it. Cats+alls is pretty idiosyncratic in outlook and notation and I think not all of its contents are widely known even in the CT community.
Mike Shulman (Apr 17 2020 at 23:46):However, if the FS construction does span several pages, then it seems unlikely to me to be simpler than the now-better-known strictifications used for semantics of type theory, and the latter are almost certainly more general and flexible.
Nathanael Arkor (Apr 17 2020 at 23:48):That's true. On the other hand, it would have been nice to solve the coherence problem in a few lines by citing Freyd–Scedrov :)
Nathanael Arkor (Apr 17 2020 at 23:50):Mike Shulman said:
I don't have a copy of cats+alls with me. Are the pullbacks associative for pasting in both directions simultaneously? That's roughly what would be needed for Sigma-types. And is the specified pullback of a diagonal again a diagonal? That's roughly what would be needed for identity types. For Pi-types one would need a particular Beck-Chevalley isomorphism to be an identity.
@Soichiro Fujii was the one who pointed this result out to me — perhaps they already know the answer to this question?
Soichiro Fujii (Apr 18 2020 at 00:37):Mike Shulman said:
The question is whether the vertical pasting of canonical pullbacks is also again a canonical pullback. This would follow from the lemma if the transpose of a canonical pullback is again a canonical pullback. Also, are they functorial on identities, i.e. is a square with identities on the top and bottom a canonical pullback?
Vertical pasting of canonical pullbacks is not always a canonical pullback. But there is a proposition (1.49(11) (iv)) guaranteeing this under a certain condition (that the suitable morphism involved is auspicious—yes, yet another idiosyncratic term).
And I think a square with identities on the left and right is a canonical pullback.
Regarding other questions of you, I am afraid that I am not familiar enough with -categories to answer immediately. I answered to Nathanael Arkor’s question only because I remembered reading about -categories, and I have not really worked with them. By the way, the idea of applying -categories to coherence issues on models of extensional Martin-Löf type theory never occurred to me, and sounds interesting!
Nathanael Arkor (Apr 18 2020 at 00:40):@Soichiro Fujii: thank you for clarifying!
Nathanael Arkor (Apr 18 2020 at 00:58):@Mike Shulman: thanks for your help!