Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: category theory

Topic: Logic & Programming Languages

sarahzrf (Mar 27 2020 at 05:05):

oh my god i just spent ages typing up a message to ask about some kind of bizarre universal property i had noticed and couldn't quite phrase right and i figured it out while typing and it's just "this universal property of everything in set A also applies to everything in this subset of A" :face_palm:

sarahzrf (Mar 27 2020 at 05:06):

well, i'll post what i typed anyway because it's a fun little set of adjunctions and stuff

sarahzrf (Mar 27 2020 at 05:06):

Fix a heyting algebra $H$:

1. $\neg \vdash \neg$ is a contravariant self-adjunction whose monad is the closure operator $\neg\neg$. Let $Reg(H)$ be the set of algebras/fixed-points of this operator, the "regular elements"—explicitly, those with $\neg\neg P \le P$. Then by standard properties of Galois connections (or of idempotent monads if u wanna b fancy), $Reg(H)$ is exactly the image of $\neg\neg$, and $\neg\neg$ is in fact left adjoint to the inclusion $Reg(H) \hookrightarrow H$.

2. Let $Dec(H)$ be the set of decidable elements—i.e., those satisfying $P \lor \neg P = \top$. We have $Dec(H) \subseteq Reg(H)$, but this can be strict (having all instances of double negation elimination ($Reg(H) = H$) implies that we have all instances of excluded middle ($Dec(H) = H$), but individual instances need not give individual decisions). I don't think the inclusion of this into either $Reg(H)$ or $H$ as a whole has adjoints on either the left or the right in general.

3. There is nonetheless some kind of adjoint-y relationship between $Dec(H)$ and $Reg(H)$, because for $P \in H, Q \in Dec(H)$, we have...

sarahzrf (Mar 27 2020 at 05:07):

(and then i realized that the property was literally just "$Dec(H) \subseteq Reg(H)$, so the universal property of $\neg\neg$ applies to things in $Dec(H)$ too")

John Baez (Mar 27 2020 at 05:36):

Nice! Open sets in a topological space form a Heyting algebra. Is there some nice topological way to think about the "decidable" and "regular" ones, and a nice topological example of a regular one that's not decidable?

Christian Williams (Mar 27 2020 at 05:39):

sarahzrf said:

$Reg(H)$ is exactly the image of $\neg\neg$, and $\neg\neg$ is in fact left adjoint to the inclusion $Reg(H) \hookrightarrow H$.

Hm, I need to think about this. I thought for a Galois connection we had $\neg \neg \neg P = \neg P$; i.e. any element of the form $\neg P$ is "regular". but you're saying the regular elements are ones that look like $\neg \neg P$. I'm probably remembering something wrong.

sarahzrf (Mar 27 2020 at 06:00):

both are true!

sarahzrf (Mar 27 2020 at 06:01):

anything of the form $\neg P$ is also $\neg\neg\neg P$, so in particular it's the double negation of itself, and anything of the form $\neg\neg P$ is the negation of $\neg P$, so something is a double negation iff it is a single negation

sarahzrf (Mar 27 2020 at 06:05):

John Baez said:

Nice! Open sets in a topological space form a Heyting algebra. Is there some nice topological way to think about the "decidable" and "regular" ones, and a nice topological example of a regular one that's not decidable?

negation in the algebra of opens is exterior iirc (i.e., complement minus boundary)
so the decidable opens are the ones such that $U \cup Ext(U) = X$—a little fiddling shows that this is true iff $U$ has no boundary, i.e. is clopen

the regular ones i think are a little subtler
an open can fail to be regular if adding part of its boundary gives something that is still open, i think
in $\mathbb R$, notorious examples of irregulars are sets missing a few isolated points, but intervals, for example, are regular i think

sarahzrf (Mar 27 2020 at 06:07):

honestly though you don't need to turn to topology or work externally to see regular propositions that aren't decidable
any negation is regular, but only a select few negations are decidable!

sarahzrf (Mar 27 2020 at 06:10):

