Reading group on "Sheaves in Geometry and Logic" · theory: category theory

I've recently started working through "Sheaves in Geometry and Logic", and was wondering if there was any interest in starting a reading group around it!

Christian Williams (Mar 23 2020 at 21:08):

Stelios Tsampas (Mar 23 2020 at 21:09):

Philip Zucker (Mar 23 2020 at 21:11):

I know someone who had been mentioning wanting to read that very book. I'm curious, but I feel like it would be beyond my level.

Reed Mullanix (Mar 23 2020 at 21:11):

It's been quite good so far, though I've only made it through the first 45 pages or so

Stelios Tsampas (Mar 23 2020 at 21:12):

Christian Williams (Mar 23 2020 at 21:13):

Stelios Tsampas (Mar 23 2020 at 21:13):

Christian Williams (Mar 23 2020 at 21:13):

John Baez (Mar 23 2020 at 21:14):

I gave up producing online lecture notes on "Sheaves in Geometry and Logic" because my group was not very excited about it and... coronavirus. If enough people were interested I could keep going, at least for a while.

Christian Williams (Mar 23 2020 at 21:16):

my motivation is mainly on the logical side. I want to master the internal language, especially all the stuff you can do with the "quantifiers as adjoints" idea.

John Baez (Mar 23 2020 at 21:16):

Reed Mullanix (Mar 23 2020 at 21:19):

I'm also interested in the logical aspect, especially from the perspective of proof assistants/PLT. The time dependent set stuff seems like it could have cool applications

Christian Williams (Mar 23 2020 at 21:21):

Christian Williams (Mar 23 2020 at 21:22):

what's your plan for reading it? I have tons of stuff I should be doing, but this book is kind of an ongoing goal.

sarahzrf (Mar 23 2020 at 21:22):

i was talking to joe moeller about this a little bit—he said that the ucr category theory group had talked about some kind of time dependent set stuff

sarahzrf (Mar 23 2020 at 21:23):

but i remember @John Baez tweeting about PSh(N^op), whereas the topos of trees is PSh(N)

sarahzrf (Mar 23 2020 at 21:23):

but joe seemed to think that the subobject classifier of the category they'd been talking about was the same as PSh(N)'s

sarahzrf (Mar 23 2020 at 21:24):

John Baez (Mar 23 2020 at 21:24):

"Time-dependent sets" in Mac Lane and Moerdijk are presheaves on N^op (that is, N with the opposite of its usual ordering). I called the objects in here "infinitely deep forests".

John Baez (Mar 23 2020 at 21:25):

The subobject classifier works sorts of similarly for presheaves on any totally ordered set (or "toset"), but the details depend on the toset in question.

sarahzrf (Mar 23 2020 at 21:27):

Reed Mullanix (Mar 23 2020 at 21:27):

@Christian Williams I generally try to get through 10-5 pages every other night, and try to formalize the important theorems in agda on the days between reading.

sarahzrf (Mar 23 2020 at 21:27):

but i mean for example the subobject classifier in PSh(N) is (classically) finite at each stage, whereas it's infinite at each stage in PSh(N^op)

sarahzrf (Mar 23 2020 at 21:27):

Reed Mullanix (Mar 23 2020 at 21:28):

Though I think I may need to switch proof assistants soon, I keep getting mired down in setoid hell.

Christian Williams (Mar 23 2020 at 21:28):

true. sometimes people are pretty loose when they say "presheaf", not caring about variance. but it matters

sarahzrf (Mar 23 2020 at 21:29):

at POPL, i met pierre-marie pedrot (one of the coq maintainers) and he was in the middle of telling me about a categorical model of type theory involving presheaves when he said that presheaves being contravariant was a historical accident and they could have as well been covariant

sarahzrf (Mar 23 2020 at 21:30):

Matt Cuffaro (he/him) (Mar 23 2020 at 21:30):

sarahzrf (Mar 23 2020 at 21:30):

Christian Williams (Mar 23 2020 at 21:32):

John Baez (Mar 23 2020 at 21:32):

True. I don't think of these cases as dramatically different: I think of them as illustrating a general pattern.

When you've got presheaves on a toset, the subject object classifier has a set of truth values at each stage that stand for "times to truth" - how long it takes something to become true, together with an extra value called "never". For presheaves on N^op you get infinitely many such values, since N is unbounded above, while for N you don't, since N^op isn't. (The "opposite" stuff gets a bit annoying around here.)

sarahzrf (Mar 23 2020 at 21:34):

well, i meant more like "quantitatively different" than "qualitatively different" i suppose

John Baez (Mar 23 2020 at 21:34):

Emily Pillmore (Mar 23 2020 at 21:41):

Has this started already? This was going to be my next book in parallel with Reihl's Categorical Homotopy Theory

Reed Mullanix (Mar 23 2020 at 21:45):

I haven't gotten too far into it yet, so I would be totally OK with starting from the beginning :slight_smile:

Emily Pillmore (Mar 23 2020 at 21:45):

Noice, well, if you commit, I'm committed as well and I'd be happy to schedule something more regular

Emily Pillmore (Mar 23 2020 at 21:46):

Thomas Read (Mar 23 2020 at 21:46):

Reed Mullanix (Mar 23 2020 at 21:50):

Ok, let's make this official! The 1st 45 pages are a bit of review + an introduction to some example topoi, so it should be pretty fast to work through.

Bhavik Mehta (Mar 23 2020 at 21:50):

On the note of formalisation, I and a couple of others are proving theorems from here in the lean theorem prover (the plan is to have roughly chapters 4-6, with a few proofs taken from the elephant instead)

Reed Mullanix (Mar 23 2020 at 21:51):

I've been meaning to learn lean for the longest time, so I would love to help out :slight_smile:

sarahzrf (Mar 23 2020 at 21:51):

Stelios Tsampas (Mar 23 2020 at 21:51):

Stelios Tsampas (Mar 23 2020 at 21:52):

Bhavik Mehta (Mar 23 2020 at 21:52):

Stelios Tsampas (Mar 23 2020 at 21:52):

Reed Mullanix (Mar 23 2020 at 21:52):

Balaram Usov (Mar 23 2020 at 21:55):

John Baez (Mar 23 2020 at 21:56):

If there's any way I can help out, let me know. When you get to the end of what I covered in parts 1-8 of my blog posts, I'd be happy to start writing more.

John Baez (Mar 23 2020 at 21:57):

I started blogging about this book because I wanted to learn topos theory really thoroughly. What stopped me was the lack of a visibly interested audience - plus, too many other things to do.

Reed Mullanix (Mar 23 2020 at 21:59):

Let's make this official: I propose that we make it to page 48 (Propositional Calculus) by Sunday. We can then set up a short discussion session (whether that be over text, or voice) to cover the material.

Emily Pillmore (Mar 23 2020 at 22:05):

Cody Roux (Mar 23 2020 at 22:41):

Count me in, if there's room! I've tried reading this book several times, I'd love another crack at it...

Emily Pillmore (Mar 23 2020 at 22:42):

Emily Pillmore (Mar 23 2020 at 22:43):

Joe Moeller (Mar 23 2020 at 22:44):

you can merge topics within the same stream by simply naming them the same thing. Is that what happened here?

Emily Pillmore (Mar 23 2020 at 22:44):

Matteo Capucci (he/him) (Mar 24 2020 at 13:06):

I've been through the first ~8 chapters (with varying level of details, tbh), I'm here too :)

John Baez (Mar 24 2020 at 16:49):

Here are two puzzles for people who want to read Sheaves in Geometry and Logic. I hope that people who are already experts on Heyting algebras don't answer these! These puzzles are connected to Section I.8 of the book.

John Baez (Mar 24 2020 at 16:49):

Puzzle 1. In an a Heyting algebra, is

\neg{P} \vee Q

equal to

P \Rightarrow Q

? Prove it's true or find a counterexample.

John Baez (Mar 24 2020 at 16:51):

Puzzle 2. In a Heyting algebra, is

(\neg \neg \neg P) \Rightarrow (\neg P)

true (that is, equal to

\top

)? Prove this or find a counterexample.

Mike Stay (Mar 24 2020 at 17:21):

For puzzle 2, you can ask lambdabot in the Haskell IRC channel for a function of type (((p -> Void) -> Void) -> Void) -> (p -> Void) with the @djinn command for a solution, if it exists. (Void type)

Cody Roux (Mar 24 2020 at 17:27):

Reed Mullanix (Mar 24 2020 at 17:38):

John Baez (Mar 24 2020 at 17:59):

Cody Roux (Mar 24 2020 at 17:59):

Stelios Tsampas (Mar 24 2020 at 19:36):

Not true! That became apparent after a bit... but I found the counter-example online hihi. Does it still count? :P

John Baez (Mar 24 2020 at 19:37):

Maybe let someone else in this reading group figure out a counterexample. Probably best to not point people to sources of answers... brain exercise is good.

Stelios Tsampas (Mar 24 2020 at 19:38):

John Baez (Mar 24 2020 at 19:39):

Thanks! If I think intuitionistically, it doesn't feel like these are equal. In intuitionistic logic I know

\neg P \vee Q

it means I either know

\neg P

or I know

Q

John Baez (Mar 24 2020 at 19:39):

That's why

\neg P \vee P

doesn't automatically equal "true" - you may not know which of

\neg P

P

holds.

Stelios Tsampas (Mar 24 2020 at 19:40):

John Baez (Mar 24 2020 at 19:40):

But I think I can know

P \Rightarrow Q

without knowing either

\neg P

Q

. Like I know "if it's raining I'll get wet outside", without knowing either that it's not raining or that I'm wet.

John Baez (Mar 24 2020 at 19:41):

Stelios Tsampas (Mar 24 2020 at 19:42):

Correction, I started proving statement 1. but I realized I had to use LEM which was a red flag.

John Baez (Mar 24 2020 at 19:42):

Puzzle 1a. In an arbitrary Heyting algebra, can you show that

(\neg P \vee Q) \Rightarrow (P \Rightarrow Q)

Cody Roux (Mar 24 2020 at 19:43):

My strategy is usually build the proof-term in my head, if there's no obvious way to do it, it's not an intuitionistic tautology :)

John Baez (Mar 24 2020 at 19:44):

Cody Roux (Mar 24 2020 at 19:44):

It should be possible to make this reasoning precise, since the first proof of decidability of IL used the completeness of a certain sequent calculus, so you can trust this intuition to a certain extent.

John Baez (Mar 24 2020 at 19:44):

I'm posing these puzzles because a bunch of people wanted to read Sheaves in Geometry and Logic to boost their understanding of topos theory and logic.

Cody Roux (Mar 24 2020 at 19:45):

John Baez (Mar 24 2020 at 19:45):

Stelios Tsampas (Mar 24 2020 at 19:45):

John Baez (Mar 24 2020 at 19:45):

John Baez (Mar 24 2020 at 19:46):

I think subobject classifiers in some pretty simple categories of presheaves should give counterexamples ("counter-models") to would-be tautologies that aren't really tautologies in every Heyting algebra. But there are other ways to get your hands on Heyting algebras that should also work... probably they're explained in Sheaves.

Stelios Tsampas (Mar 24 2020 at 19:46):

Reed Mullanix (Mar 24 2020 at 20:00):

You can also do this by just reasoning diagramatically in a Cartesian Closed Category with coproducts + initial objects that distribute nicely!

Cody Roux (Mar 24 2020 at 20:01):

That's a fair point! I do like the internal language, but I have difficulty navigating between it and the external one...

Reed Mullanix (Mar 24 2020 at 20:03):

Yeah, it can definitely be tricky, took a long time before I felt comfortable doing that

Reed Mullanix (Mar 24 2020 at 20:04):

Cody Roux (Mar 24 2020 at 20:04):

Part of why I'm so interested in this RG: part of the magic of "Sheaves" for me is to take statements which I "intuitively" (no pun intended) know are not provable, or provable in Coq, and understand what kind of theorems or counter-example this implies in clever toposes

Cody Roux (Mar 24 2020 at 20:04):

Reed Mullanix (Mar 24 2020 at 20:05):

Matteo Capucci (he/him) (Mar 24 2020 at 21:31):

A wonderful exposition of the internal language of sheaf toposes is that of Blechschmidt

Matteo Capucci (he/him) (Mar 24 2020 at 21:32):

Look up his thesis, it's called "using the internal language of toposes in algebraic geometry" or something like that

Matteo Capucci (he/him) (Mar 24 2020 at 21:32):

Matteo Capucci (he/him) (Mar 24 2020 at 21:33):

Another lovely exposition is that of Leinster, it's on the nlab and the arXiv as well

Matteo Capucci (he/him) (Mar 24 2020 at 21:34):

John Baez (Mar 24 2020 at 21:38):

Nathanael Arkor (Mar 24 2020 at 21:40):

Mike Stay (Mar 24 2020 at 21:43):

I found Z.L. Low's paper "Logic in a Topos" to be a nice exposition of the Mitchell-Benabou language and of Kripke-Joyal semantics.

Cody Roux (Mar 24 2020 at 21:54):

BTW, Kripke counter-models for classical but non-intuitionistic tautologies are, of course, also sheaf-theoretical counter-models

Stelios Tsampas (Mar 24 2020 at 22:19):

We immediately have that

Q \leq (P \Rightarrow Q)

. For the left part we have that, by definition of exponentiation,

(P \Rightarrow 0) \wedge P \leq 0 \leq Q

. But then by the adjunction for

P \Rightarrow Q

we have that

(P \Rightarrow 0) \wedge P \leq Q

gives

(P \Rightarrow 0) \leq (P \Rightarrow Q)

, thus completing the proof.

I think the difficuly was mianly being precise , the intuition was pretty clear.

Stelios Tsampas (Mar 24 2020 at 23:09):

Actually, I can make it more precise: we can then go on to to do

Q \leq (P \Rightarrow Q)

iff

Q \wedge 1 \leq (P \Rightarrow Q)

iff

1 \leq (Q \Rightarrow (P \Rightarrow Q)) = 1

. Same for the other side, so afterwards we go

1 \leq (1 \wedge 1)

, substitute both sides and finally apply distributive law for

\Rightarrow

and

\wedge

Mike Stay (Mar 24 2020 at 23:18):

As a data type, puzzle 1a says, "Can you construct a function
f:: (Pair (P -> Void) Q) -> (P -> Q)?"

Stelios Tsampas (Mar 24 2020 at 23:20):

Yes, type-theoretically it's very obvious, immediate. I was trying to use terminology from Heyting algebra only ;).

Stelios Tsampas (Mar 24 2020 at 23:20):

Reed Mullanix (Mar 24 2020 at 23:27):

Stelios Tsampas (Mar 24 2020 at 23:29):

Stelios Tsampas (Mar 24 2020 at 23:32):

Stelios Tsampas (Mar 24 2020 at 23:34):

The good thing about more concrete stuff (like Agda compared to CT) is that is saves you from the trouble of having to be precise.

Mike Stay (Mar 24 2020 at 23:44):

Mike Stay (Mar 24 2020 at 23:46):

f (Left g) = g
f (Right q) = \p -> q

Cody Roux (Mar 25 2020 at 00:50):

Surely that's not quite right either, since g would be of type P -> Void and not P -> Q. Very close though.

Mike Stay (Mar 25 2020 at 01:51):

f (Left g) = absurd
f (Right q) = \p -> q

