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: category theory

Topic: only slightly higher topoi

sarahzrf (Mar 27 2020 at 23:28):

Hey @Mike Shulman i just realized you're here & i wanted to ask you about some of the 2-topos stuff on your sub-nlab, if you'd be willing to answer my questions? I've been periodically coming back around lately to thinking about what a dependent type theory for interpretation in PreOrd—i.e., (0, 1)-Cat—would look like, and while I've only nibbled around the edges of the 2-topos stuff, the little I've managed to understand has definitely been a big help in figuring out which direction is probably the right way to go (say, the fact that I probably want to use fibrational slices rather than full slices). (I guess if (0, 0)-Cat is a 1-topos and (1, 1)-Cat should be a 2-topos, then (0, 1)-Cat should probably be a (1, 2)-topos?)

sarahzrf (Mar 27 2020 at 23:39):

i think the main things bugging me are like

1. if you do work in Opf(C) (for C a preordered set), then that's the same as working in [C, PreOrd], right? But a global element of the constant functor at some D is then gonna correspond to just an element of D, as far as I can tell, not to a monotone function C → D, and that is an identification that I would very much expect to hold if I want to be able to get such a function as the semantics of a term $x : C \vdash e : D$. If I use lax natural transformations as morphisms, it seems to work, but I have no idea what other consequences that might have???

2. something seems really fishy about the Hom type constructor. I should take another look at how it was set up on the page for the internal language, but if types are supposed to be functorial in their free variables, then shouldn't the first argument have to have type C^op rather than C? i've thought much more about my case, anyway, which is having ≤ as a proposition constructor, and i'm almost certain that just typing it as $\Gamma \vdash e : A \quad \Gamma \vdash e' : A \implies \Gamma \vdash e \le e'\ \mathsf{prop}$ is gonna be a problem. but if i keep C^op and C as completely separate types, and type ≤ as such, then how on earth do i type reflexivity and transitivity?!

sarahzrf (Mar 27 2020 at 23:41):

anyway, i welcome anyone else's input too!!

Mike Shulman (Mar 29 2020 at 14:28):

@sarahzrf Right, these are some of the main issues with internal logic of categories with directed 2-cells. My opinion is that while you may want syntactic restrictions to isolate classes of dependent types corresponding to fibrations and opfibrations, the terms in such types should not be required to be morphisms of such (to preserve cartesian arrows). This solves your (1) because a term $x:C \vdash e:D$ is a section of the projection $C\times D \to C$, and if it's not required to be a morphism of opfibrations then this is really just a map $C\to D$. For your (2) I think that the basic hom-type should depend on two copies of $C$, perhaps one marked as contravariant and one as covariant (if you like); then you can type reflexivity and transitivity (and even symmetry) without a problem since they are also not required to be maps of (op)fibrations.

sarahzrf (Mar 30 2020 at 08:34):

ok :)

sarahzrf (Mar 30 2020 at 08:35):

although, uh

sarahzrf (Mar 30 2020 at 08:35):

oh right, ok, fibrations are stable under arbitrary pullback right, ok

sarahzrf (Mar 30 2020 at 08:37):

hmmmm, i'm not quite seeing what you mean about (2)—what exactly do you mean about "two copies of $C$"?

sarahzrf (Mar 30 2020 at 08:38):

i was actually playing around a bit with maybe doing stuff over a twisted arrow category (or rather, the corresponding notion in PreOrd) so that i could talk about a "covariant component" and "contravariant component" of each free variable, but

sarahzrf (Mar 30 2020 at 08:38):

is that similar to what you're talking about?

sarahzrf (Mar 30 2020 at 13:49):

(i was thinking maybe it'd mean that quantifiers could correspond to ends/coends—cant remember whether it ended up working out, I hadn't touched this in a little while)

Mike Shulman (Mar 30 2020 at 22:57):

I just mean $x:C, y:C \vdash \hom(x,y) : \rm Type$: there are two variables.

sarahzrf (Mar 30 2020 at 22:58):

oh

sarahzrf (Mar 30 2020 at 22:58):

well, the issue i had in mind was—

sarahzrf (Mar 30 2020 at 22:59):

