Hi Todd,

it’s Eduardo :)

Sorry, eparejatobes (I don’t know your given name) – how is the second equation in the second line after

L¬¬ is an exponeital ideal in L (where there is a typo – you mean y instead of a) supposed to be obvious? I mean, I can prove it, but it’s not totally obvious to me without some calculation.

*Whoah!* that’s wrong in *many* ways! don’t know what I was thinking when I wrote that. I mean, it may be true, but not obvious at all, and in fact I don’t know how to prove it :) Thanks for spotting it. I’ve been looking for a way to fix this, and found a nice proof of $\neg\neg$ perserving finite products in this lecture notes:

So, here follows what I have:

First of all, let’s state some properties of negation which will be of great use later on; most of them are direct consequences of the definition $\neg x = x \Rightarrow 0$; note that this means that

$x \wedge y = 0 \iff x \leq \neg y$- $\neg \dashv \neg^{op}$ from the symmetry of meets
- $\neg \neg \neg = \neg$ because every poset adjunction is idempotent
- $a \wedge b = 0 \iff a \wedge (\neg\neg b) = 0$ For this, take $a \wedge b = 0 \iff a \leq \neg b$, and from the previous one $a \leq \neg b \iff a \leq \neg\neg\neg b = \neg(\neg\neg b)$ and then this equivales to $a \wedge (\neg\neg b) = 0$.

We can factor the monad $\neg\neg$ coming from the $\neg \dashv \neg^{op}$ adjunction as:

$L \to L_{\neg\neg} \to L$Let’s see first that the reflection $\neg\neg$ preserves meets; as a reflective subcategory, we have that finite meets in $L_{\neg\neg}$ are just finite meets in $L$; so that $\neg\neg \colon L \to L_{\neg\neg}$ presrving finite meets is equivalent to

$\neg\neg(a\wedge b) = \neg\neg a \wedge \neg\neg b$One inclusion is always true for a functor between posets with finite meets

$\neg\neg(a\wedge b) \leq \neg\neg a \wedge \neg\neg b$(every functor between cartesian cats is colax monoidal). Now, for the other one:

$\neg\neg a \wedge \neg\neg b \leq \neg\neg(a\wedge b)$is equivalent by adjunction to

$(\neg\neg a \wedge \neg\neg b) \wedge \neg(a\wedge b) = 0$reorganizing this to

$(\neg\neg a \wedge (\neg\neg b \wedge \neg(a\wedge b)) = 0$we can apply 3 to get

$a \wedge (\neg\neg b \wedge \neg(a\wedge b)) = 0$doing the same with $b$ we arrive at

$(a \wedge b) \wedge \neg(a\wedge b) = 0$which is always the case, via adjunction and the unit of $\neg\neg$:

$(a \wedge b) \leq \neg\neg(a\wedge b)$From this we get that double negation also preserves finite meets.

This is in the Elephant, A.4.3.1. The key is noting that

$\neg\neg(x\wedge y) = \neg\neg x \wedge \neg\neg y = \neg\neg(\neg\neg x \wedge y)$because of $\neg\neg$ idempotent. Now, taking $a \in L_{\neg\neg}$, $x,y \in L$ we have

$\begin{matrix} & L(x, y \Rightarrow a) \simeq \\ closed: & L(x\wedge y, a) \simeq \\ adjunction: & L(\neg\neg(x\wedge y), a) \simeq \\ property above: & L(\neg\neg(\neg\neg x\wedge y), a) \simeq \\ adjunction: & L(\neg\neg x \wedge y, a) \simeq \\ closed: & L({\neg\neg}x, y \Rightarrow a) \simeq \\ \end{matrix}$So we have

$x \leq y \Rightarrow a \iff \neg\neg x \leq y \Rightarrow a$So taking $y = \in L, x = y \Rightarrow a$ we get

$\neg\neg (y \Rightarrow a) = y \Rightarrow a$that is, $L_{\neg\neg}$ is an exponential ideal. From this, it is immediate that

- $L_{\neg\neg}$ is closed, with $\Rightarrow_{\neg\neg} = \Rightarrow$
- $i$ closed

From this is easy to get that $L_{\neg\neg}$ is a Boolean algebra etc.

What I don’t know how to get is that also the reflection is closed. I mean, in a different way than what you have. Really nice the expression:

$\neg(a \Rightarrow b) = \neg\neg a \wedge \neg b$haven’t seen that before.

So, sorry for the noise :)

Apart from that, does anyone knows something about Heyting algebras for which $\neg \dashv \neg^{op} \dashv \neg$? thanks!

]]>Sorry, eparejatobes (I don’t know your given name) – how is the second equation in the second line after