Hopefully now I've got it right. absurd is the name Data.Void gives to the unique function out of the initial object.

Vinay Madhusudanan (Mar 25 2020 at 03:28):

Vinay Madhusudanan (Mar 25 2020 at 03:40):

(But that's easily fixed. Note that g :: P -> Void; and it's available in the first pattern)

Mike Stay (Mar 25 2020 at 03:55):

Sigh. Yes. I should actually try typing things into Haskell first to make sure they work.

f x y =
    case x of
    Left g -> absurd (g y)
    Right q -> q

Vinay Madhusudanan (Mar 25 2020 at 03:56):

Right! (You could also have corrected the earlier one by just changing absurd to absurd . g)

Vinay Madhusudanan (Mar 25 2020 at 04:36):

I was reading about pullbacks in Milewski's book just yesterday, and if I'm not wrong, the type inference (for the "returned function") in this case is also via pullbacks? Because f takes Either (p -> Void) q, and returns a p -> q function, but neither of the cases taken separately returns p -> q — both have more "general" return types

Vinay Madhusudanan (Mar 25 2020 at 04:36):

Vlad Patryshev (Mar 25 2020 at 04:40):

I believe both alternatives produce p->q (is not there a Void ->q already? Is not there a q -> (p->q) already?)

Vinay Madhusudanan (Mar 25 2020 at 04:42):

I mean if you separately wrote f (Left g) = absurd . g (without the other case), then that would be Either (p -> Void) q -> (p -> r), not specifically … (p -> q)

Vinay Madhusudanan (Mar 25 2020 at 04:42):

Vinay Madhusudanan (Mar 25 2020 at 04:46):

So it takes one function (from the first pattern) of type p -> r, and another (from the second pattern) of type s -> q, where r and s are variable, and then deduces that the correct type is p -> q. (I'm probably using some incorrect terminology here, but hopefully the meaning is clear)

Vinay Madhusudanan (Mar 25 2020 at 04:47):

Mike Stay (Mar 25 2020 at 04:56):

Well, there's an isomorphism

c^{a + b} ≅ c^a\cdot c^b,

i.e. a function out of Either a b is the same as a pair of functions, one out of a and one out of b.

Vlad Patryshev (Mar 25 2020 at 05:44):

Reed Mullanix (Mar 25 2020 at 05:53):

Yeah, to get the categorical formulation you only need a cartesian closed category with coproducts and initial objects that distribute nicely

Vinay Madhusudanan (Mar 25 2020 at 05:57):

@Vlad Patryshev If t be the type of f: From the first pattern, we have t = p -> r; and from the second, t = s -> q; with p and q fixed, r and s variable. I thought getting t = p -> q by solving these two might be a pullback, based on what I'd understood from Milewski's example (https://bartoszmilewski.com/2015/04/15/limits-and-colimits/ ← the twice example here). I might've misunderstood

Verity Scheel (Mar 25 2020 at 06:04):

ah, you’re talking about unification/type inference. I think it can be modelled by pullbacks, but I don’t know CT well enough to say precisely ...

Verity Scheel (Mar 25 2020 at 06:11):

anyways, we don’t typically think of the two branches as having _different_ types, we think of them as having _compatible_ types that we can unify together so they are actually the same. we could make it more explicit if we wanted to, and actually write out the types as arguments, but it’s more convenient to omit them on paper, they’re just understood to be there already

Burak Emir (Mar 25 2020 at 06:58):

@Vinay Madhusudanan that is a great observation. Unification has been described categorically by Goguen "what is unification". Say the objects are sets of variables, the arrows substitutions (total mappings from vars to terms, the free vars of the substituted terms form the codomain). Then a most general unifier

\{r \mapsto q, s \mapsto p\}

is an equalizer. Equalizers can be expressed through pullbacks. https://ncatlab.org/nlab/show/equalizer

Cody Roux (Mar 25 2020 at 18:17):

As a tiny remark, this is the Kleisi category over the monad of terms over a set of variables, which is a nice setting in which to talk about instances and substitutions.

Reed Mullanix (Mar 25 2020 at 19:18):

There are also presheaf models of type theory, which is a large reason that I am reading this book! The basic idea is that

\Gamma \vdash

is a presheaf over some base category

C

, and context maps

\sigma : \Gamma \to \Delta

are natural transformations between presheaves.

Nathanael Arkor (Mar 25 2020 at 19:19):

@Reed Mullanix: I'm curious what relation of sheaves to presheaf models of type theory you're interested in?

Reed Mullanix (Mar 25 2020 at 19:21):

Well, if I understand correctly, sheaves themselves don't play nicely with these models (universes get weird)

Reed Mullanix (Mar 25 2020 at 19:22):

IE: The collection of sheaves is not a sheaf. I think you need stacks for this, but this starting to bump into the edges of my experience

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

I suppose I mean why are you interested in sheaves, rather than just presheaves, for the type theory?

Reed Mullanix (Mar 25 2020 at 19:26):

At this point, I'm trying to work up to an understanding of the stack models of type theory.

Reed Mullanix (Mar 25 2020 at 19:27):

So this is a step in that direction, albeit one with a bunch of interesting tangents :slight_smile:

Cody Roux (Mar 25 2020 at 21:19):

What's a reference for this? I have never heard of "stack models" in a type theory context...

Cody Roux (Mar 25 2020 at 21:21):

There's probably some deeper connection between all these notions: realizability, normalization proofs, sheaf models and forcing

Nathanael Arkor (Mar 25 2020 at 21:22):

Vinay Madhusudanan (Mar 26 2020 at 04:20):

Thanks for the reference! It's very interesting, and, it seems, at almost the perfect level of comprehensibility for me right now

Alex Kavvos (Mar 26 2020 at 15:18):

it's been my experience over many years that the first 45 pages of this book are by far the hardest. perhaps not conceptually, but definitely a huge obstacle to learning how to work with presheaves - they just lack a lot of intuition

Cody Roux (Mar 26 2020 at 16:52):

Can we remind people what the goal is? I think it was "first 45 pages by Sunday"? I just like to know how far behind I am on my homework :)

Reed Mullanix (Mar 26 2020 at 16:57):

Up to page 48 is the goal, so right up to Ch1, Section 7: Propositional Calculus

Cody Roux (Mar 26 2020 at 17:09):

Morgan Rogers (he/him) (Mar 27 2020 at 09:42):

1) A lot of off-topic stuff in this thread? I don't know what one can do about that.
2) I've read Sheaves in Geometry and Logic, but would love to participate in discussion about it!
3) I made a topos theory stream before finding this topic. I won't suggest that we necessarily migrate this there, but if any deeper topos theory discussions arise that might be a good space for them?

Christian Williams (Mar 27 2020 at 18:02):

Well the Sheaves book covers a lot of material, and I think people are just talking about it generally right now. The current goal is to read up to Chapter I Section 7. So essentially, presheaf categories and some of their nice structure. Some people are trying to do puzzles on it, and solve them in code.

Thanks for making the stream #topos theory . I think people would be fine with migrating over there. Let's just see what people think and then we can make links to bridge them.

Morgan Rogers (he/him) (Mar 27 2020 at 18:27):

Or perhaps make bridges to link them? :rolling_on_the_floor_laughing:
I don't know (ie have not learned, rather than am ignorant to the existence of) the languages that people are using to solve these problems; I hope people also take up John Baez's invitation to stretch their brains before resorting to automated provers so that I might be able to follow the argument they arrive at.

Cody Roux (Mar 27 2020 at 22:06):

No one is using automated provers. Some of us are using proof assistants. It's not exactly solving your problems for you.

Emily Pillmore (Mar 28 2020 at 01:49):

@Reed Mullanix might take a bit to catch up just because of work, but I'm gonna see if i can hit that by mid next week

Reed Mullanix (Mar 28 2020 at 01:50):

Morgan Rogers (he/him) (Mar 28 2020 at 12:51):

Apologies for my mistake, but on the other hand... As someone who hasn't used a proof assistant, what I'm seeing is along the lines of "I put it into a programme and it told me it was a theorem"; how am I supposed to tell the difference?

Morgan Rogers (he/him) (Mar 28 2020 at 12:56):

Jules Hedges (Mar 28 2020 at 13:06):

Automated provers are a different class of software to proof assistants, generally they work with much much weaker logics. Prover9 is a well known automated prover. Most proof assistants also have some automated proving capability added on, eg Coq's auto tactic

Jules Hedges (Mar 28 2020 at 13:08):

Loosely speaking, the user input to an automated prover is the (claimed) theorem, while the user input to a proof assistant is the (claimed) proof

Reid Barton (Mar 28 2020 at 13:19):

And given today's state of technology, usually you have to give a lot more details of the proof to satisfy a "proof assistant" than you would to satisfy a human mathematician.

Morgan Rogers (he/him) (Mar 28 2020 at 13:19):

Reid Barton (Mar 28 2020 at 13:19):

You shouldn't think of it as "assisting" you in producing a proof, but in producing a formalized proof.

Reid Barton (Mar 28 2020 at 13:20):

Another pair of terms is "automatic theorem prover"/"interactive theorem prover" (ATP/ITP).

Morgan Rogers (he/him) (Mar 28 2020 at 13:21):

That sounds like overkill for the problems that one will encounter in Sheaves in Geometry and Logic, but people like to practice their skills and hitting new problems with the tools at their disposal, so it should be fun to see what comes out of it. :grinning:

Reid Barton (Mar 28 2020 at 13:22):

You could also think of it as a tool for checking that the thing you have which you think is a proof really is a proof.

Cody Roux (Mar 28 2020 at 17:25):

Christian Williams (Mar 28 2020 at 18:00):

Morgan Rogers (he/him) (Mar 28 2020 at 18:05):

Cody Roux (Mar 28 2020 at 18:20):

I have actual questions about the first few pages of SiGL: they mention in passing that monos are preserved by pullback, a fact which is somewhat crucial to discussions about subobject classifiers. The proof was a bit finicky, it seemed a bit tougher than usual "diagram chasing". In particular, the fact that it's a limit is crucial, just the fact that the diagram commutes isn't enough.

Reid Barton (Mar 28 2020 at 18:39):

I don't have the book on hand but it seems easy enough to prove directly by diagram chasing

Reid Barton (Mar 28 2020 at 18:42):

Do you mean the fact that a pullback is a limit is crucial, or the fact that you can describe monos in terms of limits?

Joachim Kock (Mar 28 2020 at 18:49):

Two proofs coming to mind are: in cases where there is an epi-mono factorisation system, the fact follows from the fact that right-hand classes of factorisation systems are always stable under pullback (a fact which in turn is easy to establish using the unique-lifting characterisation of factorisation systems). The second argument is that an arrow is a mono iff pullback along itself produces an invertible arrow. This property is easily seen to be preserved under pullback.

Your question 1 is really interesting. I have often thought of that, when category theorists (like real category theorists, not half-baked ones like myself) just seem to know stuff off the top of their head. Obviously I don't know the answer, whether (or to what extent) it is memory or instant understanding, or both. In either case, if you work with something daily, this kind of fact or proof is surely in some sort of cache or proxy in the brain, or whatever it would be called in computer lingo.

sarahzrf (Mar 28 2020 at 18:57):

sarahzrf (Mar 28 2020 at 18:58):

now this raises the question: which lemmas belong in the L1 cache, which in L2, etc?

Cody Roux (Mar 28 2020 at 18:58):

John Baez (Mar 28 2020 at 19:30):

The fact that monos are preserved by pullback is one of those basic things that category theorists know just like group theorists know that if a normal subgroup contains the commutator subgroup, modding out by it leaves you with an abelian group.

One reason that for years I didn't feel like a category theorist is that I hadn't learned lots of these basic facts. In the last few years I've been trying.

Every branch of math has a pile of facts like this. In a way, that's what textbooks are good for.

Alexander Campbell (Mar 28 2020 at 20:17):

Here's how a category theorist would prove this result:
1) monos and pullbacks are defined "representably", so it suffices to prove this result in the category of sets;
2) this result is true in the category of sets.

Joachim Kock (Mar 28 2020 at 20:17):

Just guessing from the names, I would say that Lemma 1 belongs to L1 and Lemma 2 belongs to L2.

Alexander Campbell (Mar 28 2020 at 20:18):

What I mean by "defined representably" in 1) is that a morphism (commutative square) in a category C is a mono (pullback) iff it sent to a mono (pullback) in the category of sets by every representable functor C(X,-).

Alexander Campbell (Mar 28 2020 at 20:20):

This type of argument is second nature to category theorists, so much so that I can't distinguish in my mind between the acts of recalling the result and producing this proof.

Joachim Kock (Mar 28 2020 at 20:24):

Hi Alasdair, this just shows how life is difficult as a category theorist. For a non-category theorist, 2) is enough :-) (which is a nice and short argument, by the way)

Thomas Read (Mar 28 2020 at 20:25):

How does this work? I can't see how to do it this way without just reproducing the usual diagram chasing argument.

Joachim Kock (Mar 28 2020 at 20:27):

All functors preserve invertible arrows. Pullback is a right adjoint, so it preserves limits, hence preserves pullbacks.

John Baez (Mar 28 2020 at 20:29):

I'm not a true category theorist, so I prove that pullbacks preserve monos in any category using a diagram chase - it's no harder than any other little lemma that mathematicians are expected to know.

But I like hearing about slicker methods! I agree that ideally all proofs in category theory would be concatenations of purely verbal arguments, each one individually "obvious".

Thomas Read (Mar 28 2020 at 20:33):

Ah - so we're saying that if we have

f : a \to b

with corresponding element of the slice category

(f) \in C/b

then

f

is mono iff

(f) \times (f) \cong (f)

. And then pullback along

g : c \to b

gives a functor

C / b \to C / c

which is a right adjoint, so preserves limits. So pullback preserves monos.

Cody Roux (Mar 28 2020 at 20:47):

Ah I like this one, because this is how one would prove it in the "internal language" of the category.

Reid Barton (Mar 28 2020 at 20:48):

What all this comes down to is that the easy diagram-chasing argument is the same as the proof in Set, especially if we call the two morphisms into the pullback object "generalized elements".

Reid Barton (Mar 28 2020 at 20:51):

Christian Williams (Mar 29 2020 at 05:58):

I really like this book. I'm not reading linearly at all; I read the first two chapters last quarter (mostly), and now I'm mainly learning about the the internal logic, and the classifying topos.

Any way, how do y'all picture the reading group functioning? I imagine there should be a meeting component. We can generate video calls on Zulip very easily, using the "camera" button below the message box. There wasn't much response to the video-call proposal today, but maybe we can do it another time soon.

Reed Mullanix (Mar 29 2020 at 06:55):

Sorry, I've been a bit busy today, but I definitely think that a meeting would be very valuable :) What time would work best for everyone?

Thomas Read (Mar 29 2020 at 08:38):

Cody Roux (Mar 29 2020 at 15:46):

Reed Mullanix (Mar 29 2020 at 18:08):

Just got up as well, so if anyone wants to do an impromptu discussion, I'm game :)

Christian Williams (Mar 29 2020 at 18:45):

Christian Williams (Mar 29 2020 at 18:46):

Thomas Read (Mar 29 2020 at 18:52):

Christian Williams (Mar 29 2020 at 20:23):

it was great! we'll be meeting again next Sunday around this time, anyone is welcome to join.