btw, a fun fact: $Reg$ extends to a functor from the category of heyting algebras to the category of boolean algebras—$Reg(H)$ is always a boolean algebra (but its disjunction is not the same as $H$'s)!—and this functor is in fact the left adjoint to the inclusion from boolean algebras to heyting algebras 🤯
the unit $H \twoheadrightarrow Reg(H)$ is exactly double negation
so it's, like, an adjunction inside an adjunction

sarahzrf (Mar 27 2020 at 06:10):

this is the semantic end of the double negation translation i guess

sarahzrf (Mar 27 2020 at 06:10):

i've meant for a while now to work thru it in a lot more detail but ive never gotten around to it...

sarahzrf (Mar 27 2020 at 06:29):

hmm, for some reason i thought the unit of a reflective subcategory was called the "reflector", is that not the term :thinking:

nadia esquivel márquez (Mar 27 2020 at 06:38):

sarahzrf said:

i really fuckin need to read the coend book one of these days :sob:

God me too . . . i think this might be a good candidate for a reading group topic if more people are interested

John Baez (Mar 27 2020 at 06:38):

sarahzrf said:

btw, a fun fact: $Reg$ extends to a functor from the category of heyting algebras to the category of boolean algebras—$Reg(H)$ is always a boolean algebra (but its disjunction is not the same as $H$'s)!—and this functor is in fact the left adjoint to the inclusion from boolean algebras to heyting algebras 🤯
the reflector $H \hookrightarrow Reg(H)$ is exactly double negation
so it's, like, an adjunction inside an adjunction

Great! This sounds like the nice modern way to talk about what people traditionally call the double-negation translation relating classical and intuitionistic logic. I like this modern version!

Here's a puzzle I've never figured out, which you seem like the perfect person to solve:

The opposite of a Heyting algebra is called a co-Heyting algebra: a poset $P$ with finite limits and colimits where for each $p \in P$, the map $p \vee - \colon P \to P$ has a left adjoint. Just as Heyting algebras formalize the intuitionistic propositional calculus where we drop the law of excluded middle, co-Heyting algebras formalize the paraconsistent propositional calculus where we drop the principle of noncontradiction. A poset that's both a Heyting algebra and co-Heyting algebra is called a bi-Heyting algebra.

Puzzle. What's an example of a bi-Heyting algebra that's not a Boolean algebra?

I've heard that examples exist, but I've never seen one that I could understand.

sarahzrf (Mar 27 2020 at 06:41):

double-negation translation is a syntactic thing! what i'm describing is semantic!

sarahzrf (Mar 27 2020 at 06:42):

it's possible that you can recover it by applying this to some free algebra or something, but it's not quite the same thing a priori

sarahzrf (Mar 27 2020 at 06:43):

(also, i already said so :mischievous:)
sarahzrf said:

this is the semantic end of the double negation translation i guess

sarahzrf (Mar 27 2020 at 06:44):

hmm, interesting that examples apparently exist

sarahzrf (Mar 27 2020 at 06:45):

i think ive heard that if a category is an elementary topos and so is its opposite, then it has to be trivial, and this seems like a truncation of that

EDIT: aha, it was

Any category which is both cartesian closed and co-cartesian co-closed is a preorder

so that should imply what i said, but certainly isn't a dealbreaker when working with preorders

sarahzrf (Mar 27 2020 at 06:45):

maybe the triviality is just because of size issues that dont come into play here, like how the adjoint functor theorem works for posets :thinking:

John Baez (Mar 27 2020 at 06:45):

Okay, so "semantic end of the double negation translation" is a more precise way to say what I said, namely "modern version". It's a bit like how Lawvere theories take universal algebra and strip off some of the distracting syntactic fussiness.

sarahzrf (Mar 27 2020 at 06:46):

if "modern" means "semantic, neglecting the syntactic end", then i want no part of modernity :triumph:

John Baez (Mar 27 2020 at 06:46):

I want it.

sarahzrf (Mar 27 2020 at 06:47):

well, my specialty is programming languages, so perhaps i'm biased :)

John Baez (Mar 27 2020 at 06:49):

Yes, if you talk to computers a lot you've gotta care about syntax. I mainly talk to people precisely for this reason.

John Baez (Mar 27 2020 at 06:49):

(I'm sort of kidding; I used to study formal logic...)

sarahzrf (Mar 27 2020 at 06:52):

trying to make sense of a left adjoint to - ∨ R

sarahzrf (Mar 27 2020 at 06:52):

hmm

John Baez (Mar 27 2020 at 06:54):

Yes, it's really freaky at first! I eventually got used to it, and now I've sort of forgotten it.

sarahzrf (Mar 27 2020 at 06:55):

(also: syntax is an incredibly powerful tool for manufacturing adjunctions, but i'll let that argument go :upside_down:)

John Baez (Mar 27 2020 at 06:59):

All I mean is that I'm usually more interested in groups than group presentations, more interested in Lawvere theories than universal algebra as described by a chosen set of function symbols obeying a chosen set of axioms, more interested in posets than ways of writing these posets as sets of equivalence classes of symbols strings, and so on - the thing presented has more symmetry than the presentation.

sarahzrf (Mar 27 2020 at 07:00):

but how much do you learn about groups from the study of their presentations, and from the fact that group presentations are a thing?

John Baez (Mar 27 2020 at 07:00):

A lot!

John Baez (Mar 27 2020 at 07:00):

But I think of that as a tool for studying something I'm interested in, not the thing I'm interested in.

sarahzrf (Mar 27 2020 at 07:01):

hmm :)

sarahzrf (Mar 27 2020 at 07:01):

when it comes to groups, there's maybe a stronger argument

sarahzrf (Mar 27 2020 at 07:01):

but i think heyting algebras were invented in order to give semantics to intuitionistic logic

sarahzrf (Mar 27 2020 at 07:01):

regardless, though—

sarahzrf (Mar 27 2020 at 07:02):

i prefer to avoid thinking of either as purely a tool for studying the other

sarahzrf (Mar 27 2020 at 07:02):

they push on each other!

John Baez (Mar 27 2020 at 07:02):

Yes, that's very reasonable.

John Baez (Mar 27 2020 at 07:03):

I just find logicians and programmers are too much into syntax for me to ever really be one - just a matter of taste.

sarahzrf (Mar 27 2020 at 07:04):

no accounting for it

John Baez (Mar 27 2020 at 07:04):

Said the accountant to the mathematician...

sarahzrf (Mar 27 2020 at 07:04):

:weary:

John Baez (Mar 27 2020 at 07:05):

Anyway, that nLab page on co-Heyting algebras has a bunch of fun stuff about that left adjoint, which they call "subtraction".

John Baez (Mar 27 2020 at 07:05):

But it's probably more fun to think about it oneself for a while.

sarahzrf (Mar 27 2020 at 07:05):

oh that's fucked up because i decided on a minus sign to write it while messing around

sarahzrf (Mar 27 2020 at 07:05):

on the right track >:)

sarahzrf (Mar 27 2020 at 07:05):

or maybe i just remembered having seen it vaguely

John Baez (Mar 27 2020 at 07:08):

Part of why it'd be so cool to have bi-Heyting algebras that weren't boolean is that you've have this extra logical operation that's weirdly dual to implication and not have it reduce to other things... it seems like a kind of wonderland of adjoints.

sarahzrf (Mar 27 2020 at 07:10):

(P ∨ forall x, Q x) <-> (forall x, P ∨ Q x)
^this is unsettling

sarahzrf (Mar 27 2020 at 07:10):

and rather classical-looking

sarahzrf (Mar 27 2020 at 07:12):

actually it makes me suspicious of whether it's reasonable to expect to be able to find non-boolean co-heyting algebras with very much completeness in a constructive metatheory

sarahzrf (Mar 27 2020 at 07:17):

suppose we knew there was a complete co-heyting algebra $H$—then let $S$ be an arbitrary subsingleton set, and $(\exists x \in S. \top) \lor (\forall x \in S. \bot) = \forall x \in S. (\exists x \in S. \top) \lor \bot = \forall x \in S. \exists x \in S. \top = \top$

sarahzrf (Mar 27 2020 at 07:20):

$\exists S. \top$ is basically the $H$-internal statement "$S$ is inhabited", and $\forall x \in S. \bot$ is basically the $H$-internal statement "$S$ is empty"

sarahzrf (Mar 27 2020 at 07:21):

so if we take this embedding of external truth values into an arbitrary complete lattice, then if that complete lattice is in fact a co-heyting algebra, we must have a strong excluded middle in it for those embedded truth values, which i find incredibly suspect, because in constructive metatheories most complete lattices get their completeness from power sets

sarahzrf (Mar 27 2020 at 07:22):

buuuuuuut i suppose this is a big sidetrack.

sarahzrf (Mar 27 2020 at 07:24):

it's almost 3:30am, i don't have the patience for this, i'm gonna go look on the nlab page :upside_down:

sarahzrf (Mar 27 2020 at 07:26):

Co-Heyting algebras were initially called Brouwerian algebras.

hahahaaha poor brouwer must be rolling over in his grave

sarahzrf (Mar 27 2020 at 07:29):

image.png
:eyes::eyes::eyes::eyes:

sarahzrf (Mar 27 2020 at 07:30):

i should, like, learn some quantum mechanics

sarahzrf (Mar 27 2020 at 07:31):

beyond the point of "solve this time-independent schrödinger equation we gave you in order to figure out some energy eigenstates for a particle in a box"

sarahzrf (Mar 27 2020 at 07:32):

actually, this co-heyting algebra stuff & this boundary operator & whatnot are interesting—i guess double co-heyting-negation would be interior instead of closure?

sarahzrf (Mar 27 2020 at 07:35):

i was thinking recently about the fact that a lawvere-tierney topology defines a closure rather than an interior

sarahzrf (Mar 27 2020 at 07:36):

ok this has gotten very far from "universal constructions"

Stelios Tsampas (Mar 27 2020 at 14:52):

John Baez said:

Puzzle. What's an example of a bi-Heyting algebra that's not a Boolean algebra?

I've heard that examples exist, but I've never seen one that I could understand.

OK, according to popular sources, every totally ordered set $(P, \leq, 1, 0)$ is a Heyting algebra where $(a \Rightarrow b) \circeq 1$ for $a \leq b$, $(a \Rightarrow b) \circeq b$ otherwise. Which gave me an idea :smiling_devil:.

We dually set the subtraction $a - b \circeq 0$ for $a \leq b$ and $a$ (!!!) otherwise. This satisfies the adjointness condition $\forall z. a - b \leq z\iff a \leq b \vee z$. I'll do the $\Leftarrow$ case. So we have $a \leq b \vee z$. If $a \leq b$ then $a - b = 0$ and so $0 \leq z$. If $b < a$ then $a - b = a$. Between $a \leq (b \vee z)$ and $b < a$, it has to be that $a \leq z$, thus completing the direction.

Now suppose this totally ordered set of ours has a "dangling" element $d$, such that $0 < d < 1$. That means that our totally ordered set is absolutely not a Boolean algebra! In fact, this dangling element is also "paraconsistent" as $a \wedge (1 - a) = a$. Where do we find such a set with a dangling element? Well, my (borrowed) counterexample to the first puzzle was exactly that!

Stelios Tsampas (Mar 27 2020 at 14:59):

John Baez said:

I've heard that examples exist, but I've never seen one that I could understand.

OK, my example should work (unless I made a mistake), but do we actually understand it? What's the lesson here? For me, the lesson is that I should stop trying to make logical sense (in the "classical" meaning of logic) of these sets because them not being Boolean algebras prohibits one from doing so! Free oneself from such constraints, and these funny elements in the sets make perfect sense :).

sarahzrf (Mar 27 2020 at 14:59):

image.png
yknow, it had vaguely occurred to me that you might be able to get coheyting stuff out of a model of linear logic in the same way that you get heyting stuff—and i think im gonna do that in a minute—but it just occurred to me that ive seen this before!!

sarahzrf (Mar 27 2020 at 15:00):

or, well, something similar to it

Stelios Tsampas (Mar 27 2020 at 15:02):

sarahzrf said:

image.png
yknow, it had vaguely occurred to me that you might be able to get coheyting stuff out of a model of linear logic in the same way that you get heyting stuff—and i think im gonna do that in a minute—but it just occurred to me that ive seen this before!!

I hardly know any linear logic, but I've made a quick read in (https://golem.ph.utexas.edu/category/2018/05/linear_logic_for_constructive.html) and it looks like these are weakened compared to Heyting algebras. So I would guess that you might be able to get a similarly weakened co-Heyting thing :P.

sarahzrf (Mar 27 2020 at 15:05):

the intuitionistic implication in linear logic is $!P \multimap Q = ?P^\perp ⅋ Q$, which here is $\min(1, ?P + Q)$, where ? is dual to !

sarahzrf (Mar 27 2020 at 15:05):

also, that screenshot is from the same paper :)

Stelios Tsampas (Mar 27 2020 at 15:05):

sarahzrf said:

also, that screenshot is from the same paper :)