$L_{\neg\neg}$ is an exponeital ideal in $L$

(where there is a typo – you mean $y$ instead of $a$) supposed to be obvious? I mean, I can prove it, but it’s not totally obvious to me without some calculation.

]]>I don’t know if what follows is shorter, but I think is clearer:

First, factor the ${\neg\neg}$ monad as

$L \to L_{\neg\neg} \to L$and call the reflection $L \to L_{\neg\neg}$ also ${\neg\neg}$; the inclusion $L_{\neg\neg} \to L$ will be implicit. We obviously have

- ${\neg\neg} \dashv i$
- $i$ fully faithful
- $i$ preserves and $L_{\neg\neg}$ has finite meets

From 3 we have that for $a,b \colon L_{\neg\neg}$

$a \wedge_{\neg\neg} b = a \wedge b = {\neg\neg}(a \wedge b)$Now, everything is easy once we note that

$L_{\neg\neg}$ is an exponential ideal in $L$

This is almost immediate from the definition of $\neg(x) = x \Rightarrow 0$; for arbitrary $x,y \colon L$:

${\neg\neg}(x \Rightarrow y) = ((x \Rightarrow y) \Rightarrow 0) \Rightarrow 0 = x \Rightarrow ((a \Rightarrow 0) \Rightarrow 0) = x \Rightarrow ({\neg\neg}(y))$that is,

- ${\neg\neg}(x \Rightarrow y) = x \Rightarrow ({\neg\neg} y)$

Now, from this if $x \colon L, a \colon L_{\neg\neg}$, then

${\neg\neg}(x \Rightarrow a) = x \Rightarrow ({\neg\neg} a) = x \Rightarrow a$so that $x \Rightarrow a \colon L_{\neg\neg}$ and we get $L_{\neg\neg}$ exponential ideal.

We have, for $x,y,c \colon L_{\neg\neg}$:

$\begin{matrix} L_{\neg\neg}(x\wedge_{\neg\neg} y, c) \simeq \\ L(x \wedge y, c) \simeq \\ L(x, y \Rightarrow c) \simeq \\ L_{\neg\neg}(x, y \Rightarrow c) \end{matrix}$Note that for $a,b \colon L_{\neg\neg}$ trivially

$a \Rightarrow_{\neg\neg} b = {\neg\neg}(a \Rightarrow b) = a \Rightarrow b$and from this both

- the reflection $L \to L_{\neg\neg}$
- the inclusion $L_{\neg\neg} \to L$

are *closed*. We get then ${\neg\neg}$ closed.

The only thing left is

Every functor between cartesian categories is colax monoidal, which here amounts to

${\neg\neg}(x \wedge y) \leq {\neg\neg}(x)\wedge_{\neg\neg} {\neg\neg}(y)$(this is the easy one, of course). For the reverse, first note that Kleisli extension yields

$x \leq {\neg\neg} y \iff {\neg\neg} x \leq {\neg\neg} y$Now, for $x,y \colon L, a = {\neg\neg} a \colon L_{{\neg\neg}}$

$\begin{matrix} & L(x\wedge y, a) \simeq \\ closed: & L(x, y \Rightarrow a) \simeq \\ a = {\neg\neg}a : & L(x, y \Rightarrow {\neg\neg} a) \simeq \\ props of {\neg\neg}: & L(x, {\neg\neg}(y \Rightarrow a)) \simeq \\kleisli + exp ideal: & L({\neg\neg}x, y \Rightarrow a) \simeq \\ closed: & L({\neg\neg}x \wedge y, a) \end{matrix}$Applying the same steps to $y$, we get a bijection

$L(x\wedge y, a) \simeq L({\neg\neg}x \wedge {\neg\neg} y, c)$Taking the map given by the unit at $x\wedge y$,

$x \wedge y \to {\neg\neg}(x \wedge y)$we get what we were looking for:

${\neg\neg}x \wedge_{\neg\neg} {\neg\neg} y = {\neg\neg}x \wedge {\neg\neg} y \leq {\neg\neg}(x \wedge y)$This is just *Proposition A.4.3.1* of the Elephant adapted to this context.

As for $L_{\neg\neg}$ being a Boolean algebra, it follows at once from double negation in $L_{\neg\neg}$ being just the double negation of $L$ resctricted to $L_{\neg\neg}$. Then, for $a \colon L_{\neg\neg}$:

${\neg\neg}_{\neg\neg} a = {\neg\neg} a = a$Summing up,

the inclusion $L_{\neg\neg} \to L$ is

- fully faithful,
- closed, and
- preserves any (in particular finite) meets that exist in $L$