Alex Kreitzberg (Mar 29 2020 at 20:24):

Reed Mullanix (Mar 29 2020 at 20:46):

That was great, thanks for all for participating :) For those who missed it, we resolved to finish the rest of chapter 1, and to do exercises 10 and 11

Thomas Read (Mar 29 2020 at 20:58):

I'm wondering if it would actually be a good idea to have a stream just for this - I think it'll get hard to keep track of things if we split into lots of topics mixed into the topos stream

John Baez (Mar 29 2020 at 21:10):

By the way, is it okay if I advertise this reading group on the Azimuth blog, since it connects nicely to my series Topos theory, which is an attempt to explain Sheaves in Geometry and Logic?

Reed Mullanix (Mar 29 2020 at 21:15):

Just following up on the discussion we had about nice proofs that pullbacks preserve monos, here's my version in agda!

module _ (p : Pullback f g) where
  open Pullback p

  pullback-preserves-mono : Mono g → Mono p₁
  pullback-preserves-mono mono a b eq = unique-diagram eq (mono _ _ lemma)
    where
      lemma : g ∘ p₂ ∘ a ≈ g ∘ p₂ ∘ b
      lemma = begin
        g ∘ p₂ ∘ a ≈⟨ extendʳ (⟺ commute)  ⟩
        f ∘ p₁ ∘ a ≈⟨ refl⟩∘⟨ eq ⟩
        f ∘ p₁ ∘ b ≈⟨ extendʳ commute ⟩
        g ∘ p₂ ∘ b ∎

Reed Mullanix (Mar 29 2020 at 21:17):

  unique-diagram :
                   p₁ ∘ h ≈ p₁ ∘ i →
                   p₂ ∘ h ≈ p₂ ∘ i →
                   h ≈ i

And then use the fact that g is a mono, along with some simple commuting around

Cody Roux (Mar 29 2020 at 21:27):

Christian Williams (Mar 29 2020 at 21:27):

we can either make a stream, or maybe a reasonable compromise would be to talk in #topos theory and just prefix the reading group topics with "Sheaves RG". what do y'all think?

Christian Williams (Mar 29 2020 at 21:29):

I think we would be fine with that. Today we had 5 most of the time, and that worked well. But as long as we know what we're discussing and stay on topic (and mute mics), then we can handle more.

Christian Williams (Mar 29 2020 at 21:32):

Today we introduced ourselves, and talked generally about internal logic. Since we're focusing on the first chapter right now, we discussed the equivalence of sieves and subfunctors of representables, and how that gives the subobject classifier for a presheaf topos. Looking at the example for "time-dependent sets", presheaves on

\mathbb{N}^{op}

as @John Baez has discussed on Azimuth, one can get an idea of "generalized truth values" -- rather than something being true or not, it may be true in

n

time steps.

Christian Williams (Mar 29 2020 at 21:33):

We talked some about the "coYoneda lemma" - the fact that every presheaf is a colimit of representables, and the "nerve-realization" adjunction which is described in Section 5. I mentioned that this adjunction is very general, and can be used when defining sheaves and the complementary notion of etale bundle. But we won't get to sheaves yet; we want to get the fundamentals of presheaf categories down first.

Christian Williams (Mar 29 2020 at 21:36):

There was more discussion, connecting the ideas more to programming and type theory. But yeah, don't worry if you couldn't make it to this one; we'll just start again next week. Let us know if that time doesn't work for you.

Cody Roux (Mar 29 2020 at 21:43):

Oh I mentioned something about Kripke models possibly giving intuition. But they're so similar to Sheaves that the difference is somewhat academic.

Thomas Read (Mar 29 2020 at 21:50):

Alex Kreitzberg (Mar 29 2020 at 21:52):

Gershom (Mar 29 2020 at 22:56):

Cody Roux (Mar 30 2020 at 01:21):

I've found van Dalen's "Logic and Structure" to be a reasonable overview. A bit terse though.

nadia esquivel márquez (Mar 30 2020 at 02:21):

Hey i fell behind on the reading and couldn't join today's meeting (or whatever it was). I'll try to join next week, and from what i understand we're just planning on finishing the chapter right?

Philip Zucker (Mar 30 2020 at 03:14):

Morgan Rogers (he/him) (Mar 30 2020 at 09:56):

Would you mind expanding on this? I encountered Kripke semantics in a course on modal logic last year and it struck me that a more general formalisation could be built using sheaves, but your claim about Kripke models seems like a big leap.

Cody Roux (Mar 30 2020 at 12:33):

I guess I misspoke. Sheaves are an obvious generalization of Kripke models, so there's definitely more there. That being said, from the strict point of view of a logician, Kripke models are already sound and complete, as well as enabling a proof of cut-elimination for the sequent calculus LJ, so they're definitely worth studying.

Cody Roux (Mar 30 2020 at 12:35):

However, understanding the ins and outs of the interpretation of intuitionistic logic into Kripke structures is so similar to understanding that of presheaves that it's not clear that there's an advantage, pedagogically, to start with Kripke models.

Reid Barton (Mar 30 2020 at 12:39):

@Reed Mullanix is this part of an Agda category theory library which is available somewhere?

sarahzrf (Mar 30 2020 at 12:42):

sarahzrf (Mar 30 2020 at 12:43):

actually, i guess under typical conventions they're more like (0, 1)-copresheaves

Andrew Hirsch (Mar 30 2020 at 12:48):

Do you have a citation for that? I've been playing with an idea lately that could potentially really benefit from that perspective...

sarahzrf (Mar 30 2020 at 12:50):

errr, sorry, not kripke models of S4, kripke models of propositional intuitionistic logic

sarahzrf (Mar 30 2020 at 12:50):

sarahzrf (Mar 30 2020 at 12:51):

sarahzrf (Mar 30 2020 at 12:52):

sarahzrf (Mar 30 2020 at 12:53):

Andrew Hirsch (Mar 30 2020 at 12:53):

Okay, thanks. Less exiting if it's propositional intuitionistic logic rather than S4 for me.

sarahzrf (Mar 30 2020 at 12:53):

Andrew Hirsch (Mar 30 2020 at 12:54):

Eh, not a big deal. Maybe there's still a connection there, I'd have to think about it. After all, Kripke semantics for intuitionistic logic are connected to modal interpretations

sarahzrf (Mar 30 2020 at 12:54):

the main difference between kripke models for propositional S4 and propositional intuitionistic is whether you restrict yourself to things that are closed under accessibility

sarahzrf (Mar 30 2020 at 12:55):

Andrew Hirsch (Mar 30 2020 at 12:56):

true, so you'd have to do something about the fact that you have two notions of accessibility (the modal notion and the intuitionisitic notion) for intuitionistic S4

sarahzrf (Mar 30 2020 at 12:57):

Andrew Hirsch (Mar 30 2020 at 12:58):

yeah, so you have accessibility (essentially the same as in the model of PIL), and you have a "modal" accessibility relation (what worlds the modal reasoner believes are possible)

Andrew Hirsch (Mar 30 2020 at 12:58):

the thing is how they work together, because you often have to take steps along both relations

Matteo Capucci (he/him) (Mar 30 2020 at 13:22):

There must be a reason if the semantics of higher-order IL is called Kripke-Joyal, after all :grinning_face_with_smiling_eyes:
I came to contact with Kripke models various times and they always seemed quite the same thing as sheaf semantics, although I know little about sheaf semantics but far less about Kripke models.
For one thing, it feels like in a Kripke model

\langle W, R, \Vdash\rangle

, the Kripke frame

\langle W, R \rangle

should play the role of a site (

W

is the 'carrier',

R

the topology), while

\Vdash

should be the forcing relation of the sheaf topos on this site. I suspect the topology here is actually split between

R

and this latter, since from what I understand there can be multiple

\Vdash

on a given frame while the (Kripke-Joyal) forcing relation in a topos is canonically associated to the topos.

Matteo Capucci (he/him) (Mar 30 2020 at 13:23):

I will Google a bit more though, it seems a fruit hanging so low that it's hard to believe nobody repead it yet

Matteo Capucci (he/him) (Mar 30 2020 at 13:50):

Andrew Hirsch (Mar 30 2020 at 13:51):

Cody Roux (Mar 30 2020 at 14:46):

Reed Mullanix (Mar 30 2020 at 18:15):

Reid Barton (Mar 30 2020 at 18:22):

Philip Zucker (Mar 31 2020 at 16:34):

Matteo Capucci (he/him) (Mar 31 2020 at 18:53):

Thomas Read (Apr 03 2020 at 14:48):

On p57 they say "Our discussion of the propositional calculus has indicated that the basic operations

\wedge

\vee

, and

\Rightarrow

of this calculus can all be described as adjoints". How can

\vee