Hahahah what a delightful coincidence!

sarahzrf (Mar 27 2020 at 15:06):

i really recommend taking a look at it! iirc andrej bauer (i think it was him?) said he thought it was the most important paper in constructivism in the last... well, i dont want to misquote what time period he said, but it was probably some number of years

sarahzrf (Mar 27 2020 at 15:07):

plus it gives an extremely useful viewpoint on linear logic other than the "logic of resources" one, which i think is sorely needed in popularization

Stelios Tsampas (Mar 27 2020 at 15:07):

Will do then, thanks for the recommendation :).

sarahzrf (Mar 27 2020 at 15:07):

er, i cant remember whether it invents that viewpoint, but it certainly presents it

Stelios Tsampas (Mar 27 2020 at 15:08):

sarahzrf said:

plus it gives an extremely useful viewpoint on linear logic other than the "logic of resources" one, which i think is sorely needed in popularization

I have a bunch of colleagues in my uni that are messing around with linear logic exactly because they think they accurately represent programmer's intentions when wanting to pass on "resources" in a secure manner. Hmmm...

sarahzrf (Mar 27 2020 at 15:09):

no, it's good for that! it's just that that's the only one i usually hear people talk about, except maybe in actual brass tacks linear logic papers

sarahzrf (Mar 27 2020 at 15:09):

i'd love to see more of its facets acknowledged in its popular image

Stelios Tsampas (Mar 27 2020 at 15:17):

sarahzrf said:

