Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I tried to structure the entry Heyting algebra a bit more. Check if you like it.
I also added a little bit to the Examples-section.
In the section on toposes it says that a “Grothendieck (0,1)-topos” is a locale. Is that correct? Shouldn’t it say: a Grothendieck (0,1)-topos is a category of open subsets of a topological space?
The entry looks good.
Shouldn’t it say: a Grothendieck (0,1)-topos is a category of open subsets of a topological space?
Why do you say that? Just like a Grothendieck 1-topos need not have enough points, a (0,1)-topos need not either.
OK, I can vaguely see the point of all those Definition boxes, especially if we were later to put in proofs for the equivalences between them, but is there a reason for separating out Remarks like that? Is there no room for a paragraph that just stands on its own?
Why do you say that?
Sorry, that was nonsense. Not sure why I said that.
is there a reason for separating out Remarks like that?
I like it. It helps me scan the entry very quickly for information. But feel free to delete the remark-environments again, or some of them, if you feel that’s better.
I’ve never liked Remark environments in books; Definition/Theorem/Proof are formal but remarks are not, so Remark environments only make sense to me in books (like Walter Rudin’s) where every paragraph is numbered and you want a word to stick in front of the number when citing it. After our discussion about the proof environment at Eckmann-Hilton argument, I was afraid that you wanted these too. But since you write
feel free to delete the remark-environments again, or some of them
I don’t feel threatened that the Lab will become as ugly as all that. (^_^)
I think Remark environments make sense when (1) you want to refer back to the remark later (“see Remark 4.3”) or (2) you want a paragraph or a group of paragraphs to be “set apart” from the rest of the text as a sort of “side comment,” so that upon encountering the line space after the remark-environment the reader thinks “okay, that digression is over, now back to the main development.”
My only aim is to make the nLab a useful source of information. Useful for me also means that I can extract information from an entry efficiently and quickly – – say when having a quick glance at an entry while in the middle of the discussion with somebody else. For that i want to have it a structure as clear as possible.
We have or had a bunch of entries that were not structured very well. One had to read the whole entry carefully line by line to get the relevant information. For instance there were some tendencies to write historical or terminological remarks before the definition was even stated, to intersperse the definition with plenty of paranthetical remarks or with examples or consequences before it was even fully stated, and things like that. I tried and will continuously try to restructure such entries, to make them more efficiently readible, will move historical remarks to the end of the entry, will try to separate clearly definitions from side remarks from examples, etc.
In my attempts to add structure to entries, maybe I am overshooting here and there and adding too much structure. Since I am not dogmatic about any of this but just want to have useful entries, you should all feel free to in turn polish my edits if you find them misguided.
I agree that the organisation of entries is often bad, (although of course this is better than no entry at all).
If a remark is truly an aside, then it probably belongs in a different place. I’ve done this with half of one remark, which began “for example” (and also added to it). The rest of that remark, however, seems to me part of the main development of the definition, so I removed it from the Remark environment. Another Remark environment remains.
Urs, the thing which I do not like about structuring is that the entries grow with all the extra data, extra tables, extra titles, extra fonts, extra boxes etc. I myself remember things very visualy and the shorter is the text i comprehend and remember it better, after I understand it once. So in conclusion I like the structure and levels of strcuture when an entry grows already big before blwing it additionally. But for small entries which have 2-3 paragraphs and where the visual memory and visual comprehension works best, I am irritated when it becomes full of tables.
So in conclusion I like the structure and levels of strcuture when an entry grows already big before blwing it additionally. But for small entries which have 2-3 paragraphs and where the visual memory and visual comprehension works best, I am irritated when it becomes full of tables.
We can do something about this: expand these short entries! ;-)
(The thing is if you create an entry that is still very short, I will add the TOC immediately so that it is there later when the entry grows bigger. For if I don’t do it immediately, I will forget to do it. And since many of you don’t do it, nobody would.)
And since many of you don’t [add the TOC], nobody would.
I’m now good at adding the TOC, so that I get a chance to add it the right way rather than Urs’s wrong way. (We don’t change each other’s versions.) Without Urs to spur me, I might forget!
I agree with Zoran that there is an advantage to shorter things; it’s easier for me to “grok” a page, or a section of a page, if it doesn’t require lots of scrolling up and down (or even left and right!) to read. For this reason I sometimes change displayed equations to inline ones, if they are small, and collapse bulleted/numbered lists into a paragraph.
For instance, if a definition has only two fairly short conditions, I think it is easier to read in a paragraph rather than in a numbered list. I think lists are only helpful when they contain at least three entries, and often three or even four conditions can be more easily grasped when described in a paragraph.
I’m not against organization/structure as such, but I think the point is not to let the structure overshadow the content.
Okay. I get the point.
In contrast to Mike, I’ve come to like spread out white space and bulleted lists after seeing Urs’s usage of them! I use the latter a lot more now, even in simple emails.
Okay, that’s useful to know, too! :-)
Explicitly state a number of simple properties used in the proofs.
These facts are frequently useful in themselves when thinking about Heyting algebras, so it’s good to have them stated cleanly in the “Properties” section. This should also help with simplifying the proofs of the theorems, letting them focus on the main ideas.
Add an “Idea” section, as suggested at Template page.
I have added more hyperlinks to technical terms (such as to logical conjunction for “and”, etc.) and I have taken the liberty of slightly adjusting the wording in the first paragraph (here).
Thanks, Urs! (I’ve adjusted links slightly: one went to conjunction which seems to be something different.)
I think I’ve made most of the changes to this page that I had my eye on for now. There’s one more which I’d like to get feedback on before I go and try to make it: currently the page defines a Heyting algebra to be a poset. But it seems to me that some important examples of Heyting algebras are most naturally modeled instead as preorders/prosets.
In particular, perhaps the prototypical Heyting algebra is the collection of propositions in some logic, ordered by syntactic entailment. Given two propositions that are syntactically different (e.g., and for some ), I think one typically doesn’t want to take them to be the same proposition, even when there’s a theorem that they’re equivalent. Accordingly, the implication page already describes this as a preorder.
So my feeling is that the most natural definition of a Heyting algebra should not require to be antisymmetric. The main consequence of that in this page would be that instead of equations like , we should be writing equivalences. The definition also should then make clear that is only a preorder, not a poset, and add that many authors do require a Heyting algebra to be a poset. What do you think?
This is not different from the situation with Boolean algebras, and it’s completely standard to require antisymmetry in that case. I think it’s best to stick to the standard definitions. In the merely preordered case one sometimes says Heyting prealgebra.
In the case of the propositions in logic, I would just say that they syntactic Heyting algebra is the quotient of propositions by bi-entailment. Two propositions that entail each other aren’t the same proposition, but they induce the same object of the Heyting algebra. This, again, has plenty of analogues elsewhere in categorical logic, e.g. two terms in type theory that are judgmentally equal aren’t the same term, syntactically speaking (in the fully explicit sense that terms would be represented in a proof assistant), but they induce the same morphism of the syntactic category.
I sort of agree that the categorically natural notion doesn’t require asymmetry. But then we have to treat those objects category-theoretically, in particular considering two of their elements “the same” when they are isomorphic rather than just equal. From a univalent perspective, therefore, the notion of “equality” for those elements should be isomorphism – and in the preordered case we’re fortunate that we can even achieve that in classical set-theoretic foundations by simply taking the poset quotient.
If one wants to make Heyting algebras only a preorder, one would have to do the same thing with every other structure in (0,1)-category theory, such as lattices, distributive lattices, semilattices, pseudolattices, suplattices, complete lattices, frames, sigma-frames, coframes et cetera.
Lattices have a purely algebraic definition based upon the meets and joins of lattices being commutative idempotent monoid operations satisfying certain absorption laws, where any statement involving the partial order could be rewritten as an equation involving the meet or join. As a result, Heyting algebras could be defined in any symmetric monoidal category with diagonals. If one makes Heyting algebras a preorder they can only be defined in a finitely complete category, since lattices without antisymmetry are not algebraic.
Thanks, Mike, that’s helpful. I’ll limit myself in that direction to adding a link to Heyting prealgebra, then, and perhaps trying to expand the latter page a bit with the thoughts in your last comment.
Is there a term for the non-antisymmetric version of a lattice, or of a Boolean algebra? There is preframe, but with a different meaning.
A non-antisymmetric version of a lattice is a thin bicartesian category, or equivalently a bicartesian proset.
Reverted redirects, see discussion at complete Heyting algebra
1 to 39 of 39