be described as an adjoint, or is this a typo? (I remember something from the bi-Heyting algebra thread about a left adjoint to

\vee

, which certainly doesn't generally exist in a Heyting algebra)

Nathanael Arkor (Apr 03 2020 at 14:56):

the coproduct functor

+ : \mathscr C^2 \to \mathscr C

is left adjoint to the diagonal functor

\Delta : \mathscr C \to \mathscr C^2

(which is left adjoint to the product functor)

Nathanael Arkor (Apr 03 2020 at 14:58):

(this is a special case of a general fact about colimits, diagonal functors and limits)

Thomas Read (Apr 03 2020 at 14:59):

Thomas Read (Apr 03 2020 at 15:01):

Felt like a different flavour to the

a \wedge b \le c \iff a \le b \Rightarrow c

type stuff, but you're probably right.

Nathanael Arkor (Apr 03 2020 at 15:04):

yes, these functors aren't endofunctors, so the adjunctions look a little different to the tensor-hom adjunction

Cody Roux (Apr 03 2020 at 15:05):

Slightly related question: how does the algebraic structure of subobjects relate to the algebraic structure of the ambient category? I feel like if your category has finite limits and colimits, you have a lattice structure, but other than that I'm not sure. When do you have

\Rightarrow

for example? Certainly being an LCCC is enough, but that seems like a lot to ask.

Cody Roux (Apr 03 2020 at 15:12):

Cody Roux (Apr 03 2020 at 15:40):

Unrelated: it took me a minute to realize the category of subobjects of an object

X

is always a poset....

Morgan Rogers (he/him) (Apr 03 2020 at 15:59):

Pullbacks, or even just pullbacks of monos along monos, are enough for intersections, (recall our discussion about pullbacks of monos being monos). Unions are already trickier: in a regular category where one has images, it suffices to have finite coproducts, since the union of

A \hookrightarrow X

and

B \hookrightarrow X

is the image of the canonical map

A \sqcup B \to X

. There is always a maximum element, of course, and having an initial object in your category is sufficient but not necessary to ensure a minimal element in all of the subobject lattices.

Morgan Rogers (he/him) (Apr 03 2020 at 16:04):

As for the Heyting operation, I don't think you can do any better than weakening the conditions on a LCCC, asking only for the exponentials you need for the subobject lattices.

A \Rightarrow B

is precisely local exponentiation, after all.

Cody Roux (Apr 03 2020 at 16:57):

Thanks, Morgan! That clarifies things. Though I would like to have more intuition on the notion of "Regular Category".

Morgan Rogers (he/him) (Apr 03 2020 at 16:58):

A rather dry but very comprehensive early account is in "Categories, Allegories" by Freyd and Scedrov.

Dan Doel (Apr 03 2020 at 17:00):

There was a presentation at the last Compose about 'regular logic' that might be up your alley (not sure if you saw it).

Dan Doel (Apr 03 2020 at 17:01):

I don't recall it being a super clear explanation of regular categories, though, I guess.

Cody Roux (Apr 03 2020 at 17:33):

I did not. I feel like I'm not able to keep up with the raw amount of content getting blasted out there...

Dan Doel (Apr 03 2020 at 17:35):

Dan Doel (Apr 03 2020 at 17:38):

Cody Roux (Apr 03 2020 at 18:13):

John Baez (Apr 03 2020 at 20:24):

I'd be happy to answer "intuition" questions about regular categories, since I feel I know just enough to answer them and not so much that my answers will be extremely sophisticated and therefore incomprehensible.

The crudest intuition is that regular categories are just nice enough so that you can define relations between objects, and compose these relations, just like you can in

\mathsf{Set}

John Baez (Apr 03 2020 at 20:25):

If you think about how composing relations works in terms of logic, you'll see it uses "and" and "there exists".

John Baez (Apr 03 2020 at 20:25):

So "regular logic", the kind of logic that works in regular categories, is a very primitive form of logic that's good at handling "and" and "there exists", and not much else.

Cody Roux (Apr 03 2020 at 20:59):

Morgan Rogers (he/him) (Apr 03 2020 at 23:07):

My Masters "essay" was on this subject; I tried to work out the minimal structure you need to have a well-defined category of relations. It turns out to be very close to regular categories, but you can do better by e.g. not demanding products. One concrete gain I got is that you can define the category of relations for a groupoid, but you might be disappointed to hear that it's just an isomorphic groupoid.

Philip Zucker (Apr 04 2020 at 00:36):

Regular logic seems interesting! I was not aware of regular logic before it came up just now but it seems like a natural fit for thinking about which logical statements of linear inequalities are easily provable via linear programming (and maybe the capabilities of other efficient solvers)? The existential and conjunction are naturally expressed as feasibility and combining constraints. The single allowed outer universal quantifier and entailment corresponds to polytope containment, which is expressible with some duality shenanigans.

John Baez (Apr 04 2020 at 00:38):

@Brendan Fong and @David Spivak would love to talk to you about that. Their categorical approach to regular logic really thinks of it in terms of "constraint satisfaction" and "combining constraints".

John Baez (Apr 04 2020 at 00:46):

John Baez (Apr 04 2020 at 00:47):

Soichiro Fujii (Apr 04 2020 at 01:26):

I think the existence of a strict initial object is sufficient for a minimal element, because it entails that for any object

A

, the unique morphism

0\longrightarrow A

is mono. (An initial object

0

is called strict if every morphism into

0

is an isomorphism.) Without strictness, however, the unique morphism out of

0

may not be mono, as for instance in

\mathbf{Set}^\mathrm{op}

the unique morphism

\{\ast\}\longrightarrow \emptyset

is not mono; in other words, in

\mathbf{Set}

the function

\emptyset\longrightarrow \{\ast\}

is not epi.

As for an explicit counterexample of a category with a (non-strict) initial object in which there is an object

A

with no minimal subobject, consider the full subcategory of the opposite of

\mathbf{Set}^3

consisting of the four objects

A=(2,2,0)

(1,2,0)

(2,1,0)

and

(1,1,1)

Soichiro Fujii (Apr 04 2020 at 01:37):

Um, sorry, maybe we must also add e.g.,

(1,1,2)

for the counterexample to work. It is definitely a very ad hoc example... :sweat_smile:

Philip Zucker (Apr 04 2020 at 02:12):

John Baez (Apr 04 2020 at 02:33):

Yes, it's a nice paper. Evan gave a talk on it at the UCR applied category theory special session in 2017 - slides here.

sarahzrf (Apr 04 2020 at 04:28):

Evan Patterson (Apr 04 2020 at 04:51):

Morgan Rogers (he/him) (Apr 04 2020 at 11:23):

Morgan Rogers (he/him) (Apr 04 2020 at 11:26):

Classifying topos of people learning categorical logic and hopefully some topos theory?

Christian Williams (Apr 05 2020 at 17:34):

Christian Williams (Apr 05 2020 at 17:49):

@Cody Roux @Philip Zucker @Thomas Read @Reed Mullanix @Fatima Afzali @Alex Kreitzberg, and anyone else

Christian Williams (Apr 05 2020 at 17:49):

Or we can push it back some, if the time was not clear. We didn't plan this very officially.

Cody Roux (Apr 05 2020 at 17:50):

Alex Kreitzberg (Apr 05 2020 at 17:51):

Reed Mullanix (Apr 05 2020 at 17:51):

Thomas Read (Apr 05 2020 at 17:52):

Christian Williams (Apr 05 2020 at 17:56):

Christian Williams (Apr 05 2020 at 17:59):

Reed Mullanix (Apr 05 2020 at 18:58):

  BaseChange! : ∀ {B} (f : B ⇒ A) → Functor (Slice B) (Slice A)
  BaseChange! f = record
    { F₀           = λ X → sliceobj (f ∘ arr X)
    ; F₁           = λ g → slicearr (pullʳ (△ g))
    ; identity     = refl
    ; homomorphism = refl
    ; F-resp-≈     = λ eq → eq
    }


  module _ (pullbacks : ∀ {X Y Z} (h : X ⇒ Z) (i : Y ⇒ Z) → P.Pullback C h i) where
    private
      open P C
      module pullbacks {X Y Z} h i = Pullback (pullbacks {X} {Y} {Z} h i)
      open pullbacks

    BaseChange* : ∀ {B} (f : B ⇒ A) → Functor (Slice A) (Slice B)
    BaseChange* f = record
      { F₀           = λ X → sliceobj (p₂ (arr X) f)
      ; F₁           = λ {X Y} g → slicearr {h = Pullback.p₂ (unglue (pullbacks (arr Y) f)
                                                                     (Pullback-resp-≈ (pullbacks (arr X) f) (△ g) refl))}
                                            (p₂∘universal≈h₂ (arr Y) f)
      ; identity     = λ {X} → ⟺ (unique (arr X) f id-comm identityʳ)
      ; homomorphism = λ {X Y Z} {h i} → unique-diagram (arr Z) f (p₁∘universal≈h₁ (arr Z) f ○ assoc ○ ⟺ (pullʳ (p₁∘universal≈h₁ (arr Y) f)) ○ ⟺ (pullˡ (p₁∘universal≈h₁ (arr Z) f)))
                                                                  (p₂∘universal≈h₂ (arr Z) f ○ ⟺ (p₂∘universal≈h₂ (arr Y) f) ○ ⟺ (pullˡ (p₂∘universal≈h₂ (arr Z) f)))
      ; F-resp-≈     = λ {X Y} eq″ → unique (arr Y) f (p₁∘universal≈h₁ (arr Y) f ○ ∘-resp-≈ˡ eq″) (p₂∘universal≈h₂ (arr Y) f)
      }


    !⊣* : ∀ {B} (f : B ⇒ A) →  BaseChange! f ⊣ BaseChange* f
    !⊣* f = record
      { unit   = ntHelper record
        { η       = λ X → slicearr (p₂∘universal≈h₂ (f ∘ arr X) f {eq = identityʳ})
        ; commute = λ {X Y} g → unique-diagram (f ∘ arr Y) f
                                               (cancelˡ (p₁∘universal≈h₁ (f ∘ arr Y) f) ○ ⟺ (cancelʳ (p₁∘universal≈h₁ (f ∘ arr X) f)) ○ pushˡ (⟺ (p₁∘universal≈h₁ (f ∘ arr Y) f)))
                                               (pullˡ (p₂∘universal≈h₂ (f ∘ arr Y) f) ○ △ g ○ ⟺ (p₂∘universal≈h₂ (f ∘ arr X) f) ○ pushˡ (⟺ (p₂∘universal≈h₂ (f ∘ arr Y) f)))
        }
      ; counit = ntHelper record
        { η       = λ X → slicearr (pullbacks.commute (arr X) f)
        ; commute = λ {X Y} g → p₁∘universal≈h₁ (arr Y) f
        }
      ; zig    = λ {X} → p₁∘universal≈h₁ (f ∘ arr X) f
      ; zag    = λ {Y} → unique-diagram (arr Y) f
                                        (pullˡ (p₁∘universal≈h₁ (arr Y) f) ○ pullʳ (p₁∘universal≈h₁ (f ∘ pullbacks.p₂ (arr Y) f) f))
                                        (pullˡ (p₂∘universal≈h₂ (arr Y) f) ○ p₂∘universal≈h₂ (f ∘ pullbacks.p₂ (arr Y) f) f ○ ⟺ identityʳ)
      }

Reed Mullanix (Apr 05 2020 at 19:00):

  unique-diagram : p₁ ∘ h ≈ p₁ ∘ i →
                   p₂ ∘ h ≈ p₂ ∘ i →
                   h ≈ i

Cody Roux (Apr 05 2020 at 19:49):

Variables Z Y : Type.


Variable f : Z -> Y.


Definition P : Type -> Type := fun X => X -> Prop.

Definition f_star : P Y -> P Z :=
  fun S => fun z => S (f z)
.

Definition exists_f : P Z -> P Y :=
  fun S => fun y => exists z, f z = y /\ S z.

Definition forall_f : P Z -> P Y :=
  fun S => fun y => forall z, f z = y -> S z.

Definition subset {X} : P X -> P X -> Prop :=
fun S T => forall x, S x -> T x.

Theorem left_adjoint : forall S T,
  subset S (f_star T) <->
  subset (exists_f S) T.
Proof.
  intros; split.
  - intros; intro; intros.
    destruct H0.
    destruct H0.
    unfold f_star in H.
    rewrite <- H0.
    apply H.
    apply H1.
  - intros.
    intro.
    intros.
    unfold f_star.
    apply H.
    unfold exists_f.
    exists x.
    split; [reflexivity | apply H0].
Qed.

Print left_adjoint.

Theorem right_adjoint : forall S T,
  subset (f_star S) T <->
  subset S (forall_f T).
Proof.
  intros; split.
  - intros; intro; intros; intro; intros.
    apply H.
    unfold f_star.
    rewrite H1.
    apply H0.
  - intros; intro.
    intros.
    unfold forall_f in H.
    unfold subset in H.
    unfold f_star in H0.
    apply H with (x := f x).
    + exact H0.
    + reflexivity.
Qed.

Print right_adjoint.

Cody Roux (Apr 05 2020 at 19:49):

Cody Roux (Apr 05 2020 at 19:51):

But, you can replace Prop with Type to get the version on the slice category of Set (well, Type)

Cody Roux (Apr 05 2020 at 19:51):

Although you might want to prove something stronger than <->, albeit there might be some theorem for free that applies here...

Cody Roux (Apr 05 2020 at 19:52):

It's a bit fun that formalizing the "proof irrelevant" version in Coq gives you the proof relevant version for free...

Thomas Read (Apr 05 2020 at 21:24):

Forgot to ask - why does Proposition 5 (pullbacks preserve colimits) ask for

\mathbf{C}, \mathbf{C}/B'

and

\mathbf{C}/B

to all be cartesian closed? Isn't just

\mathbf{C}/B

cartesian closed enough by the previous prop?

Alex Kreitzberg (Apr 05 2020 at 21:25):

@Christian Williams I wanted to double check I wasn't missing a key intuition for theorem 2 from chapter 9.

Theorem 2, part (Left Adjoint):

\exists_f S \subset U \iff S \subset f^* (U)

The proof sketch you gave in the meeting was:

I didn't know how to quickly make"there exists" into "union". But union being a coproduct seemed like a significant point you wanted to emphasize.

I don't think the proof I made uses the union definition, is that bad? Am I cheating below? My proof:

Theorem 2: For any function

f : Z \rightarrow Y

between sets Z and Y the inverse image functor

f^* : P Y \rightarrow P Z

between subsets has a left adjoint

\exists_f

. That is

\exists_f S \sub U \iff S \sub f^*(U)

Suppose

\exists_f S \sub U

. This is equivalent to

y \in \exists_f S \Rightarrow y \in U

. The set

E_f S

is by definition

\{ y \in Y

| there exists a

z

with

f z = y

and

z \in S \}

. So

y \in \exists_f S \Rightarrow y \in U

gives

Substituting

f z = y

to the left of the then, into the

y

to the right of the then gives:

if we have a

z \in S

then

z \in f^*(U)

. In other words

S \subset f^*(U)

We proved

S \subset f^*(U)

by assuming

\exists_f S \sub U

, so

\exists_f S \subset U \Rightarrow S \subset f^*(U)

Now, suppose x is in

E_f S

, that is, there exists a z in S so that f z = x.
z in S implies, because of condition (*), that f z is in U. Or in other words, x is in U.
This means

E_f S \subset U

.
We proved

E_f S \subset U

assuming

S \subset f^*(U)

, that is, we proved

S \subset f^*(U) \Rightarrow E_f S \subset U

Christian Williams (Apr 05 2020 at 21:33):

Andre Knispel (Apr 05 2020 at 22:45):

Theorem left_adjoint : forall S T,
  subset S (f_star T) <->
  subset (exists_f S) T.
Proof.
  intros. split; intros H x H0.
  - destruct H0 as (x0 & H0 & H1).
    rewrite <- H0.
    apply H, H1.
  - apply H.
    exists x.
    split; [reflexivity | assumption].
Qed.

Theorem left_adjoint' : forall S T,
  subset S (f_star T) <->
  subset (exists_f S) T.
Proof.
  intros. split; intros H x H0.
  - destruct H0 as (x0 & H0 & H1).
    rewrite <- H0.
    apply H, H1.
  - apply H. exists x. auto.
Qed.

Theorem right_adjoint : forall S T,
  subset (f_star S) T <->
  subset S (forall_f T).
Proof.
  intros; split; intros H x H0.
  - intros z H1.
    apply H.
    unfold f_star.
    rewrite H1.
    assumption.
  - apply (H (f x)).
    + exact H0.
    + reflexivity.
Qed.

Theorem right_adjoint' : forall S T,
  subset (f_star S) T <->
  subset S (forall_f T).
Proof.
  intros; split; intros H x H0.
  - intros z H1.
    apply H.
    unfold f_star.
    congruence.
  - apply (H (f x)); auto.
Qed.

Andre Knispel (Apr 05 2020 at 22:50):

I was looking at the previous Coq proofs and felt they were a bit verbose, so I thought I might as well get a little rust off my Coq skills. The theorems with a ' use some light proof automation to skip some easy steps, and the regular version is just the same proof only compacted down a little.

Andre Knispel (Apr 05 2020 at 22:54):

There are probably a few more things that could be done by automation, but I'm happy for now

sarahzrf (Apr 05 2020 at 23:39):

ah, this is the kind of thing you might want to use my depleted CT coq development for, once it's in a place where i'd release it :-)

Cody Roux (Apr 06 2020 at 02:03):

I guess, though this is a ridiculously trivial example. Anything more complex and the pain goes up (locally) exponentially.

Cody Roux (Apr 06 2020 at 02:04):

Christian Williams (Apr 06 2020 at 02:13):

When I care about a theorem, I try to find a canonical proof. Today I was trying to do that for the quantifier adjunctions. It only became clear when I thought of

\exists

as a coend and

\forall

as an end.
quantifiers.png

Christian Williams (Apr 06 2020 at 02:15):

Here we are viewing sets

X, Y

as discrete categories, and subsets as predicates (functors)

U:X\to 2

V:Y\to 2

. Then precomposition by

f

is preimage, and quantification is Kan extension.

Christian Williams (Apr 06 2020 at 02:32):

This is satisfying; but it depends on the fact that you can interpret sets as discrete categories. The equivalence

\mathrm{Set}/X \simeq [X,\mathrm{Set}]

does not even make sense for a general (locally cartesian closed) category. But surely there's a way to continue this nice "universal" version of the story to that level of generality...

Thomas Read (Apr 06 2020 at 06:36):

Where does this

\text{Prop}(\dotsb)

syntax come from? I can follow the proof from context but I don't really get what that means.

Christian Williams (Apr 06 2020 at 17:02):

Yes, sorry I should explain more. We're thinking of sets as "proposition-enriched categories", where instead of hom-sets we have hom-truth values -- which is true if the two elements are equal, and false otherwise.

Christian Williams (Apr 06 2020 at 17:04):

So you can read

\forall y \; \forall x \; \mathrm{Prop}(Y[f(x)=y],2[U(x)\Rightarrow V(y)])

as
"for all

y

, for all

x

, if

f(x)=y

, then if

x\in U

then

y\in V

Morgan Rogers (he/him) (Apr 06 2020 at 18:35):

Christian Williams (Apr 08 2020 at 00:23):

@Ryan Wisnesky I understand that there is an analogy between

\mathrm{Lan}

and

\Sigma

\mathrm{Ran}

and

\Pi

; but so far the only way that we're understanding it as an actual generalization is in the case of

\mathrm{Set}

. do you or @Mike Shulman or anyone else know how to make the generalization precise for an arbitrary LCCC?

Christian Williams (Apr 08 2020 at 00:24):

Maybe it's not so good to bring the discussion back here either... but oh well; this Sunday we were talking about quantifiers as adjoints, so it's relevant.

Nathanael Arkor (Apr 08 2020 at 00:25):

presumably you want something stronger than "

\Sigma

is a left adjoint, which can therefore be written as a left Kan extension"?

Christian Williams (Apr 08 2020 at 00:27):

Yes, a deeper connection. A conceptually clear, unbroken chain of generalization from

\vee, \wedge

\exists, \forall

\mathrm{Lan}, \mathrm{Ran}

which includes the general

\Sigma

and

\Pi

Mike Shulman (Apr 08 2020 at 00:28):

Well, the case of Set can be repeated essentially verbatim for any LCCC by talking about Kan extensions between presheaves on internal categories. Is that what you want?

Christian Williams (Apr 08 2020 at 00:31):

This sounds great and I need to work it out for myself. I don't yet see how this gives

\Sigma

and

\Pi

. But, given any

f:a\to b

C

we have the triple adjoint; what if

a

and

b

are internal categories only trivially?

Christian Williams (Apr 08 2020 at 00:36):

Do you mean that when

c\in C

is an internal category, the category of internal presheaves on

c

is equivalent to the slice category over

c