no, it's good for that! it's just that that's the only one i usually hear people talk about, except maybe in actual brass tacks linear logic papers

I agree! The biggest problem is that they're looking to also implement a processor with linear logic primitives (linear capabilities) as hardware primitives. Which is a very touch task, if you want the performance to be somewhat tolerable. And, alas, without decent performance, it's tough convincing people on the practical side of things through formal arguments alone :/.

Stelios Tsampas (Mar 27 2020 at 15:18):

I should convince them to join the zulip! Most likely they'll go "Oh no, not this again" and roll their eyes. Bah, plebs!

sarahzrf (Mar 27 2020 at 15:22):

i honestly dont know whats reasonable in this day and age, cpus are insane

sarahzrf (Mar 27 2020 at 15:23):

although to be fair, insane cpus are usually designed by companies like intel

sarahzrf (Mar 27 2020 at 15:26):

okay this is WAY off topic from "universal constructions" :|

sarahzrf (Mar 27 2020 at 15:26):

is there a way to fork a topic

Stelios Tsampas (Mar 27 2020 at 15:27):

Fork a topic fast? I don't know. But we can just modify the topics.

Stelios Tsampas (Mar 27 2020 at 15:27):

But it's cool, nobody will notice hihi. :zip_it:

Nathanael Arkor (Mar 27 2020 at 15:29):

@sarahzrf: yes, if you edit a post, you can change the topic name to fork it into a separate topic

Nathanael Arkor (Mar 27 2020 at 15:29):

you can actually edit the topics of anyone's posts, which makes it easier to clean things up

sarahzrf (Mar 27 2020 at 15:29):

oh neat

sarahzrf (Mar 27 2020 at 15:29):

don't mind if i do...

Nathanael Arkor (Mar 27 2020 at 15:30):

(though, it'd be super neat to be able to just select exactly which messages you want to fork)

sarahzrf (Mar 27 2020 at 15:32):

hope no one minds, honestly this is basically what i derailed to

sarahzrf (Mar 27 2020 at 15:32):

as i always do >.>

Stelios Tsampas (Mar 27 2020 at 15:34):

Oh, the off-topicness was going waaaaay back! OK, that's cool :).

Stelios Tsampas (Mar 27 2020 at 15:34):

@sarahzrf What does $Reg$ stand for?

sarahzrf (Mar 27 2020 at 15:35):

"regular"—i did mention that, but it was probably easy to miss

sarahzrf (Mar 27 2020 at 15:36):

btw here's my source for the stuff i saw saying about adjunctions w/ boolean algebras https://ncatlab.org/nlab/show/Heyting+algebra#ToBooleanAlgebras

Stelios Tsampas (Mar 27 2020 at 15:38):

Thanks! :)

vikraman (Mar 27 2020 at 15:48):

Sub(1) in a presheaf topos would be an example of a bi-heyting algebra that's not boolean, wouldn't it?

sarahzrf (Mar 27 2020 at 15:53):

what makes it bi-heyting?

vikraman (Mar 27 2020 at 18:25):

It is bi-heyting for the same reason that powersets are bi-heyting, I think of these as intuitionistic powersets. The nLab page on bi-heyting toposes cites a slick proof.

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

vikraman said:

It is bi-heyting for the same reason that powersets are bi-heyting, I think of these as intuitionistic powersets. The nLab page on bi-heyting toposes cites a slick proof.

It is a very slick proof! So the next question is: what's the co-Heyting operation?

vikraman (Mar 27 2020 at 18:30):

$X \cup A \supseteq B \Leftrightarrow X \supseteq B \setminus A$

vikraman (Mar 27 2020 at 18:31):

I'm unable to type in the LaTeX but I think this is the structure

Nathanael Arkor (Mar 27 2020 at 18:31):

(you need two dollar signs)

Ben Steffan (Mar 27 2020 at 18:31):

(also the last \superseteq is misspelled)

Nathanael Arkor (Mar 27 2020 at 18:32):

it's supseteq, I think: $X \cup A \supseteq B \Leftrightarrow X \supseteq B \setminus A$

Nathanael Arkor (Mar 27 2020 at 18:34):

and \setminus for backslash

Nathanael Arkor (Mar 27 2020 at 18:37):

(the joys of LaTeX!)

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

vikraman said:

$X \cup A \supseteq B \Leftrightarrow X \supseteq B \setminus A$

That's the definition of a co-Heyting operation, but I was trying to ask "what does the co-Heyting operation concretely do in a given presheaf topos?" If I take the simplest non-Boolean example of presheaves on the category $A \to B$, for instance, what is the co-Heyting operation on a subobject lattice Sub(X)?

vikraman (Mar 27 2020 at 18:59):

In terms of sieves or cribles? I don't have a good intuition for those but I will try to think.

sarahzrf (Mar 27 2020 at 19:16):

that's not co-heyting, that's the formula for a right adjoint to $\cup$ i can't fucking read

vikraman (Mar 27 2020 at 19:20):

$\cup$ is a product in the dual and has a right adjoint, making it a co-heyting algebra, isn't that correct?

John Baez (Mar 27 2020 at 19:26):

So, I tweeted about bi-Heyting algebras, as one does, and I learned something that it seems you folks have already learned:

Any totally ordered set with a top and bottom element is a bi-Heyting algebra, and if this set has more than 2 elements it's not a Boolean algebra.

So, a very nice bi-Heyting but non-Boolean algebra is the totally ordered set {false, maybe, true}. A very simple 3-valued logic!

It may seem hard to think and do math while avoiding the "law of excluded middle" - the axiom that says for any proposition P, either P or not P. In fact you can get used to avoiding it. I know lots of mathematicians who can. It's an ability you can turn on and off. (1/n)

- John Carlos Baez (@johncarlosbaez)

sarahzrf (Mar 27 2020 at 19:26):

yeah, i misread supseteq as subseteq

vikraman (Mar 27 2020 at 19:39):

This is the subobject classifier in $Set^{\rightarrow}$ or $\widehat{\Delta[1]}$

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

John Baez said:

So, I tweeted about bi-Heyting algebras, as one does, and I learned something that it seems you folks have already learned:

Any totally ordered set with a top and bottom element is a bi-Heyting algebra, and if this set has more than 2 elements it's not a Boolean algebra.

So, a very nice bi-Heyting but non-Boolean algebra is the totally ordered set {false, maybe, true}. A very simple 3-valued logic!

Yes, that looks about right :).

sarahzrf (Mar 28 2020 at 01:47):

hmm, so i wonder

sarahzrf (Mar 28 2020 at 01:49):

if a bi-heyting algebra is supposed to allow you to talk about both closures and interiors, is there some way of getting an interesting bi-heyting algebra out of a topological space? i was gonna suggest the borel algebra but that's boolean (in classical foundations at least)

sarahzrf (Mar 28 2020 at 01:54):

oh, you know what i wanna know now? what is the computational content of all this

sarahzrf (Mar 28 2020 at 01:54):

okay so it probably all comes back to linear logic, i never did think that thru...

John Baez (Mar 28 2020 at 02:17):

I don't know how to get a bi-Heyting algebra out of a topological space in an interesting way.

But this nLab article is nice:

https://ncatlab.org/nlab/show/bi-Heyting+topos

It shows the lattice of subobjects of any object in any presheaf category is bi-Heyting!

For example the lattice of subgraphs of a graph (using the category theorist's definition of "graph".)

So I now have vast numbers of bi-Heyting algebras to play with. :cowboy:

vikraman (Mar 28 2020 at 02:25):

@John Baez in particular, your example of 3-valued logic is also an instance of this, since it is the subobject classifier of presheaves over $\Delta[1]$

John Baez (Mar 28 2020 at 02:31):

Great, I was wondering about this and failing miserably to see how it was an example.

John Baez (Mar 28 2020 at 02:33):

So all totally ordered sets with top and bottom are also an instance of this.

John Baez (Mar 28 2020 at 02:34):

But it seems much more fun now to have non-totally-ordered bi-Heyting algebras.

Gershom (Mar 28 2020 at 04:20):

I haven't worked this through, but I think I can give another large class from the description. We know that finite joins distributing over potentially infinite meets = complete heyting algebra. Dually, finite meets over potentially infinite joins must = complete co-heyting algebra. When both hold, you get a bi-heyting algebra. A nice large case when both hold is any finite distributive lattice.

sarahzrf (Mar 28 2020 at 04:24):

haha i googled "finite distributive lattice" and image.png

John Baez (Mar 28 2020 at 06:01):

Nice! That's a big class, the finite distributive lattices. It's also nice that the opposite category of FinDistLat is FinPoset, so any finite poset gives a finite distributive lattice and thus a bi-Heyting algebra.

To get the finite distributive lattice corresponding to a finite poset $P$, first form the poset of upsets in $P$ with the reverse ordering (this is the free finite meet completion on $P$). Then form the distributive lattice of downsets in that. This is the free distributive lattice on $P$.

I'm sort of quoting the nLab, but I sort of wrote this part, to help me remember it.

Gershom (Mar 28 2020 at 06:07):

Right, that's the free distributive lattice. But that's not the birkhoff duality you describe. For that, just form the downsets, and you're done! (In the other direction, take the join-irreducible/join-prime elements to get the poset back).

(you can also do the same thing with upsets and meets if you prefer).

sarahzrf (Mar 28 2020 at 06:38):

i saw the word "downset" so just a quick note to anyone who might not know: downward-closed sets are (0, 1)-presheaves and taking x↓ is the (0, 1)-yoneda embedding

sarahzrf (Mar 28 2020 at 06:42):

(and the inclusions of downward-closed sets are some sort of fibration, maybe even the discrete ones... need to work that out (and whether "discrete" makes sense in this context))

John Baez (Mar 28 2020 at 17:31):

Right, that's the free distributive lattice. But that's not the birkhoff duality you describe. For that, just form the downsets, and you're done! (In the other direction, take the join-irreducible/join-prime elements to get the poset back.

Hmm, then perhaps I screwed up the nLab page. Oh, no, maybe I just misread it. Maybe you could check it:

• Finite distributive lattices

and either fix errors or tell me about them. It would be nice to make the explanation better, too.

sarahzrf (Mar 28 2020 at 19:11):

i just realized that the universal property i was thinking about with $Dec(H)$ and $Reg(H)$ might not have been as trivial as i decided after all

sarahzrf (Mar 28 2020 at 19:13):

well, ok, so what got me thinking about it again is that coq's ssreflect library defines a thing called classically like so:

Definition classically P : Prop := forall b : bool, (P -> b) -> b.

sarahzrf (Mar 28 2020 at 19:13):

(there's a coercion registered from bool to Prop so that b can be written there as if it were a proposition)

sarahzrf (Mar 28 2020 at 19:13):

now, this is easily equivalent to double negation

sarahzrf (Mar 28 2020 at 19:14):

because it's the same as ((P -> true) -> true) /\ ((P -> false) -> false), and false <-> False (where lowercase true and false are booleans being coerced to propositions, while uppercase True and False are fundamentally propositions, so logically equivalent but not judgmentally equal)

sarahzrf (Mar 28 2020 at 19:16):

but the reason why it's defined this way is for convenience of use—say you want to prove a goal which is a boolean coerced into a proposition, and you know H : classically P; then you can just apply H directly to your goal b and now you need to prove P -> b—you've weakened your goal using H

sarahzrf (Mar 28 2020 at 19:17):

whereas if it were defined as double negation, this use case would have to be a lemma

sarahzrf (Mar 28 2020 at 19:17):

but anyway: this felt to me like it was saying something like...

sarahzrf (Mar 28 2020 at 19:18):

"P as perceived by booleans is indistinguishable from ~ ~ P"

sarahzrf (Mar 28 2020 at 19:18):

which would be the criterion for a reflection, except that ~ ~ P need not be decidable, so i thought something odd was going on

sarahzrf (Mar 28 2020 at 19:19):

and then i decided that it was as simple as what i said earlier, but... now i'm suspicious again, because it seems as though we can maybe say that the reflection of $H$ into $Reg(H)$ is somehow "generated" by $Dec(H)$

sarahzrf (Mar 28 2020 at 19:25):

so, ok, if we have $P \in H$ we can contravariantly yoneda-embed it to get $y(P) \in coPSh(H)$, then we can restrict that along the inclusion of either $Reg(H)$ or of $Dec(H)$ to get a copresheaf on one of those. the fact that we have a reflection into $Reg(H)$ says that restricting along the inclusion into there gives us $y(\neg\neg P)$ (where $\neg\neg P$ is considered as an element of $Reg(H)$), but it's possible that the restriction to $Dec(H)$ is not representable at all.

sarahzrf (Mar 28 2020 at 19:28):

i swear i was going somewhere with this...

sarahzrf (Mar 28 2020 at 19:30):

oh!

sarahzrf (Mar 28 2020 at 19:31):

i think maybe we have something like... "if restricting $y(P)$ and $y(Q)$ to $Dec(H)$ gives the same thing, then it already does when you restrict to $Reg(H)$"

sarahzrf (Mar 28 2020 at 19:32):

or rather, i think thats the correct statement of what i vaguely wanted to say the whole time, but now im no longer sure it's actually true :sweat_smile:

sarahzrf (Mar 28 2020 at 20:40):

OKAY, here's a question!

sarahzrf (Mar 28 2020 at 20:42):

say a poset $P$ is markovian if for any monotone function $f : P \to 2$, we have $(\neg\forall x. f(x) = 1) \to \exists x. \neg(f(x) = 1)$

sarahzrf (Mar 28 2020 at 20:43):

of course, classically every poset is markovian

sarahzrf (Mar 28 2020 at 20:43):

markov's principle states that the discrete poset $\mathbb N$ is markovian

sarahzrf (Mar 28 2020 at 20:44):

now: if $P$ is markovian, does it follow that $P^\mathrm{op}$ is markovian?? or does anybody have a brouwerian counterexample?

sarahzrf (Mar 28 2020 at 20:45):

neither is instantly obvious to me, and i'm wondering if maybe i should instead define markovian as $(\neg\forall x. \neg(f(x) = 1)) \to \exists x. f(x) = 1$, which i believe is equivalent to $P^\mathrm{op}$ being markovian under my current definition

Vlad Patryshev (Mar 30 2020 at 04:07):

I wonder if this is the right topic, but I've just implemented Lawvere topologies (in Grothendieck toposes) in Scala: https://github.com/vpatryshev/Categories/blob/master/src/main/scala/math/cat/topos/LawvereTopology.scala
Comments/contributions welcome.

sarahzrf (Mar 31 2020 at 01:30):

ok i found my brouwerian counterexample :triumph:

sarahzrf (Mar 31 2020 at 01:31):

constructively: $\mathbb{N}^\mathrm{op}$ is markovian (as is anything with a greatest element), but if $\mathbb{N}$ under the standard ordering is markovian, then it also is when it is discrete, which is just markov's principle

sarahzrf (Mar 31 2020 at 01:31):

:sad:

sarahzrf (Mar 31 2020 at 01:32):

this is a pain...

sarahzrf (Mar 31 2020 at 01:35):

i wanted to be able to state "this satisfies LPO" as "decidable propositions are closed under quantification by monotone functions from this thing"

sarahzrf (Mar 31 2020 at 01:36):

but i think that's not equivalent to "we can decide between forall holds and exists counterexample"

sarahzrf (Mar 31 2020 at 01:36):

because converting between them hinges on being able to instantiate w/ a negated version, but that switches variance!

sarahzrf (Mar 31 2020 at 01:37):

does anybody know if there's work on generalizations of omniscience principles to ordered domains of discourse?

sarahzrf (Mar 31 2020 at 01:37):

is martin escardo maybe on this server...? :-)

Dan Doel (Mar 31 2020 at 02:31):

What is $2$? I thought $ℕ$ with $\leq$ would require that every $ℕ → 2$ is constant.

Dan Doel (Mar 31 2020 at 02:31):

So it would be Markovian, just like the opposite.

Dan Doel (Mar 31 2020 at 02:33):

Is $2$ actually the Sierpinski space?

sarahzrf (Mar 31 2020 at 02:45):

sorry yeah

sarahzrf (Mar 31 2020 at 02:45):

well no

sarahzrf (Mar 31 2020 at 02:45):

it's the Sierpinski space in the sense that it has the ordering you're thinking of

sarahzrf (Mar 31 2020 at 02:45):

but it's not the Sierpinski space in the sense that it's not the power set of the singleton, since we're working intuitionistically

Dan Doel (Mar 31 2020 at 02:50):

Yeah. The walking arrow or whatever.

Gershom (Mar 31 2020 at 08:24):

Btw John, thanks for the push. I fixed things up a bit and added some more tidbits.

sarahzrf (Mar 31 2020 at 15:57):

this seems like a possibly good place to mention that for a while now ive been working on a coq development of all kinds of depleted category theory (term ive coined for truth-value enriched / (0, 1)-category theory / category theory specialized to preorders)

sarahzrf (Mar 31 2020 at 16:01):

goal is to be something where you can one day think to yourself "hmmmmmmm separating conjunction is Just™ depleted day convolution" and then immediately be able to actually get something out of this in coq by just doing, say

Require Import depleted.psh.

Definition program_state : Type := ...
Instance program_state_proset : Proset program_state := ...
Instance program_state_promonoidal : Promonoidal program_state := ...

Definition assertion : Type := PSh program_state.

and bam, now writing ⊗ means separating conjunction

sarahzrf (Mar 31 2020 at 16:02):

and you get all of your logical connectives for free from structure on (depleted) presheaves

sarahzrf (Mar 31 2020 at 16:03):

or, say, you read about linear logic for constructivism, go "oh shit that sounds really cool", decide you want to play with the chu construction

sarahzrf (Mar 31 2020 at 16:04):

great, you already have complete heyting algebras and a bunch of lemmas about them to play with, and the ordering on a product, and stuff like that, that should be plenty to make you not lose momentum when you realize how much basic theory you were taking for granted if you have adhd like me :upside_down:

sarahzrf (Mar 31 2020 at 16:05):

well, that's my ideal here for what function this development should be able to serve, anyway

sarahzrf (Mar 31 2020 at 16:05):

hope it sounds appealing to someone other than me :-)