reflexivity is gonna be something like $\Gamma \vdash e : A \implies \Gamma \vdash \mathsf{refl}_e : e \le_A e$

sarahzrf (Mar 30 2020 at 22:59):

except that that's ill-typed if one side is supposed to be $A^\mathrm{op}$

sarahzrf (Mar 30 2020 at 23:01):

but if i do go with both being $A$, then $\le$ is not a fibration

sarahzrf (Mar 30 2020 at 23:01):

...i think. more to the point, we lose the ability to transport by $\le$, which corresponds to being a fibration iirc

sarahzrf (Mar 30 2020 at 23:01):

since $\le$ is contravariant in its first argument

Nathanael Arkor (Mar 30 2020 at 23:08):

I realise I'm missing a lot of the context here, so apologies if this is a naïve question, but rather than having $\leq$ as a type constructor (à la directed type theory), is it possible a type theory with rewriting (where $\leq$ is essentially a different kind) could be suitable?

Nathanael Arkor (Mar 30 2020 at 23:08):

I think you don't have the same issues with variance in type theories with rewriting

Nathanael Arkor (Mar 30 2020 at 23:09):

(on the other hand, it might be totally unsuitable for the problems you're interested in)

sarahzrf (Mar 30 2020 at 23:17):

i don't know anything about type theories with rewriting—never even heard the term :sweat_smile:

sarahzrf (Mar 30 2020 at 23:17):

can you tell me about em?

Nathanael Arkor (Mar 30 2020 at 23:18):

the idea is that they give a nice internal language for things like poset-enriched categories and 2-categories — instead of having equalities between terms (e.g. for $\beta$- and $\eta$-rules), you instead have directed rewrites

Nathanael Arkor (Mar 30 2020 at 23:18):

it's a more computational approach to the typical computation rules

sarahzrf (Mar 30 2020 at 23:18):

do you have a source i can check out?

Nathanael Arkor (Mar 30 2020 at 23:18):

let me find a good reference

sarahzrf (Mar 30 2020 at 23:18):

haha, jinx

sarahzrf (Mar 30 2020 at 23:19):

anyway though, it does seem to me like it should be possible for this to be a bona fide proposition

Nathanael Arkor (Mar 30 2020 at 23:19):

I think the classical reference is Seely's Modelling computations: A 2-categorical framework (http://www.math.mcgill.ca/rags/WkAdj/LICS.pdf)

sarahzrf (Mar 30 2020 at 23:19):

because this should be some kind of truncation of a 2-topos type theory, and hopefully 2-topoi should have a type theory

Nathanael Arkor (Mar 30 2020 at 23:19):

a more recent reference is Fiore–Saville's A type theory for cartesian closed bicategories (https://arxiv.org/pdf/1904.06538.pdf)

sarahzrf (Mar 30 2020 at 23:19):

awww the typesetting is unpleasant :(

sarahzrf (Mar 30 2020 at 23:19):

oh that's nicer

Nathanael Arkor (Mar 30 2020 at 23:20):

which has more pleasant type setting :big_smile:

Nathanael Arkor (Mar 30 2020 at 23:20):

yes, I would have imagined it would be possible in the directed type theory style too

Nathanael Arkor (Mar 30 2020 at 23:21):

(and there's often value in different syntaxes for the same theory, which emphasise different perspectives)

Nathanael Arkor (Mar 30 2020 at 23:22):

but depending on what you want to use the type theory for, maybe rewrites could provide a different starting point too

sarahzrf (Mar 30 2020 at 23:22):

:thumbs_up:

Nathanael Arkor (Mar 30 2020 at 23:23):

(I'm biased because I really don't like seeing "op" in type theories, which seems to be quite common in directed type theories — I personally think variance should be entirely implicit in the syntax)

sarahzrf (Mar 30 2020 at 23:24):

you mean like having another arrow?

Nathanael Arkor (Mar 30 2020 at 23:25):

I mean, take the simply-typed $\lambda$-calculus as an example: the function type constructor is contravariant in its first argument, but the variance is entirely encoded in the introduction/elimination rules, etc.

Nathanael Arkor (Mar 30 2020 at 23:26):

the variance is a sort of side-effect of the other rules; it doesn't need to be explicit

Nathanael Arkor (Mar 30 2020 at 23:26):

similarly for rewriting, where you're talking about homs, but variance is never explicit in the syntax

sarahzrf (Mar 30 2020 at 23:42):

i feel like that's a different Kind Of Thing but i'd have to really chew on it to articulate why >.>

Mike Shulman (Mar 31 2020 at 00:03):

Going back to the original conversation... that's right, $\le$ is not a fibration of the same variance in both its variables, so when you substitute the diagonal into it, you get something that's not a fibration at all. Ergo, if you want reflexivity (and presumably you do), you have to allow dependent types that aren't fibrations (of any variance). You can still transport by $\le$ in types that are fibrations, it's just that not all types are fibrations. See for instance https://arxiv.org/abs/1705.07442 for a type theory in which not all types are fibrations, but there is an internal characterization of those that are.

Mike Shulman (Mar 31 2020 at 00:05):

I think STLC is at a different level than what we're talking about here. STLC is the internal language of a CCC, and there are type constructors such as the function-type that are contravariant on some of their arguments. But the question here is about the internal language of a 2-category with an "opposite" operation on its objects, and in which some type families and terms are contravariant in their arguments. I don't know of any way to make that "implicit", although you can represent the "opposite" modality judgmentally.

Nathanael Arkor (Mar 31 2020 at 00:08):

dualising objects does make quite a difference, yes — what formal categorical structure does this correspond to?

sarahzrf (Mar 31 2020 at 00:09):

every category, or in my case every preordered set, has an opposite

sarahzrf (Mar 31 2020 at 00:09):

if you like, it probably corresponds to being autonomous

Nathanael Arkor (Mar 31 2020 at 00:10):

ah, so you want a type theory for the category $\mathbf{Preord}$, rather than a type theory for arbitrary (structured) preorder-enriched categories?

sarahzrf (Mar 31 2020 at 00:10):

:point_up: see the first post

Nathanael Arkor (Mar 31 2020 at 00:11):

ah, I misread the post — that makes perfect sense

Nathanael Arkor (Mar 31 2020 at 00:12):

that is a little different from the focus of the rewriting theories, then

Nathanael Arkor (Mar 31 2020 at 00:12):

sorry for sending you down an unrelated rabbit hole :sweat_smile:

Nathanael Arkor (Mar 31 2020 at 00:14):

oh wait, I had read

Right, these are some of the main issues with internal logic of categories with directed 2-cells.

which is relevant (but I misinterpreted that as being the main focus)

sarahzrf (Mar 31 2020 at 00:15):

it's cool!

Dan Doel (Mar 31 2020 at 00:15):

Some families on the universe are co/contravariant with respect to function spaces in relatively ordinary type theory, and that's implicit.

Dan Doel (Mar 31 2020 at 00:16):

You don't need to talk about $\mathcal U$ and $\mathcal U^{op}$, although perhaps it would be convenient to be able to do that rather than carrying around proofs of variance.

Dan Doel (Mar 31 2020 at 00:21):

Although the 'win' with identities/paths is that everything respects them, so you don't need to carry around anything. If not everything respects directed maps in the same way, I'm unclear what the win is on carrying around the information in one way or another.

Mike Shulman (Mar 31 2020 at 00:23):

@sarahzrf 2-categories such as Cat and Preord are not autonomous; the duality is just a "2-contravariant involution". You can make it an autonomous duality if you move to the bicategory Prof instead, or a star-autonomous duality if you use multivariable adjunctions, but the internal languages of those cases are even murkier.

sarahzrf (Mar 31 2020 at 00:24):

ah

Mike Shulman (Mar 31 2020 at 00:26):

@Dan Doel You can make it implicit there because the universe $\mathcal{U}$ doesn't carry within it the notion of "morphism": it's only an $\infty$-groupoid, not a category structure of any sort. It just so happens that there is a type constructor $\to$ that can be used to make $\mathcal{U}$ into a category, but there are also other choices of ways to make $\mathcal{U}$ into a category.

You can get plenty of win from knowing that some things respect morphisms, even if you don't know that everything does, as long as you have sensible and useful rules for deducing which things respect morphisms.