? (Hm, no because there can be many category structures on

c

Christian Williams (Apr 08 2020 at 00:45):

Looking through the "internal category theory" chapter of Jacobs' Categorical Logic; probably in here.

Mike Shulman (Apr 08 2020 at 00:52):

Close: the category of internal presheaves over a discrete internal category is equivalent to the corresponding slice category.

Cody Roux (Apr 09 2020 at 00:54):

Here's a question that came up in the reading group last week, and I just want to jot it down to see if anyone has any thoughts: why is it useful to consider the category of presheaves over

C

as the free cocompletion of

C

? What's special about colimits that we want them all, and why is having the free such device useful? In particular, there is no clear relation between these new colimits and the old colimits of

C

Soichiro Fujii (Apr 09 2020 at 02:40):

I think one answer is because this universal characterization leads to the nerve and realization construction. For any small category

\mathcal{C}

and any locally small cocomplete category

\mathcal{E}

, to give a functor

\mathcal{C}\longrightarrow \mathcal{E}

is equivalent (by this characterization) to give a cocontinuous (= small-colimit-preserving) functor

[\mathcal{C}^{\mathrm{op}},\mathbf{Set}]\longrightarrow \mathcal{E}

, which in turn is equivalent (by an adjoint functor theorem) to give a left adjoint functor

[\mathcal{C}^{\mathrm{op}},\mathbf{Set}]\longrightarrow \mathcal{E}

(“realization”; its right adjoint is “nerve”).

Mike Shulman (Apr 09 2020 at 03:33):

In fact the freeness of the presheaf category means that there is no relation between the new colimits and the old ones of C, in as strong a sense as possible: the only colimits that are preserved by the Yoneda embedding are the absolute ones, those that are preserved by any functor whatsoever for purely diagrammatic reasons.

Mike Shulman (Apr 09 2020 at 03:35):

You can, however, force the Yoneda embedding to preserve any particular colimits you like in C, by restricting to the subcategory of presheaves that preserve those colimits. This is described (among other places) in section 3.12 of Kelly's book.

Mike Shulman (Apr 09 2020 at 03:37):

One way to motivate the free cocompletion is to think of colimits as analogous to sums in algebra. Then the free cocompletion (i.e. presheaf category) of a category C is analogous to the free abelian group (or module) on a set. Not every module is free, but the free ones are very important, not least because any module admits a presentation as a quotient of a map between free modules. Similarly, any locally presentable category admits a presentation as a sort of "colimit" of presheaf categories.

John Baez (Apr 09 2020 at 05:32):

Here's a nice example of the analogy Mike pointed out between the free abelian group

\mathbb{Z}[S]

on a set

S

and the free cocompletion

\hat{C}

of a category

C

. If

M

is a monoid then the multiplication on

M

extends to a bilinear map

making

\mathbb{Z}[M]

into a ring, the monoid ring of

M

. (The case where

M

is a group is the most famous, and then we speak of the 'group ring'). Following the analogy, we see that if

C

is a monoidal category

\hat{C}

becomes a monoidal category where the tensor product is cocontinuous in each argument. The tensor product on this monoidal category is called Day convolution.

Thomas Read (Apr 09 2020 at 07:16):

Thanks everyone - this is something that confused me until quite recently, and these explanations have really helped finish sorting out my mental models.

When I first heard "free cocompletion" without knowing what it meant, I assumed that it would mean adding in all the colimits that don't exist in

\mathbf{C}

but leaving the ones that do exist alone... which is very wrong for colimits, but actually a fairly accurate description of what the Yoneda embedding does to limits!

Thomas Read (Apr 09 2020 at 07:43):

Does anyone have a reference for proving that a colimit is absolute iff it is preserved by Yoneda? I've found the result mentioned in several places (e.g. https://ncatlab.org/nlab/show/absolute+colimit) but no details of a proof beyond "because it's the free cocompletion"

Oscar Cunningham (Apr 09 2020 at 08:31):

Thomas Read (Apr 09 2020 at 08:31):

Oscar Cunningham (Apr 09 2020 at 08:32):

Like 'The Yoneda embedding is universal among completions that preserve all limits'?

Thomas Read (Apr 09 2020 at 08:32):

Thomas Read (Apr 09 2020 at 08:34):

Oscar Cunningham (Apr 09 2020 at 08:36):

I guess Mike Shulman's reference to Kelly's book should give the answer, but I'm not understanding section 3.12 on its own, and I don't want to read an entire enriched book to get the

\mathbf{Set}

answer.

Thomas Read (Apr 09 2020 at 08:58):

Yeah same. This happens to me enough that I probably just need to learn enriched category theory properly someday....

Paolo Capriotti (Apr 09 2020 at 09:18):

I don't know a reference, but the proof is pretty simple. A cocone is colimiting if and only if every representable presheaf maps it to a limiting cone. A colimiting cocone being preserved by Yoneda corresponds the stronger fact that every presheaf maps it to a limiting cone.

Now, let

F : \mathcal A → \mathcal B

be a functor, and

X → L

a colimting cocone in

\mathcal A

preserved by Yoneda. Then for any representable presheaf

P

\mathcal B

, the induced presheaf

F^*P = PF

\mathcal A

turns the colimit into a limit

PFL → PFX

. Therefore

FX → FL

is a colimiting cocone.

Note that we haven't used that

P

is representable, so this argument shows that

FX → FL

is also preserved by the Yoneda embedding of

\mathcal B

, which is also easy to see directly.

Thomas Read (Apr 09 2020 at 10:00):

Christian Williams (Apr 12 2020 at 17:59):

I need to be writing today, but I hope y'all still meet and let me know what you cover.

Thomas Read (Apr 12 2020 at 20:08):

Maybe Easter was a bad choice of day :hatching_chick: :hatching_chick:
How are people getting on with the material? Do we want to find another time or wait till next Sunday?

Cody Roux (Apr 13 2020 at 14:51):

I was going to ask: did the meeting happen? I think Sunday is fine, as long as we expect a couple of duds on Easter and Christmas or whatever.

Reed Mullanix (Apr 13 2020 at 20:24):

Stelios Tsampas (Apr 13 2020 at 20:26):

Anton Lorenzen (Apr 13 2020 at 21:02):

How far did you get? I am currently at the beginning of the second chapter and reading one section a day (a bit late to the party I guess :))

Christian Williams (Apr 13 2020 at 21:49):

Just wanted to clarify -- here you're talking about forming

Cat(C)

as a proarrow equipment, using the adjoints-to-composition to define co/limits, and hence internal Kan extensions, correct?

Christian Williams (Apr 13 2020 at 21:49):

Also, did we ever decide whether we wanted to start our own stream or merge with #theory: topos theory ?

Thomas Read (Apr 14 2020 at 08:14):

The plan for last Sunday had been to get up to the end of chapter 2 section 4. Since that meetup didn't happen I'm not sure if we'll try to get a little further by this Sunday or not, but either way sounds like you'll be caught up by then!

Anton Lorenzen (Apr 19 2020 at 08:23):

The second chapter was a bit harder and we (me and a friend) only made it to the end of section 6. How are you progressing?

Thomas Read (Apr 19 2020 at 10:34):

Christian Williams (Apr 19 2020 at 17:21):

Christian Williams (Apr 19 2020 at 17:27):

Thomas Read (Apr 19 2020 at 17:44):

Christian Williams (Apr 19 2020 at 18:02):

Christian Williams (Apr 19 2020 at 18:39):

Thomas and I talked about Ch. 2; everything was fine because we knew about the nerve-realization form of the adjunction between presheaves and bundles. Now we're wondering whether the same can be done for general Grothendieck topologies -- does anyone know?

Besides that question, we decided to go on to Ch. 4 First Properties of Elementary Topoi, to get on to the logic. Let us know if that works for you.

Cody Roux (Apr 19 2020 at 21:40):

Sounds good, though I had mentioned wanting to get the basics of Sheaves at some point...

Cody Roux (Apr 19 2020 at 21:41):

Also: since sheaves over a general Grothendiek topology are a subcategory of presheaves, is there anything else to add to the construction?

John Baez (Apr 19 2020 at 21:57):

Over spaces we have a nice equivalence between "etale spaces over X" and "sheaves on X", which Mac Lane and Moerdijk obtain by restricting the adjunction between "bundles over X" and "presheaves on X", so I think Christian is asking how much of this persists in the case of general Grothendieck topology.

John Baez (Apr 19 2020 at 21:57):

All I can say is that I haven't seen anyone try to define bundles over a category with a Grothendieck topology.

sarahzrf (Apr 19 2020 at 22:06):

Gershom (Apr 19 2020 at 23:04):

John Baez (Apr 19 2020 at 23:16):

Nice! But this is actually the concept of fiber bundle over an object in a site.

John Baez (Apr 19 2020 at 23:18):

Thomas Read (Apr 20 2020 at 08:41):

I'd forgotten we hadn't actually finished chapter II yet - do people want to move straight on to logic, or should we finish chapter II + do some exercises and then decide next week?

Morgan Rogers (he/him) (Apr 20 2020 at 09:05):

@Riccardo Zanfa and I tried to do this just over a year ago, and it was one of the routes into this analysis, which it seems @Chaitanya Leena Subramaniam and Mathieu Anel have taken to much further than we did. I think that someone trying to get a concrete understanding of their paper could certainly try to put their results in geometric terms.

Anton Lorenzen (Apr 20 2020 at 14:30):

I am not sure how much time I'll have this week, but I could commit to reading three sections.. So maybe we set 4.3 as a goal and those with time and interest can do the rest of chapter two?

Cody Roux (Apr 21 2020 at 00:30):

Thomas Read (Apr 22 2020 at 18:35):

The idea is that you show that the limit of a diagram consisting of "baseable" objects (i.e. objects

X

such that

X^Y

exists for all

Y

) is itself baseable. Then for any object

X

in a topos we have an equalizer diagram that looks like

X \rightarrowtail PX \rightrightarrows \Omega

(where

X \rightarrowtail PX

is what Mac Lane and Moerdijk call the "singleton arrow"

\{\cdot\}_B

). And

PX

and

\Omega

are baseable so we find that

X

is baseable.
More explicitly we get that

X^A

is the equalizer of a diagram that looks like

P(X \times A) \rightrightarrows PA

since

P(X)^A \cong P(X \times A)

and

\Omega^A \cong PA

. It ought to be fairly straightforward to show this is just another way of writing the definition that Mac Lane and Moerdijk find.

Morgan Rogers (he/him) (Apr 23 2020 at 11:10):

Having covered up to the end of Chapter III, anyone in this reading group has enough background to read my paper with @Jens Hemelaer ; perhaps some of you will find it interesting :wink:

Ryan Wisnesky (Apr 25 2020 at 00:17):

@Christian Williams I'm afraid my knowledge of Kan extensions is completely confined to Set

Cody Roux (Apr 26 2020 at 17:10):

Henry Story (Apr 26 2020 at 17:14):

I was just reading about sheaves in Goldblatt's Topoi.
(Got stuck for a while on

Sub(1) \cong \mathcal{E}(1,\Omega)

saying the subobjects of 1 are isomorphic to the set of functions into Omega, when I realized that there is the function

0: 0 \to 1

that is always around)

Thomas Read (Apr 26 2020 at 17:48):

We usually do the meeting about 15 minutes from now, if no one has strong preferences to the contrary

Thomas Read (Apr 26 2020 at 17:52):

@Cody Roux @Philip Zucker @Christian Williams @Reed Mullanix @Fatima Afzali @Alex Kreitzberg @Stelios Tsampas @Anton Lorenzen @nadia esquivel márquez or anyone else who wants to join

Reed Mullanix (Apr 26 2020 at 17:54):

Henry Story (Apr 26 2020 at 18:00):

Thomas Read (Apr 26 2020 at 18:03):

Do people want zoom or jitsi? (I only have a free zoom account so if we do that might be best if someone else sets it up)

Reed Mullanix (Apr 26 2020 at 18:05):

Thomas Read (Apr 26 2020 at 18:05):

Reed Mullanix (Apr 26 2020 at 18:09):

Thomas Read (Apr 26 2020 at 18:10):

Thomas Read (Apr 26 2020 at 18:11):

Thomas Read (Apr 26 2020 at 21:20):

Brief summary of the meeting:
We started by talking about Chapter II. We discussed the definition of a sheaf and motivation for this being an important concept. We considered the intuition for sheafification and basic examples. We then moved on to the beginning of Chapter IV, and talked about the various different definitions of an elementary topos. We also discussed good examples to keep in mind of non-Boolean toposes.

Next time the plan is to read up to Chapter IV Section 6. People seem especially interested in understanding the Beck-Chevalley condition.

Henry Story (Apr 26 2020 at 21:27):

I pointed to Goldblatt's much more introductory book Topoi: The Categorical Analysis of Logic which I was just reading a chapter on sheaves on.
I mentioned complement Topoi and their relation to closed topological sets and falsificationist logic as discussed in the bi-Heyting algebra thread in this forum.
I asked if Sheaves were related to HoTT, where I came across the concept too, and tried to understand it by writing up a blog, but apparently HoTT needs pre-sheaves in order to fit in with HoTT's concept of Universes.
I wondered where exponentials come up in Topoi (that was what I was researching today thinking they would come in the definition of implication. But apparently they are more likely to come in at the level of quantification. So I need to look there.)
An example of a topology may be to look at recursively enumerable sets. Another example to look at is the realizability topos.
Thanks, it was very helpful to see how these concepts are intuited by different people and to see what uses others are making of them.

Anton Lorenzen (Apr 26 2020 at 21:42):

That sounds nice! I missed it unfortunately, but I am going to try to take part next week. Will the next meeting also be around 8 pm Berlin time on Sunday (like today?)

John Baez (Apr 27 2020 at 03:55):

I would like to talk about Beck-Chevalley, because that's one of the subtler aspects of this game.

Christian Williams (Apr 28 2020 at 04:56):

John Baez (Apr 28 2020 at 05:55):

Probably. I'll either be there or I won't.... don't worry about me. What material on Beck-Chevalley are you trying to cover? The stuff in Sheaves in Geometry and Logic, or something else too?

Cody Roux (May 03 2020 at 17:37):

Cody Roux (May 03 2020 at 17:38):

I could also use a bit of intuition on Beck's theorem, right now I don't get it at all

Thomas Read (May 03 2020 at 17:50):

Reed Mullanix (May 03 2020 at 17:50):

Thomas Read (May 03 2020 at 17:51):

@Cody Roux @Philip Zucker @Christian Williams @Reed Mullanix @Fatima Afzali @Alex Kreitzberg @Stelios Tsampas @Anton Lorenzen @nadia esquivel márquez @John Baez etc

Reed Mullanix (May 03 2020 at 17:51):

Cody Roux (May 03 2020 at 17:57):

Dan Doel (May 03 2020 at 17:58):

@Cody Roux I'm not an expert, but you might want to look at this, which seems related to me.

E.G. I think it might be saying that D is (equivalent to) a category of algebras on objects of C iff it has free algebras (left adjoint) and it has all algebras presentable by generators and relations.

Thomas Read (May 03 2020 at 17:59):

Dan Doel (May 03 2020 at 17:59):

Reed Mullanix (May 03 2020 at 18:00):

Christian Williams (May 03 2020 at 18:00):

Thomas Read (May 03 2020 at 18:01):

Cody Roux (May 03 2020 at 18:01):

Cody Roux (May 03 2020 at 19:31):

So: one of my big questions coming out of this is: what is a good reference for an internal logic of toposes? The ideal reference for me would do this in a style as close as possible to the classical ZF/IZF/CZF presentation, rather than, e.g. what can be found here: https://ncatlab.org/nlab/show/fully+formal+ETCS#the_theory_of_elementary_toposes which is still very categorical in flavor.

Cody Roux (May 03 2020 at 19:38):

sarahzrf (May 03 2020 at 19:45):

Cody Roux (May 03 2020 at 19:49):

We're getting to that next. Something that is troublesome though, is that the current chapter is taking a quite nuclear approach to proving that finite colimits exist, as well as exponentials, whereas it seems like working within some logical internal language would be astronomically easier for some poor logician like myself. It's not clear however, that the version of the Mitchell-Benabou language in the book can even be defined before doing all this tough leg work.

sarahzrf (May 03 2020 at 19:52):

sarahzrf (May 03 2020 at 19:53):