sarahzrf (Mar 31 2020 at 16:07):

dunno how many coq users there are here

sarahzrf (Mar 31 2020 at 16:17):

(this is why i was asking about the "markovian" stuff—i'm working on a module for this development with some of the results from that escardó omniscience paper, like the omniscience of the conats, so that if you want to use bool instead of Prop in some places like depleted presheaves for computability purposes, you can still talk about what kinds of infs/sups it's possible to take)

sarahzrf (Mar 31 2020 at 16:17):

(and since im working with all kinds of preordered sets, asking about restriction to only monotone predicates seemed like a natural generalization)

Thomas Read (Mar 31 2020 at 17:52):

I'm not an expert on this kind of stuff, but it seems cool so I appreciate you talking about it here!

Nathanael Arkor (Mar 31 2020 at 21:16):

this sounds like it could be a really useful project for gaining intuition for some of the more sophisticated categorical constructions and putting it in a more familiar context!

sarahzrf (Mar 31 2020 at 21:16):

oh it definitely has been @_@

Nathanael Arkor (Mar 31 2020 at 21:16):

(even not considering the Coq library)

Nathanael Arkor (Mar 31 2020 at 21:18):

depleted category theory (term ive coined for truth-value enriched / (0, 1)-category theory / category theory specialized to preorders)

