Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• I ended up polishing type theory - contents (which is included as a floating table of contents in the relevant entries):

1. expanded and re-arranged the list under “syntax”, created stubs for the missing items definition and program

2. expanded the (logic/type theory)-table to a (logic/category theory/type theory)-table and subsumed some of the items into it that were floating around elsewhere.

• at axiom of choice into the section In dependent type theory I have moved the explicit statement taken from the entry of dependent type theory (see there for what I am talking about in the following).

One technical question: do we need the

  : true


at the very end of the formal statement of the theorem?

One conceptual question: I feel inclined to add the following Remark to that, on how to think about the fact that the axiom of choice is always true in this sense in type theory. But please let me know what you think:

Heuristically, the reason that the axiom of choice is always true when formulated internally this way in dependent type theory is due to the fact that its assumption thereby is stated in constructive mathematics:

Stated in informal but internal logic, the axiom of choice says:

If $B \to A$ is a map all whose fibers are inhabited, then there is a section.

But now if we interpret the assumption clause

a map all whose fibers are inhabited

constructively, we have to provide a constructive proof that indeed the fibers are inhabited. But such a constructive proof is a choice of section.

So constructively and internally the axiom is reduced to “If there is a section then there is a section.” And so indeed this is always true.

Would you agree that this captures the state of affairs?

• I added a sentence to fundamental group which contains a link to an example for a fundamental group of an affine scheme.
• split off total complex from double complex. Let the Definition-section stubby, as it was, but added a brief remark on exactness and on relation to total simplicial sets, under Dold-Kan and Eilenberg-Zilber. More to be done.

• Dedekind completions of quasiorders (not just linear orders) may now be found at Dedekind completion. Example: the lower Dedekind completion of the quasiorder of continuous functions is the quasiorder of lower semicontinuous functions.

• I put a bunch of stuff there that might be of interest to the logicians and foundationalists among us, although it’s still pretty trivial.

• Am I correct in supposing that the first definition of Dedekind cuts at real numbers object is missing an openness condition (as given in the later, power object-using definition on the same page)?
• created an entry coefficient and linked it with

as well as with

(the toc is neither meant to already be complete nor to be optimally organized, please expand and polish as you see the need)

• Another new article: sequence space. I await the inevitable report that this term is also used for other things.

• New page: Banach coalgebra.

Hopefully you all know that $l^1$ is a Banach algebra under convolution, but did you know that $l^\infty$ is a Banach coalgebra under nvolution? (Actually, they are both Banach bialgebras!)

• created a little table: chains and cochains - table and included it into the relevant entries (some of which still deserve to be edited quite a bit).

• I have created a table relations - contents and added it as a floatic TOC to the relevant entries.

• I added a few observations under a new section “Results” at bornological set. Bornological sets form a quasitopos. I don’t have a good reference for the theorem of Schanuel.

Related is an observation which hadn’t occurred to me before: the category of sets equipped with a reflexive symmetric relation is a quasitopos. I’d like to return to this sometime in the context of thinking about morphisms of (simple) graphs.

• I have started an entry (∞,n)-category with adjoints, prompted by wanting to record these slides:

• Nick Rozenblyum, Manifolds, Higher Categories and Topological Field Theories, talk Northwestern University (2012) (pdf slides)

If anyone can say more about the result indicated there, I’d be most grateful for a comment.

Also, I seem to hear that at Luminy 2012 there was some extra talk, not appearing on the schedule (maybe by Nick Rozenblyum, but I am not sure) on something related to geometric quantization. If anyone has anything on that, I’d also be most grateful.

• I am starting a table of contents, to be included as a floating TOC for entries related to duality:

duality - contents

But it’s a bit rough for the time being. I haven’t decided yet how to best organize it and I am probably still lacking many items that deserve to be included. To be developed. All input is welcome.

• I started the article Z-infinity-module. Hopefully someone here can say something more interesting about them!

• I'm putting all the big duality theorems from measure theory at Riesz representation theorem. Only a couple are filled in so far, but I'm out of time for today.

• Heya. I haven’t actually made the necessary changes, but the various pages on dependent type theory make the statement that every DTT or MLTT is the internal logic of an LCCC and every LCCC is the categorical semantics of some DTT/MLTT. However, this is extremely confusing (it took me 2 or 3 hours to find a page where it was made completely clear), since it makes explicit use of super-strong extensionality (I think this is called beta-translation), that is to say, it is a theorem about extensional DTTs/MLTTs.

It’s not even totally clear to me that every intensional type theory actually has an (∞,1)-categorical semantics without the consideration of the univalence axiom. I would make this clearer, but I am really out of my depth with type theories, so I’m just alerting you to the fact that this is stated confusingly almost everywhere (the only place where it’s clear is in the page on identity types).

• Disambiguation: dual. Here I listed all of the pages on a kind of dual (but not a kind of duality, which is at duality).

• New page: positive cone, including the extended positive cone of a W*-module.

• Wrote Lambert W function. It was an excuse to record Joyal’s proof of Cayley’s theorem on the number of tree structures one can put on an $n$-element set (which is $n^{n-2}$).