i constantly write shit down pointfully, sometimes even do set comprehension, when ive literally never worked thru the details of interpreting something like mitchell-benabou :upside_down:

sarahzrf (May 03 2020 at 19:53):

Henry Story (May 03 2020 at 20:35):

He uses the term

\Omega

to denote those.
I did not get that far into reading the thesis. But it could be interesting to this group as it seems to involve topoi.

sarahzrf (May 03 2020 at 20:48):

Thomas Read (May 03 2020 at 21:08):

BTW plan for next week is to read the couple sections later on in the book on the Mitchell-Bénabou language and Kripke Joyal semantics, as well as maybe skim the rest of Chapter IV.

John Baez (May 03 2020 at 21:36):

Sorry, I was busy. I'm not sure "explaining" Beck-Chevalley is something I can do at this point, more like "assembling lots of facts about it in hopes of getting a really clear explanation". I'd be happy to discuss it here. I'm not so good at video meetings.

Thomas Read (May 03 2020 at 21:48):

I'd love to hear about it here! At the moment I get the impression from other people that it's important, but I'm not really sure how to think about it or why I should care about it

John Baez (May 03 2020 at 21:53):

At present I think of a Beck-Chevalley as an "unexpected relation between inverse images and direct images, that you might not have noticed if you weren't paying careful attention". It shows up in lots of contexts.

John Baez (May 03 2020 at 21:59):

Here's a basic one. Suppose you have a map of sets

f : S \to T

. Then you have the usual "inverse image" map sending subsets of

T

to subsets of

S

John Baez (May 03 2020 at 22:00):

Now, if you have a commutative square of maps between sets... ugh, something like

D ----> C
|       |
v       v
B ----> A

John Baez (May 03 2020 at 22:02):

You can take their inverse image and then their image, or take their image and then take their inverse image!

John Baez (May 03 2020 at 22:03):

In other words, you can go up and then to the right, or to the right and then up.

John Baez (May 03 2020 at 22:03):

Puzzle 1 (for beginners only). Find an example where the results are not the same.

John Baez (May 03 2020 at 22:05):

However, if our commutative square is a pullback square, the results are always the same!

Puzzle 2 (for beginners only). Show that if our square is a pullback square in Set we get the same thing if we take any subset of B and

John Baez (May 03 2020 at 22:08):

Was all this too obvious, @Thomas Read? This is the basic idea of Beck-Chevalley - it's an example of a general pattern. This probably don't explain why it's important, but basically you can count on anything so simple as this being important if it's not an instant consequence of other simple things.

Thomas Read (May 04 2020 at 06:50):

No, that helps! Thanks! I'd only seen the first version stated in the book, which insists that two of the maps are monos - I'm much happier with this symmetric version.

Thomas Read (May 04 2020 at 07:13):

So in Set I think (slight spoiler for @John Baez 's question below)
.
.
.
.
.
the Beck Chevalley condition holds for a commuting square iff the canonical map

D \to B \times_A C

is surjective, which in Set is the same as asking that the square is a weak pullback. I don't know whether any of that generalises to other toposes?

Morgan Rogers (he/him) (May 04 2020 at 08:03):

The reason for going through all this legwork is really independent of the logical or geometric content of toposes: it's showing that in order to have all of the properties/structure of a topos, we only need to verify a minimal amount, and the remainder is automatic. It's possible some of the proof of that fact could be done by other means; a higher logic interpretation of the power object adjunction might be interesting! But if you're happy to accept or assume that the structure is there already, or if you can show it's there by other means, then you can get straight into the logic without worrying about it.

Cody Roux (May 04 2020 at 14:57):

I agree, but my question is: does this legwork involve defining exponentials and colimits first? Otherwise I'd be happy to do that once I have a thing that's close to a set theory, just by doing the usual logical constructions.

Henry Story (May 04 2020 at 15:20):

I decided illustrate a subobject of an RDF graph in the topos of graphs (using A Guided Tour in the Topos of Graphs for help).
Here the arrows are named by triples

\langle subject, relation, object \rangle

and the objects are the first and third projections, so we have a graph given by

In the illustration I avoided the duplication by just naming the arrows with the relation.
GraphTopos.jpg

Henry Story (May 04 2020 at 15:28):

This is different from RDF graph homomorphisms (see Benjamin Braatz's thesis), of which there are a few different ones. The simples one

\mathsf{RDFHom}

keeps the literals in square brackets and the nodes names with URIs fixed, whereas simple Graph homomorphisms don't make that distinction. Interestingly @Ryan Wisnesky had to re-structure the work on Functorial Databases in order to avoid his inferencing engines just collapsing isomorphic graphs even though the literals were distinct -- for just that reason.

Henry Story (May 04 2020 at 15:38):

Now I am wondering what is the opposite of the Category of Graphs?
Is it that the opposite of a category that is a Topos is always a category of homomorphisms between objects that are Heyting lattices of subobjects from the topos?
(I am extrapolating from

\mathsf{Set^{op}} \cong \mathsf{CABA}

)

Morgan Rogers (he/him) (May 04 2020 at 15:42):

What do you mean by "defining"? It's being shown that those things exist given only finite limits and power objects; we could just take our definition of a topos to include finite colimits and exponentials, but the point is that we get these things for free. If you don't care about starting from the most efficient possible definition, then none of this legwork is necessary, you can just work under the assumption that they're there :wink:

Ryan Wisnesky (May 05 2020 at 01:18):

Indeed @Henry Story this is a key point for applied category theorists to remember: when you are treating sets as data in CS applications, equality on the nose can matter, and constructions that are only defined up to isomorphism may be too lose to be practical if used naively. The first time we ran a left Kan extension in CQL data such as 'Bill' and 'Alice' did indeed disappear, replaced by autogenerated identifiers in an isomorphic way, and it caught us off guard, despite being so obvious in retrospect. We then had to add additional structure on categories to preserve these 'attributes' during data migration, triggering all the papers with David Spivak

Henry Story (May 05 2020 at 07:03):

I was catching up on reading "Shaves in Geometry and Logic", which oddly misses out on the topos of graphs. Reading chapter 1, a Topos is strongly related (identified?) with the Category of Functors

\mathbf{Set}^{\mathsf{C}^{\mathrm{op}}}

. This is so close to Spivak's functorial Databases which are functors

\mathbf{Set}^\mathsf{C}

where

\mathsf{C}

is a small category playing the role of a schema. Why does this

^{\mathrm{op}}

appear here when thinking about topoi?
(The article Relational foundations for functorial data migration I think is the article that first looks at how to add typing to a DB schema instance so as to pin down certain types)

Pastel Raschke (May 05 2020 at 09:20):

[Cop, Set] are the (Set-valued) presheaves, [C, Set] are the (Set-valued) copresheaves

space and quantity is a very deep and somewhat bewildering rabbit hole, one of the major contributions of category theory. isbell duality etc. check out yoshihiro maruyama's work.

generic figures and their glueings is a very good (free!) introduction to presheaf toposes (from what i've heard). described as a stepping stone to sheaves in geometry and logic. six visualizable examples follow you through the book.

Morgan Rogers (he/him) (May 05 2020 at 09:34):

Not quite. Presheaf toposes form a subclass of Grothendieck toposes, which form a subclass of elementary toposes. They're one of the easiest classes of topos to work in, and every Grothendieck topos is a subtopos of a presheaf topos. This is why they're introduced first.
Henry Story said:

We want the Yoneda embedding to be covariant: each object

c

gives a representable presheaf

Hom_C(-,c)

Morgan Rogers (he/him) (May 05 2020 at 09:36):

Sometimes it can be more convenient to work covariantly and think of the resulting topos of copresheaves as "presheaves over

C^{\mathrm{op}}

", though.

John Baez (May 05 2020 at 15:46):

This is an interesting question: can we generalize the usual result $\mathsf{Set^{op}} \cong \mathsf{CABA}$ to an arbitrary topos in a nice way?

John Baez (May 05 2020 at 15:47):

Is there an analogue of a complete atomic Boolean algebra in a general topos

\mathsf{T}

, such that

\mathsf{T}^{\rm op}

is equivalent to the category of these?

Cody Roux (May 05 2020 at 16:44):

Seems unlikely, given how messy the Heyting algebra

\Omega

is in a general intuitionistic set theory (it doesn't even have to be a set!).

Cody Roux (May 05 2020 at 16:45):

Cody Roux (May 05 2020 at 16:47):

But the natural intuition of: "atoms of

P(A)

are sets

\{a\}

for every

a\in A

" definitely doesn't fly here, since there a lot of subsets of

\{a\}

in general.

Morgan Rogers (he/him) (May 05 2020 at 16:47):

@Cody Roux haven't you already gotten to Section 5 of Chapter IV in the reading group?

Cody Roux (May 05 2020 at 16:48):

Morgan Rogers (he/him) (May 05 2020 at 16:49):

Cody Roux (May 05 2020 at 16:49):

Morgan Rogers (he/him) (May 05 2020 at 16:49):

That is,

\mathcal{E}^{\mathrm{op}}

is equivalent to the category of algebras of some monad on the topos

Cody Roux (May 05 2020 at 16:50):

Morgan Rogers (he/him) (May 05 2020 at 16:51):

I'm saying that in principle one could extract a theory describing what those algebras are, albeit a general construction would have to be indexed over the topos.

Cody Roux (May 05 2020 at 16:51):

Morgan Rogers (he/him) (May 05 2020 at 16:52):

Cody Roux (May 05 2020 at 16:52):

Cody Roux (May 05 2020 at 16:53):

Morgan Rogers (he/him) (May 05 2020 at 16:54):

I'm not claiming to have provided a comprehensive answer, but seeing

\mathcal{E}^{\mathrm{op}}

as monadic over

\mathcal{E}

makes an affirmative answer seem less of a stretch, I think :innocent:

John Baez (May 05 2020 at 16:56):

Yeah, I think that @Mike Shulman and/or the nLab talks about a generalization of the double powerset functor for any topos

\mathsf{T}

that acts as a monad whose algebras give

\mathsf{T}^{\rm op}

John Baez (May 05 2020 at 16:57):

John Baez (May 05 2020 at 16:59):

Morgan Rogers (he/him) (May 05 2020 at 17:01):

Aha! My argument vindicated! :stuck_out_tongue_wink:
It's worth noting that a similar thing will work whenever the functors appearing in Isbell duality are monadic, which yields relativised versions of this construction for any expression of a topos as internal presheaves over a base topos. I wonder how far this can be taken.

Morgan Rogers (he/him) (May 05 2020 at 17:04):

@Olivia Caramello has done a lot of work on using toposes to obtain and study dualities. She might have some further insights to share, or some references about this.

Henry Story (May 05 2020 at 17:23):

My thought was more as follows: 1) the subobjects of a any object in a topos T form a Heyting lattice (actually a hefting algebra, but that forms something that is an extended lattice as far as I understand) 2) so perhaps

T^{op}

is a category given by the functor

^{op}

that maps objects x of T to their Heyting "lattice". The

T^{op}

would then have as objects Heyting lattices and as morphism the morphisms between such "lattices". There is no requirement that there be atoms of the heyting lattice. I was admittedly trying to generalizing from one case. ;-)

Morgan Rogers (he/him) (May 05 2020 at 17:42):

Oh actually that was recommended by @Pastel Raschke, but it looks like a reasonable gentle introduction to me too :grinning_face_with_smiling_eyes:

Olivia Caramello (May 06 2020 at 05:29):

@John Baez With @Riccardo Zanfa we are currently writing a paper on stacks and relative toposes where we establish, among (many) other things, for any small-generated site (C, J), an adjunction between the category of C-indexed categories and that of toposes over Sh(C, J), which generalizes the classical presheaf/bundle adjunction. This sends, on the one hand, a C-indexed category to the topos of sheaves on the domain of the corresponding fibration with respect to the Grothendieck topology on it lifted from the base (a topology originally introduced by Giraud in the context of stacks, which can also be characterized as the smallest Grothendieck topology which makes that fibration a comorphism of sites to (C, J)), and, on the other hand, a topos E over Sh(C, J) to the C-indexed category sending each object c of C to the category of geometric morphisms over Sh(C, J) from the relative topos Sh(C, J)\slash l(c) (where l is the canonical functor from C to Sh(C, J)) to E. Once we have completed this work, I will make sure to inform you.

Olivia Caramello (May 06 2020 at 05:57):

The monadic approach to Stone-type dualities is well presented in section VI.4 of Johnstone's book Stone spaces, and can clearly be generalized to the setting of an arbitrary base topos. Also my approach to the construction of this kind of dualities via 'bridges', introduced in this paper, can be generalized to arbitrary base toposes, since the tecniques employed in it are pointfree and constructive.

Henry Story (May 09 2020 at 18:42):

Have been away 4 days doing administrative tasks and found 650 new messages here :-)

That book is very helpful. In the time I had remaining I been reading it very careful, to make sure I understand the new notation. So I am only at page 40. It is just the right level for me.

It looks like I had some good intuitions about gluing and RDF when I wrote this blog post on Data and Interpretation where this image comes up Bob.jpg (which is a gluing of an image onto another)

Henry Story (May 09 2020 at 21:00):

For those with a historical/philosophical interest, The End of the Metaphysics of Being and the Beginning of the Metacosmics of Entropy Daniel Ross traces evolutionary thinking back to the presocratic Empedocles who 2500 years ago, conceived of the world as arising by chance and evolving randomly. He imagined randomly arising body parts (eg. eyes, and arms) being glued to other body parts in order to create the creatures that we see.

John Baez (May 09 2020 at 23:32):

What does this have to do with the reading group on Sheaves in Geometry and Logic? It makes sense to keep this particular discussion tightly focused on questions that come up when people are studying that book.

Henry Story (May 10 2020 at 05:42):

Pastel Raschke (May 10 2020 at 09:49):

liveblogging generic figures should probably go in its own topic, maybe in the topos or general stream

Thomas Read (May 10 2020 at 17:33):

I'm not going to be able to make it to the meeting today - if someone can post a brief summary of what happens that would be great!

Thomas Read (May 10 2020 at 17:34):

Also I arbitrarily nominate @Reed Mullanix to start the video call if he's around

Cody Roux (May 10 2020 at 17:37):

Reed Mullanix (May 10 2020 at 17:42):

Henry Story (May 10 2020 at 17:51):

I don't think that leaves anyone over. Which is fine, as it will give me time to catch up (if that still is possible).

Joachim Kock (May 11 2020 at 22:18):

I like to look at the Beck-Chevalley for slice categories of Set like this: It is the categorical analogue of the basic fact in linear algebra that composition of linear functors is given by matrix multiplication.

To see this, note that slice categories are the objective analogue of vector spaces: a vector space spanned by S is a linear combination of elements in S, i.e. a (finite) family of scalars indexed by S. (The word finite should be put in many places, let's ignore that.) Similarly, an object in the slice category Set/S is a family of sets indexed by S. Just as the vector space on S is the linear-combination completion of S, the slice category is the sum-completion. A linear functor is a functors Set/S -> Set/T that preserves sums. One shows that these are given by spans S <- M -> T by pullbacks and postcomposition.

Beck-Chevalley says that: composition of linear functors is given by pullback composition of spans.

Joachim Kock (May 11 2020 at 22:20):

(People often say that Span(Set) is a categorification of Vect. I agree of course, but I would rather say that it is a categorification of matrix algebra, and that the actual categorification is the category of slice categories and linear functors. They are equivalent of course :-) But with slice categories you see the actual vectors!)