did you consider "thin category theory"?

sarahzrf (Mar 31 2020 at 21:21):

hmmmmm, im not sure i did, and it does seem more immediately obvious to more people, if less punny

sarahzrf (Mar 31 2020 at 21:21):

although, um

sarahzrf (Mar 31 2020 at 21:21):

there's a certain shift in perspective, i think, between thinking of an object as a "thin category" and as a "(0, 1)-category"

sarahzrf (Mar 31 2020 at 21:22):

which is my rationalization for why i wanna stick to "depleted" :>

sarahzrf (Mar 31 2020 at 21:22):

if i say "i have this thin category C, and then a presheaf F on it", then you're probably gonna assume it takes values in Set

sarahzrf (Mar 31 2020 at 21:23):

if i say "i have this (0, 1)-category C, and then a presheaf F on it", then you should assume it takes values in truth values!

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

that's probably a fair assumption

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

and coming up with names for things is half the fun :P

sarahzrf (Mar 31 2020 at 21:24):

i guess there's a point to be made that if you say you're doing "thin category theory", that suggests that you're only working with thin categories, and hence you shuoldnt be considering presheaves outside of the second kind

sarahzrf (Mar 31 2020 at 21:24):

but. i like my term =w=

Reid Barton (Mar 31 2020 at 21:24):

oh, depleted is the opposite of enriched?

sarahzrf (Mar 31 2020 at 21:24):

yes haha

sarahzrf (Mar 31 2020 at 21:25):

at least when you talk about uranium, i think

sarahzrf (Mar 31 2020 at 21:25):

and there are certainly people who treat category theory as if it were radioactive...

Nathanael Arkor (Mar 31 2020 at 21:28):

only in category theory do you get something enriched when you deplete...

sarahzrf (Mar 31 2020 at 21:29):

well, no, that's my logic—it's "enriched", but in fact the category you enrich over (truth values) is strictly less rich than the default (Set), so you're not really enriching, you're depleting

John Baez (Mar 31 2020 at 21:37):

I keep advocating for "impoverished", but the uranium analogy makes me understand "depleted" a bit better.

sarahzrf (Mar 31 2020 at 21:39):

"depleted" rolls off the tongue better :smirk:

Reid Barton (Mar 31 2020 at 21:43):

Are there foods which are specially modified to have less vitamin D, or whatever?

sarahzrf (Mar 31 2020 at 21:43):

lol

Matteo Capucci (he/him) (Mar 31 2020 at 22:33):

gluten-free categories

Matteo Capucci (he/him) (Mar 31 2020 at 22:34):

we already have burritos, tacos and enchiladas

T Murrills (Mar 31 2020 at 22:38):

functors G and F, pronounced ‘gluten’ and ‘free’ respectively,

Reed Mullanix (Mar 31 2020 at 22:40):

If we have gluten free functors, they must be adjoint to some gluten forgetful functor :thinking:

T Murrills (Mar 31 2020 at 22:42):

also I like depleted because it comes from a nicely nounable verb; you can talk about “depletion” functors or “depleting” a category when moving between categories you enrich over. (enriching over truth values thus gives a (nontrivial) “maximally depleted” version of—I want to say—any category enriched over [a category with an initial object]? (maybe not, I’m not sure yet. Something that works in a special way with the composition/something like a “monoidal zero”. Concept is out there, I just don’t know it yet!) Anyway, the depletion from such an enriched category to one enriched over truth values suggests the usage of “depleted” given here)

sarahzrf (Apr 02 2020 at 03:44):

@Jade Master youll be pleased to know that my depleted CT development includes definitions of quantales and depleted day convolution, so u could formalize that blog post extremely quickly in it by just defining the monoidal proset generated by a petri net ^__^

Jade Master (Apr 02 2020 at 03:55):

Ooh interesting. I'd love to do something with this...

sarahzrf (Apr 02 2020 at 03:55):

do you know any coq

Jade Master (Apr 02 2020 at 04:30):

I don't but I want to learn!

sarahzrf (Apr 04 2020 at 06:56):

since i guess ive turned this into the (0, 1)-category theory topic

sarahzrf (Apr 04 2020 at 06:56):

what's a (1, 1)-filter?

sarahzrf (Apr 04 2020 at 06:57):

actually a (1, 1)-ideal is probably a better idea

sarahzrf (Apr 04 2020 at 06:58):

actually no

i think a (1, 1)-filter might be a flat functor to Set

but i'd need to figure out the definition of flat functors first :upside_down:

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

sarahzrf said:

since i guess ive turned this into the (0, 1)-category theory topic

Can I just get some clarity about what the indices mean in eg (0,1)-category? You hinted at it earlier, but I figure I should make sure I'm understanding right

Matteo Capucci (he/him) (Apr 04 2020 at 12:23):

An $(n,k)$-categories is a category with $n$ "levels" of morphisms (objects are $0$-morphisms) and such that every morphism above level $k$ is invertible

Matteo Capucci (he/him) (Apr 04 2020 at 12:26):