the reflection $L \to L_{\neg\neg}$ is

- eso,
- closed, and
- preserves finite meets
- it also preserves joins, of course

From this we get that

double negation ${\neg\neg} \colon L \to L$ is

- closed,
- and preserves finite meets

By symmetry of $\wedge$, we get

$\neg \dashv \neg^{op}$and ${\neg\neg} = \neg^{op}\neg$. It’d be nice if being De Morgan would be equivalent to this adjunction being an ambijunction

$\neg \dashv \neg^{op} \dashv \neg$one such Heyting algebra is automatically De Morgan; guess there should be examples of De Morgan Heyting algebras for which $\neg^{op}$ is not *left* adjoint to $\neg$.

I’ve moved the comments on theorem numbering to their own thread: Theorem numbering.

]]>But what I am hesitant (no: unwilling) to do is to preemptively think up anchor names for everything in sight even before I refer to a single one.

Me too. But in that case, I just leave them unnumbered until I decide that I wish to refer to them.

I agree, the bug should be fixed; and when it is, then you can just make everything numbered to start with, without thinking of names. However, so long as you cannot think of a name, then numbering it gives you no additional benefit (and leaving it unnumbered works around the bug, while we have it).

]]>Bug or no bug, there’s not much point to numbering the theorems/remarks/etc if you can’t refer to them later by number. And the only safe way to do that is with the anchors.

That’s what we currently do anyway, being forced by the bug: if I want to refer to something by number, I need to anchor everything in between in order for the numbers to come out right.

But what I am hesitant (no: unwilling) to do is to preemptively think up anchor names for everything in sight even before I refer to a single one. It would be good, I agree, but there is some limit being reached here.

]]>Bug or no bug, there’s not much point to numbering the theorems/remarks/etc if you can’t refer to them later by number. And the only safe way to do that is with the anchors.

]]>Yes, very true.

On the other hand, maybe there is hope that this bug will disappear some day? I keep liking the idea that the software helps me save time, instead of me having to invest time to work around it…

]]>If we do use numbered theorem environements, I think we should always also include an anchor name:

```
+-- {: .num_remark #MyRemark}
```

IIRC there is an instiki bug that rears its head when some, but not all, of the numbered theorems on a given page have anchor names assigned.

]]>I think that’s a good suggestion, Urs (and I’ve begun doing that, but not consistently).

I’d like to propose another suggestion: when including redirects, make a point of including plural forms. That way a link can be made directly from the plural, without extra fuss.

]]>when it should be

`+-- {: .un_remark}`

I have a general suggestion: let’s use

```
+-- {: .num_remark}
```

and similar by default. That’s more useful when an entry grows. (And all entries will grow *eventually*…)

Oops! Yes, I see it now – thanks.

]]>It’s an subtle typo; I had

```
+-- {: un_remark}
```

when it should be

```
+-- {: .un_remark}
```

It’s fixed now.

]]>Toby, I see you made edits at Heyting algebra, in particular putting the remark in an environment. But it renders funny, and I can’t see what’s wrong with the syntax. Does it look funny to you, and if so can you fix it?

]]>No, I think I was jumping to unjustified conclusions and being confused, sorry.

]]>Todd, I just broke your last link by making it permanent: Heyting algebra: Proofs.

]]>Sorry, could you explain what you mean? Is there an easier way to see this than what I put down in Heyting algebra: Proofs?

]]>That does at first seem a little surprising; but then when I think about it in terms of logic, it’s obvious. (-:

]]>Actually, your comment made me realize how all this is connected with the double negation translation (a page I have just started), which I would imagine requires machinations of the sort worked out at Heyting algebra.

Here’s something that actually took me by surprise: double negation on a Heyting algebra $\neg\neg: L \to L$ preserves not only finite meets, but the implication operation as well! It follows from this that the inclusion $L_{\neg\neg} \to L$ also preserves implication (contrary to what was stated before at Heyting algebra, so I guess this will take someone else besides me by surprise (-: ).

]]>That’s intriguing! I would have expected there to be an abstract reason for that, but I can’t think of one right now. Abstract nonsense implies that $Bool \to Heyt$ has a left adjoint, whose unit is then necessarily a Heyting algebra map, but then how can we identify the Boolean reflection with $L_{\neg\neg}$?

]]>I’ve inserted some proofs of statements made at Heyting algebra, particular on the “regular element” left adjoint to the full inclusion $Bool \to Heyt$.

The proof that $L \to L_{\neg\neg}$ preserves implication seemed harder than I was expecting it to be. Or maybe my proof is a clumsy one? If anyone knows a shorter route to this result, I’d be interested.

]]>