John Baez (May 11 2020 at 22:22):

Yeah, the first time I understood Beck-Chevalley was when I was helping Jeffrey Morton with his thesis (on groupoidification and TQFTs), and we were using spans of groupoids

X \rightarrow A \to Y

to transport Vect-valued presheaves on

X

to Vect-valued presheaves on

Y

, by pulling back and then pushing forward.

John Baez (May 11 2020 at 22:24):

For this procedure to be functorial - for it to send the composite of spans of groupoids into the composite of maps - we needed Beck-Chevalley.

John Baez (May 11 2020 at 22:24):

Dan Doel (May 12 2020 at 03:40):

I don't know if the type theory interpretation is already known to the people who asked, or too similar to the set theory one, but I think it works like this:

In the original Beck-Chevalley square, two of the pullback functors are going to have left adjoints. Pullback is like substitution to change contexts in type theory, and the left adjoint is usually said to be the Σ type. To make the correspondence better, though, those should be the pullback of projection substitutions like

Γ,x:A ⊢ Γ

which induces weakening

\mathsf{wk} : \mathsf{Tm}(Γ) → \mathsf{Tm}(Γ,x:A)

. The other axis is just an arbitrary substitution

Δ ⊢ σ : Γ

which gives a transformation

\mathsf{Tm}(Γ) → \mathsf{Tm}(Δ)

The commutative square of pullbacks is induced by the choice of whether to do the arbitrary substitution first or weaken first. So, the other functors involved are

\mathsf{Tm}(Δ) → \mathsf{Tm}(Δ,x:A[σ])

for weakening after substitution, and

\mathsf{Tm}(Γ,x:A) → \mathsf{Tm}(Δ,x:A[σ])

for substitution after weakening. The two weakening functors have left adjoints

Σ_A : \mathsf{Tm}(Γ,x:A) → \mathsf{Tm}(Γ)

and

Σ_{A[σ]} : \mathsf{Tm}(Δ,x:A[σ]) → \mathsf{Tm}(Δ)

The Beck-Chevalley page says that the adjoints induce a 'mate'

h_!k^* → g^*f_!

. This says that if we show a term by first substituting and then quantifying, it induces a term where we first quantify and then substitute. So there is a rule like:

That's good, because it tells us how to get terms of the substituted type on the bottom. However, it's bad because the rule only goes one way, and we want to define the substituted type to actually be the same thing as the type built in the substituted context. So, Beck-Chevalley says that this is actually an isomorphism, and we are justified in treating the types as the same. If it didn't hold (for some category we want to reason about with type theory), then we would need a type theory where a value of type

(Σ_{x:A} B)[σ]

may not be usable as if it had type

Σ_{x:A[σ]} B[σ,x]

. It's not clear to me what you could even do with the former type in that scenario, though. It is not merely an 'explicit substitution' theory, but one in which those substitutions fail to commute through type formers, so I suppose you would need operations that deal directly with substituted types.

There is a similar condition for Π types, but I think for the opposite direction.

Cody Roux (May 17 2020 at 16:54):

Henry Story (May 17 2020 at 17:04):

I did not advance much this week sadly. Though I got a better understanding of the first 50 pages of "Generic figures and their glueings" (and also skimmed forward -- after p100 I start getting lost)

Thomas Read (May 17 2020 at 17:34):

I'll be around for a little bit if people are keen (though haven't had much time to look at the book, since I'm revising for exams at the moment)

Henry Story (May 17 2020 at 18:01):

Thomas Read (May 17 2020 at 18:02):

Henry Story (May 17 2020 at 20:51):

We had an interesting discussion on a variety of topics in this call.
One thing I was wondering about regarding presheafs (as explained for example in Generic Figures and their Glueings comes from noticing how similar presheafs are to @David Spivak functorial semantics of databases. These are seen as functors from a small category

C

of schemas to

Set

ie the functor

C \to Set

. A presheaf is the functor

C^{op} \to Set

. Why does this

op

appear. (I think I got an answer somewhere to this recently - ah yes here, but that does not explain the relation to Functorial DBs). Perhaps @Ryan Wisnesky will know. We were guessing this was related to something from topology. But coming from computing the simple functorial view seems easy to understand. So it would be nice to understand what is gained by the

^{op}

Dan Doel (May 18 2020 at 00:05):

The intention of each is different. Saying that a database is a functor

C → \mathsf{Set}

is like treating

C

as an algebraic theory, and looking at models in

\mathsf{Set}

. Maps in the functor category are homomorphisms of models. This is like Lawvere theories and such.

But generally, one is not interested in single presheaves as some kind of

C

-like thing. I think generally one is interested in the presheaf category as a richer setting for models to lie in. So a presheaf

C^{op} → \mathsf{Set}

is like a richer sort of set whose values vary according to

C

. Then you want to look at models in the presheaf category, say.

One notable 'model' is the Yoneda embedding

C → [C^{op},\mathsf{Set}]

. This is like a model of

C

\mathsf{Psh}(C)

that is equivalent to the original

C

. But

\mathsf{Psh}(C)

has much more structure, so it can be useful to work with this model to deduce facts about

C

(this is how 'representability' arguments work).

Also, this shows up in type theory quite readily. If

T

is your syntactic category, then functors

T → \mathsf{Set}

are like models of your type theory where types are interpreted as sets, and terms as functions between them. If you want to create a syntactic sort of model, the obvious one of this sort is where each type is interpreted as the set of closed terms of that type. A term

Γ ⊢ e : A

is interpreted as a function on sets that takes closed terms for

Γ

and produces a closed term of type

A

However, there are all sorts of examples where only considering closed terms is not good enough, even if you want to prove a theorem about closed terms. So, you start to consider open terms, but that is exactly what presheaves and the Yoneda embedding get you. Presheaves

[T^{op},\mathsf{Set}]

are like sets that vary coherently depending on a context

Γ

. The Yoneda embedding

T → [T^{op},\mathsf{Set}]

takes each type

A

to the presheaf of open terms

Γ \mapsto Γ ⊢ e : A

There are some more intricate constructions where

T

isn't the same in both cases, but that is the general idea of how it arises in type theory.

Dan Doel (May 18 2020 at 00:12):

There are other, simpler examples of this idea arising in type theoretic/programming contexts, too. For instance, the categorical way of modelling de Bruijn indices is as functors

[\mathsf{FinSet},\mathsf{Set}]

. You might say that is covariant, but this is misleading. The way to think about these as related to the above is that they are presheaves on

\mathsf{FinSet}^{op}

. And the reason for this is that

\mathsf{FinSet}^{op}

is the free Cartesian category with one object. So, it is like the category of contexts where there is only one type with no structure.

So, then,

[\mathsf{FinSet},\mathsf{Set}]

becomes a setting to have models of algebras with untyped variables.

Ryan Wisnesky (May 18 2020 at 08:55):

Yes @Henry Story , we very well could have used presheaves instead of copresheaves, but the connections to algebraic theories and their models are most direct without going through an op, as @Dan Doel says. The approaches are equivalent and we do pay for it later: when writing CQL queries, there are places where given a foreign key f : s -> t, the user has to provide a "widget from t to s", rather than s to t, and it's tricky. So maybe one way to describe the choice is that using copresheaves makes schemas easy but queries hard, and presheaves makes schemas tricky but queries easy. The details are in the algebraic databases paper and I'd be happy to elaborate; profunctors and 'frozen databases' would be involved

Robert Seely (May 19 2020 at 22:58):

One aspect of B-C is that it makes the translation from categories "work" - e.g. the correspondance between the categorical structure and its logical counterpart. An example may be found in my thesis (Hyperdoctrines, natural deduction, and the Beck condition. (RAG Seely, Zeitschrift f. math. Logik und Grundlagen d. Math. 29 (1983) 505-542.)) which deals with this in the Lawvere-ian context of first order logic with equality, but many similar examples abound.

Henry Story (May 20 2020 at 18:55):

Reading Generic Figures and their Glueings I came across the description of a Category

Fig(X)

of the

\Bbb{C}-Set X

(a pre-sheaf), which seems to me to be very much like a Grothendieck construction that I found in Spivack's functorial semantics. What are types in one category, thurn out to be objects in the Figure category.
Ie. one can't as they just write there I think really have a morphism f between two objects as there would be many morphisms f with the same name. The morphism would actually need to be a triple.
Screen-Shot-2020-05-20-at-20.52.40.png

Henry Story (May 20 2020 at 22:13):

The good news is: after reading the first 50 pages of "Generic Figures and their Glueings" I think I now understand example (viii) p25 of "Sheaves in Geometry and Logic" on

Set^{C^{op}}

. :sweat:

Henry Story (May 21 2020 at 14:27):

I wonder what you mean by the Free Cartesian Category with one object.
I was under the impression that

Set^{op}

was the category of Finite Boolean Algebras, reached by taking every object of Set and mapping it to its powerset, and ordering that powerset by set inclusion, constituting thus a boolean algebra. The morphisms between those boolean algebras go of course in the opposite direction to the functions in Set to which they correspond.
A few weeks ago I drew out some diagrams on

Set^{op}

which I guess would look the same in

FinSet^{op}

to get clear about what a (co-)product would look like there. I did not finish the diagram as the powersets explode, as their name suggests. At the time I was trying to get an understand of how

Set^{op}

was a complement tops so I also drew out a picture of a Pushout diagram for conjunction in the complement topos of Boolean algebras.

Dan Doel (May 21 2020 at 14:32):

Well, for one,

\mathsf{Set}^{op}

is not "the category of Boolean algebras". It is the category of complete, atomic boolean algebras, which are particular kinds of boolean algebras. But that's kind of beside the point.

Henry Story (May 21 2020 at 14:32):

yes, I was trying to remember that off the top of my head. I missed a few words :-)

Henry Story (May 21 2020 at 14:38):

But I guess that individual objects in

FinSet^{op}

all are CABAs made out of one type which is the Top object of the CABA. So in a sense each individual CABA has only one type.

Dan Doel (May 21 2020 at 14:40):

So, the free Cartesian category generated by an object has objects like

T^n

, where

T

is the generating object. And maps

T^n → T^m

decompose into

m

maps

T^n → T

specifying where each part of the result comes from. However, the only maps of this restricted form are projections out of the

n

-ary Cartesian product. So, each of the

m

maps is just a selection from

n

possible values. And so

T^n → T^m

is like a function

m → n

where

m

and

n

are finite sets.

Dan Doel (May 21 2020 at 14:41):

The actual (opposite) category of finite sets has redundant objects, because you only need one finite set of each size, but that doesn't matter with respect to equivalence of categories.

Dan Doel (May 21 2020 at 14:45):

Dan Doel (May 21 2020 at 14:51):

And this is the same structure you get for contexts from having just the variable rules in a 'type theory' with a single type. Contexts

Γ

are just lists of variables with that type, and if you have contexts

Γ

and

Σ

, a substitution for

Σ

using variables in

Γ

is just a

Σ

-sized list of the variables from

Γ

, which is equivalent to saying which position in

Γ

each position of

Σ

maps to.

Henry Story (May 21 2020 at 14:57):

Henry Story (May 21 2020 at 15:09):

There is this 2016 PhD thesis that explains Dependent Object Types, it's relation to

F_{<:}

and more.... I think if I could find a good way to tie the maths to that, I'd learn much faster.

Dan Doel (May 21 2020 at 15:18):

I think the way people are starting to study type theory categorically, subtyping does not exist at the most fundamental level. Every term has a single particular type. Subtyping is a convenience that elaborates a 'surface syntax' into the more fundamental theory by inserting mediating maps between subtype and supertype.

Henry Story (May 21 2020 at 15:24):

yes, but I guess there is some CT gadget that brings that concept under one term, so that it can be studied.
The other things is that DOT comes with dependent types. So it has both Dependent Types and a type hierarchy.
I wonder if one can read off their one page description what category that corresponds to.

Henry Story (May 21 2020 at 15:35):

Dan Doel (May 21 2020 at 17:05):

Well, I don't recall if I've read it, but from the abstract, it is probably more in the vein of what I said than the traditional subtyping-as-fundamental approach. It is an algebraic/structural presentation of concepts that are often treated with a "material" approach.

I.E. there is no notion of types that 'are actually' subtypes of the cofree coalgebra in that they are subcollections of its values, vs. merely having a monomorphism into the cofree coalgebra. Algebraicly this distinction makes no sense, but traditional notions of subtyping have it. Same with traditional set theory. Some sets 'actually are' subsets of a given set, while others are merely isomorphic to, but not actually, subsets. But from an algebraic perspective this doesn't matter.

I suppose a way to look at this is that the algebraic view is looking at the essential structure involved. "What structural relationship do subclasses have with respect to superclasses." But type theories that involve subtyping directly have inessential details involved, like how particular things are implemented, or whether one can algorithmically recognize particular cases of the structure (because that is probably an undecidable problem in general).

Christian Williams (May 30 2020 at 17:18):

Christian Williams (May 30 2020 at 19:04):

I suppose it's good to just talk here anyway, for everyone to share.
Tomorrow I'll be working through some examples, and we can talk about internal logic or anything else.

Christian Williams (May 30 2020 at 19:05):

Those who have been coding up some of the proofs -- are they publicly available? It might be helpful to see them.

Cody Roux (May 30 2020 at 19:34):

I'm game! I haven't been coding up any proofs, sadly. Though I once did define the CCC structure on presheaves... maybe I should dig that up.

Cody Roux (May 31 2020 at 16:02):

Christian Williams (May 31 2020 at 16:13):

Today I want to just talk on the server, at the usual time (about two hours from now). But if you get more people, feel free to meet.

Christian Williams (May 31 2020 at 18:04):

So I'm looking at VI.5 and VI.6, The Mitchell-Benabou Language and Kripke-Joyal Semantics. I'm hoping to get a feel for how expressions in the language can be translated into constructions in any topos.

Christian Williams (May 31 2020 at 18:07):

An example formula is that of the "object of epimorphisms"

\mathrm{Epi}(X,Y) = \{f\in Y^X\; |\; \forall y\in Y\; \exists x\in X\; f(x)=y\}

Christian Williams (May 31 2020 at 18:12):

This a subobject of

Y^X

, of course, and we can show that its "elements" satisfy the universal property of epimorphism; and moreover they claim that this allows for important logical statements to be internalized to a topos, such as the axiom of choice (this can be expressed as "exponentiation preserves epis").

Cody Roux (May 31 2020 at 18:14):

Christian Williams (May 31 2020 at 18:15):

Good question. I've always thought of the axiom of choice as "every epi has a section".

Cody Roux (May 31 2020 at 18:15):

Sure, and I even understand how one might prove that from a couple other formulations

Cody Roux (May 31 2020 at 18:16):

Christian Williams (May 31 2020 at 18:17):

So, why should this one be equivalent... What does it mean to say exponentiation preserves epis? They write out the long formula below the claim, but it can be written more simply with

\mathrm{Epi}(X,Y)

Cody Roux (May 31 2020 at 18:19):

Christian Williams (May 31 2020 at 18:20):

Cody Roux (May 31 2020 at 18:21):

Christian Williams (May 31 2020 at 18:22):

If you have a function into the set of surjections