Beware that we tacitily assume there are always infinitely many level of morphisms, albeit an $(n,k)$-category has only one morphism (up to isomorphism) above level $n$.

Matteo Capucci (he/him) (Apr 04 2020 at 12:26):

So it makes sense to talk about $(n,k)$-categories for $k>n$

Matteo Capucci (he/him) (Apr 04 2020 at 12:36):

A $(0,1)$-category has a non-trivial collection of objects ($0$-level), and a trivial collection of $1$-morphisms between any two objects ($1$-level). Since $k=1$, you can have non-invertible $1$-morphisms. Hence your category is a poset.

Matteo Capucci (he/him) (Apr 04 2020 at 12:38):

A $(1,1)$-category has a non-trivial collection of objects ($0$-level), a non-trivial collection of $1$-morphisms between any two objects ($1$-level) and a trivial collection of $2$-morphisms between any parallel $1$-morphisms. Since $k=1$, you can have non-invertible $1$-morphisms. Hence your category is a normal category.

Matteo Capucci (he/him) (Apr 04 2020 at 12:39):

A $(1,0)$-category has non-trivial objects and $1$-morphisms, trivial $2$-morphisms and every $1$-morphism is invertible. Hence your category is a groupoid!

Matteo Capucci (he/him) (Apr 04 2020 at 12:45):

Beware: 'trivial' means either a singleton or empty, 'non-trivial' means 'not necessarily trivial' :sweat_smile:

Morgan Rogers (he/him) (Apr 04 2020 at 13:06):

Thanks! That clears that up.

Amar Hadzihasanovic (Apr 04 2020 at 13:09):

@Matteo Capucci This makes $(0,0)$-categories setoids (set + equivalence relation) and not sets, right?

Amar Hadzihasanovic (Apr 04 2020 at 13:11):

In fact I think this should always allow that there is an equivalence relation on parallel $n$-morphisms in an $(n,k)$-category...

Matteo Capucci (he/him) (Apr 04 2020 at 13:14):

Indeed... that's funny.

Matteo Capucci (he/him) (Apr 04 2020 at 13:18):

I don't know then

Amar Hadzihasanovic (Apr 04 2020 at 13:21):

Oh, I don't think that's a problem. I noticed this kind of thing arising when one tries to pass from
“$n$-categories as $n$-dimensional things + composition operation on $n$-cells”
to
“$n$-categories as $\infty$-dimensional things that are 'trivial' above $n$”

Amar Hadzihasanovic (Apr 04 2020 at 13:22):

When you turn the composition into $(n+1)$-dimensional “compositors”

Amar Hadzihasanovic (Apr 04 2020 at 13:24):

Because to pass from the first to the second you would need to introduce some $(n+1)$-cells, and then you would make the most economical choice: do not duplicate any $n$-cells!

Amar Hadzihasanovic (Apr 04 2020 at 13:25):

But to obtain something equivalent to the first from the second, you would need to state that as an additional property: there are no duplicates...

Amar Hadzihasanovic (Apr 04 2020 at 13:26):

And this $(n,k)$-business, as you say, is done from the second perspective rather than the first

Amar Hadzihasanovic (Apr 04 2020 at 13:26):

Besides, it makes constructivists happier, so why not?

Reid Barton (Apr 04 2020 at 13:27):

You should consider categories up to equivalence, so that setoids and sets are the same. Also by the same logic, a (0, 1)-category would be a preorder, not a partial order (a partial order is a preorder in which $x \le y \wedge y \le x \implies x = y$).

Amar Hadzihasanovic (Apr 04 2020 at 13:34):

That's context-dependent, though. If we are considering these $(n,k)$-things as special $\infty$-things, then they are not stable under equivalence, e.g. a set would be equivalent to any disjoint union of contractible $\infty$-groupoids.

Amar Hadzihasanovic (Apr 04 2020 at 13:36):

The definition as given by Matteo needs some mentions of strict equality.

Amar Hadzihasanovic (Apr 04 2020 at 13:37):

Unless maybe we want to replace every mention of “uniqueness” with “contractible space of choices”...

Amar Hadzihasanovic (Apr 04 2020 at 13:38):

(Which is what you get if you stated it in HoTT, I guess.)

Reid Barton (Apr 04 2020 at 13:38):

If you're working in some $\infty$-context then you should generally interpret "unique" as "contractible space of choices".

Amar Hadzihasanovic (Apr 04 2020 at 13:40):

We were defining some $\infty$-things, but nobody said we were doing it in an $\infty$-context :)

Amar Hadzihasanovic (Apr 04 2020 at 13:41):

I guess I was thinking more of “defining what the $(n,k)$-categories are in a specific model of higher categories”.

Matteo Capucci (he/him) (Apr 04 2020 at 14:15):

Yeah it's not really a problem to have equivalences in the last level, yet I can't reconcile it with whta is mentioned here https://ncatlab.org/nlab/show/%28n%2Cr%29-category

Matteo Capucci (he/him) (Apr 04 2020 at 14:16):

Like, the definition and the 'periodic table' disagree, as @Amar Hadzihasanovic points out

sarahzrf (Apr 04 2020 at 20:33):

note that in general, an (n, r)-category for r > n is only interesting when r = n+1

sarahzrf (Apr 04 2020 at 20:33):

larger r is equivalent to that

sarahzrf (Apr 04 2020 at 20:33):

and r = n+1 means you have a preorder on the highest-level cells

sarahzrf (Apr 25 2020 at 17:55):

sarahzrf said:

i just realized that the universal property i was thinking about with $Dec(H)$ and $Reg(H)$ might not have been as trivial as i decided after all

HAHAHA i came back to this just now and i figured it out :D

sarahzrf (Apr 25 2020 at 17:56):

• $Dec(H)$ is dense in $H$

sarahzrf (Apr 25 2020 at 17:56):

• $Dec(H)$ is codense in $Reg(H)$

sarahzrf (Apr 25 2020 at 17:57):

wait, i think that's right.

sarahzrf (Apr 25 2020 at 18:04):

ok nvm i realized that the reasoning i was working on only really applied to the heyting algebra of truth values >.>

sarahzrf (Apr 25 2020 at 18:05):

might still be true but uhhh i dont know