f:E\to \mathrm{Epi}(X,Y)

, does that give you a surjection

E\times X\to Y

Dan Doel (May 31 2020 at 18:23):

Cody Roux (May 31 2020 at 18:24):

In my mind, the "real" axiom of choice, is

\forall x\exists y\ \phi(x,y)\ \Rightarrow\ \exists f\forall x\ \phi(x,f(x))

Christian Williams (May 31 2020 at 18:24):

Cody Roux (May 31 2020 at 18:24):

Cody Roux (May 31 2020 at 18:26):

Christian Williams (May 31 2020 at 18:26):

John Baez (May 31 2020 at 18:29):

Christian Williams (May 31 2020 at 18:29):

Yes, defined

\bar{f}(e,x) = f(e)(x)

; this will be a surjection because each

f(e)

is. But it seems like you can't go back the other way -- if you have a surjection

g:E\times X\to Y

and you curry it, that doesn't mean that every

\bar{g}(e)

will be a surjection.

Christian Williams (May 31 2020 at 18:29):

John Baez (May 31 2020 at 18:29):

Cody Roux (May 31 2020 at 18:31):

Not sure what I mean, but basically you have an epi

X \twoheadrightarrow

you want to build an epi

X^E \twoheadrightarrow Y^E

, so take a function

g\in Y^E

we need to somehow find a function

f\in X^E

. I'm wondering if that existential will do it.

Christian Williams (May 31 2020 at 18:32):

Ah okay, yes that makes more sense. You're saying

\mathrm{Epi}(X,Y)^E \simeq \mathrm{Epi}(X^E,Y^E)

Reid Barton (May 31 2020 at 18:35):

I'm pretty sure "exponentiation preserves epis" (at least in Set) means "if

X \to Y

is epi then

X^E \to Y^E

is epi", particularly as this is indeed equivalent to the axiom of choice.

Dan Doel (May 31 2020 at 18:36):

@Cody Roux Consider truncation

|-| : X → \Vert X \Vert

. That's an epi. Then preservation says that forall

g : A → \Vert X \Vert

there is an

h : A → X

that

g

factors through.

Dan Doel (May 31 2020 at 18:36):

Cody Roux (May 31 2020 at 18:36):

@Reid Barton I'm just asking for an argument of this. I do see the implication "epis are split"

\Rightarrow

"exponentiation preserves epis", but the other direction is not forthcoming.

Reid Barton (May 31 2020 at 18:37):

Christian Williams (May 31 2020 at 18:38):

So in

\mathrm{Set}

, given

f:E\to \mathrm{Epi}(X,Y)

we can construct

\bar{f}:\mathrm{Epi}(X^E,Y^E)

by defining

\bar{f}(g)(e) = f(e)(g(e))

. That's surely the isomorphism.

Cody Roux (May 31 2020 at 18:38):

Oooh. That's why I'm not a category theorist. I always forget to apply to the identity.

Cody Roux (May 31 2020 at 18:39):

Ok now that's out of the way: what does

\{f \in X^Y \mid \forall y\exists x\ f(x) = y\}

in the M-B language mean externally?

Cody Roux (May 31 2020 at 18:40):

I think we should re-translate this into a question of the form: "what does

U\Vdash \forall y\exists x\ f(x) = y

mean externally?"

Christian Williams (May 31 2020 at 18:42):

Yeah, so the part in the text that seems to be doing all the good work is Theorem 1 from Kripke-Joyal Semantics, its proof. Have you used this syntax before? It's all pretty new to me.

Cody Roux (May 31 2020 at 18:42):

Sure! It's standard from realizability theory, one of the few things I understand a little bit. Also in Kripke semantics.

Cody Roux (May 31 2020 at 18:43):

Basically intuitively it means either "True with evidence

U

" or "True in the world

U

" depending on which framework you're in.

Christian Williams (May 31 2020 at 18:44):

When I read about it, I remember @David Spivak saying in a talk that he didn't think the internal language was that exciting until he learned about Kripke-Joyal semantics. I can see that it's really convenient and expressive, basically packaging up the reasoning you'd want to do with MB.

Cody Roux (May 31 2020 at 18:44):

The second interpretation is probably a bit more relevant here, though the realizability view is still close at hand.

Christian Williams (May 31 2020 at 18:44):

Cody Roux (May 31 2020 at 18:46):

So then

\phi

being true in the M-B semantics means

1\Vdash\phi

if I'm not incorrect.

Cody Roux (May 31 2020 at 18:46):

Christian Williams (May 31 2020 at 18:47):

Yeah, that's right. So, we're trying to interpret

U\Vdash \forall y\exists x\ f(x) = y

Cody Roux (May 31 2020 at 18:48):

Ok, there's a subtle point here, since the interpretation of

\exists

involves some epi.

Christian Williams (May 31 2020 at 18:50):

Yeah, so unpacking it using Theorem 1, we can see that each part of the formula contains a lot of information.

Cody Roux (May 31 2020 at 18:50):

So.

U\Vdash \forall y\exists x\ f(x) = y

iff for all

p: V\rightarrow U

and

\beta:V\rightarrow Y

V\Vdash \exists x\ f(x) = \beta

, again if I'm not mistaken.

Cody Roux (May 31 2020 at 18:52):

Christian Williams (May 31 2020 at 18:52):

Yep, looks right. But... looking at this unpacking now, I'm thinking that this doesn't really give the categorical construction; it just tells you the niceness of the interpretation of this "forcing". What do you think?

Cody Roux (May 31 2020 at 18:53):

I mean. Eventually it's going to give you a categorical notion of being a surjection...

Cody Roux (May 31 2020 at 18:53):

Cody Roux (May 31 2020 at 18:54):

Christian Williams (May 31 2020 at 18:55):

Cody Roux (May 31 2020 at 18:55):

Christian Williams (May 31 2020 at 18:56):

Ah, I see that if we're thinking about "global" properties like "being an epimorphism", then

U=1

, so a lot of these unpackings will simplify.

Cody Roux (May 31 2020 at 18:56):

Ok. Next step, we get rid of the

\exists

. This requires a given epi

q:W\twoheadrightarrow V

and a generalized object

\gamma: W\rightarrow X

such that

W\Vdash fpq(\gamma)=\beta q

Cody Roux (May 31 2020 at 18:59):

Cody Roux (May 31 2020 at 19:01):

So, simplifying due to

U=1

, we should be able to assume that

V=1

(I think?)

Cody Roux (May 31 2020 at 19:01):

Cody Roux (May 31 2020 at 19:03):

Ok wait for a minute. I'm not actually sure we can set

V=1

. Let's do the full version first.

Christian Williams (May 31 2020 at 19:03):

Christian Williams (May 31 2020 at 19:04):

Part

(vi')

of the theorem gives an easier version of unpacking

\forall

that they use.

Christian Williams (May 31 2020 at 19:06):

They aren't letting

U=1

because they want to consider the general case of

U\times X\to Y

being epi; but it seems like you could just do a without-loss-of-generality argument.

Cody Roux (May 31 2020 at 19:07):

To summarize:

f : X\rightarrow Y

is an internal epi if for every

\beta : V\rightarrow Y

, there is some epi

q : W\twoheadrightarrow V

and a

\gamma : W\rightarrow X

such that

f\gamma = \beta q

. Did I get that right?

Christian Williams (May 31 2020 at 19:09):

Christian Williams (May 31 2020 at 19:10):

Cody Roux (May 31 2020 at 19:10):

That doesn't seem so bad. It's also not quite enough to get you a section, obviously.

Cody Roux (May 31 2020 at 19:11):

Christian Williams (May 31 2020 at 19:13):

Cody Roux (May 31 2020 at 19:13):

Cody Roux (May 31 2020 at 19:14):

Christian Williams (May 31 2020 at 19:15):

Cody Roux (May 31 2020 at 19:17):

let some

j,k:Y \rightarrow Z

be such that

j\neq k

we need to find some

W

and

\gamma_1,\gamma_2:W\rightarrow X

that "witness" this distinction.

Christian Williams (May 31 2020 at 19:19):

Cody Roux (May 31 2020 at 19:20):

Cody Roux (May 31 2020 at 19:21):

Christian Williams (May 31 2020 at 19:22):

Cody Roux (May 31 2020 at 19:23):

Cody Roux (May 31 2020 at 19:24):

Christian Williams (May 31 2020 at 19:24):

By the way if anyone has been trying to follow along, you should probably just read VI.6; this example is explained well.

Christian Williams (May 31 2020 at 19:25):

Cody Roux (May 31 2020 at 19:27):

Cody Roux (May 31 2020 at 19:29):

Anyways, my only point was that now you know that there exists a

W\twoheadrightarrow \{y\mid jy\neq k y\}\rightarrowtail Y

and two morphisms

\gamma_1, \gamma_2

that make the whole shebang commute.

Christian Williams (May 31 2020 at 19:29):

Cody Roux (May 31 2020 at 19:29):

Cody Roux (May 31 2020 at 19:30):

Cody Roux (May 31 2020 at 19:33):

But I think the whole exciting thing for me is that I already know how to reason internally in this logic. And there's interactive tools to help you do it. No such luck in category theory.

Cody Roux (May 31 2020 at 19:34):

It's also easy for me to have intuition of the form: "I can never prove this, because I'd have to pull an

x:X

out of thin air..." which somehow makes it easy to see if something isn't true in general in sheaves.

Cody Roux (May 31 2020 at 19:34):

Cody Roux (May 31 2020 at 19:37):

The big difficulty for me is to understand where these epimorphisms come from in the definitions of

U\Vdash \phi\vee\psi

and

U\Vdash\exists x\ \phi(x)

. They are crucial, since they contain a lot of the intuitionistic content, but their appearance refers to some technical lemmas from chapter IV, which I have little intuition about...

Christian Williams (May 31 2020 at 19:39):

Cody Roux (May 31 2020 at 19:41):

Cody Roux (May 31 2020 at 19:42):

If it were a tiny bit more extensional, it would basically be the internal language of Toposes (with universes and NNOs)

Christian Williams (May 31 2020 at 19:42):

Yeah, I think those are ultimately about epi-mono factorization (necessary to take joins of subobjects, and for tons of other things), and the fact that pullbacks preserve coproducts (extensive).

Christian Williams (May 31 2020 at 19:45):

How much do you really mean this to be true? It should be the internal language of a specific topos, right?

Cody Roux (May 31 2020 at 19:47):

There's some finicky technical details, so I won't stick my head out, but if you add functional extensionality, make equality extensional, and remove the universes, I wouldn't be surprised if the free theory of toposes with NNOs isn't bi-interpretable into Coq.

Ralph Sarkis (Sep 13 2021 at 08:26):

If you ended up not completely following this group and are still interested in reading the book, we are starting another reading group here.

Stream: theory: category theory

Topic: Reading group on "Sheaves in Geometry and Logic"

Reed Mullanix (Mar 23 2020 at 21:05):

Christian Williams (Mar 23 2020 at 21:08):

Stelios Tsampas (Mar 23 2020 at 21:09):

Philip Zucker (Mar 23 2020 at 21:11):

Reed Mullanix (Mar 23 2020 at 21:11):

Stelios Tsampas (Mar 23 2020 at 21:12):

Christian Williams (Mar 23 2020 at 21:13):

Stelios Tsampas (Mar 23 2020 at 21:13):

Christian Williams (Mar 23 2020 at 21:13):

John Baez (Mar 23 2020 at 21:14):

Christian Williams (Mar 23 2020 at 21:16):

John Baez (Mar 23 2020 at 21:16):

Reed Mullanix (Mar 23 2020 at 21:19):

Christian Williams (Mar 23 2020 at 21:21):

Christian Williams (Mar 23 2020 at 21:22):

sarahzrf (Mar 23 2020 at 21:22):

sarahzrf (Mar 23 2020 at 21:22):

sarahzrf (Mar 23 2020 at 21:23):

sarahzrf (Mar 23 2020 at 21:23):

sarahzrf (Mar 23 2020 at 21:24):

John Baez (Mar 23 2020 at 21:24):

John Baez (Mar 23 2020 at 21:25):

sarahzrf (Mar 23 2020 at 21:27):

Reed Mullanix (Mar 23 2020 at 21:27):

sarahzrf (Mar 23 2020 at 21:27):

sarahzrf (Mar 23 2020 at 21:27):

Reed Mullanix (Mar 23 2020 at 21:28):

Christian Williams (Mar 23 2020 at 21:28):

sarahzrf (Mar 23 2020 at 21:29):

sarahzrf (Mar 23 2020 at 21:29):

sarahzrf (Mar 23 2020 at 21:30):

sarahzrf (Mar 23 2020 at 21:30):

Matt Cuffaro (he/him) (Mar 23 2020 at 21:30):

sarahzrf (Mar 23 2020 at 21:30):

Christian Williams (Mar 23 2020 at 21:32):

John Baez (Mar 23 2020 at 21:32):

sarahzrf (Mar 23 2020 at 21:34):

John Baez (Mar 23 2020 at 21:34):

Emily Pillmore (Mar 23 2020 at 21:41):

Reed Mullanix (Mar 23 2020 at 21:45):

Emily Pillmore (Mar 23 2020 at 21:45):

Emily Pillmore (Mar 23 2020 at 21:46):

Thomas Read (Mar 23 2020 at 21:46):

Reed Mullanix (Mar 23 2020 at 21:50):

Bhavik Mehta (Mar 23 2020 at 21:50):

Reed Mullanix (Mar 23 2020 at 21:51):

sarahzrf (Mar 23 2020 at 21:51):

sarahzrf (Mar 23 2020 at 21:51):

Stelios Tsampas (Mar 23 2020 at 21:51):

Stelios Tsampas (Mar 23 2020 at 21:52):

Bhavik Mehta (Mar 23 2020 at 21:52):

Stelios Tsampas (Mar 23 2020 at 21:52):

Reed Mullanix (Mar 23 2020 at 21:52):

Balaram Usov (Mar 23 2020 at 21:55):

John Baez (Mar 23 2020 at 21:56):

John Baez (Mar 23 2020 at 21:57):

Reed Mullanix (Mar 23 2020 at 21:59):

Emily Pillmore (Mar 23 2020 at 22:05):

Cody Roux (Mar 23 2020 at 22:41):

Emily Pillmore (Mar 23 2020 at 22:42):

Emily Pillmore (Mar 23 2020 at 22:42):

Emily Pillmore (Mar 23 2020 at 22:43):

Joe Moeller (Mar 23 2020 at 22:44):

Joe Moeller (Mar 23 2020 at 22:44):

Emily Pillmore (Mar 23 2020 at 22:44):

Emily Pillmore (Mar 23 2020 at 22:44):

Matteo Capucci (he/him) (Mar 24 2020 at 13:06):

John Baez (Mar 24 2020 at 16:49):

John Baez (Mar 24 2020 at 16:49):

John Baez (Mar 24 2020 at 16:51):

Mike Stay (Mar 24 2020 at 17:21):

Cody Roux (Mar 24 2020 at 17:27):

Reed Mullanix (Mar 24 2020 at 17:38):

John Baez (Mar 24 2020 at 17:59):

Cody Roux (Mar 24 2020 at 17:59):

Stelios Tsampas (Mar 24 2020 at 19:36):

John Baez (Mar 24 2020 at 19:37):

Stelios Tsampas (Mar 24 2020 at 19:38):