at *complete Boolean algebra* I fixed the missing ${}^{op}$ and then added a pointer to *Set – Properties – Opposite category and Boolean algebras*.

cross-linked with *Euler form* and added these pointers:

Discussion of *Euler forms* (differential form-representatives of Euler classes in de Rham cohomology) as Pfaffians of curvature forms:

{#MathaiQuillen86} Varghese Mathai, Daniel Quillen, below (7.3) of

*Superconnections, Thom classes, and equivariant differential forms*, Topology Volume 25, Issue 1, 1986 (10.1016/0040-9383(86)90007-8){#Wu05} Siye Wu, Section 2.2 of

*Mathai-Quillen Formalism*, pages 390-399 in*Encyclopedia of Mathematical Physics*2006 (arXiv:hep-th/0505003)Hiro Lee Tanaka,

*Pfaffians and the Euler class*, 2014 (pdf){#Nicolaescu18} Liviu Nicolaescu, Section 8.3.2 of

*Lectures on the Geometry of Manifolds*, 2018 (pdf, MO comment)

Mention that geometric homotopy type theory is not well-defined yet.

]]>added to [[Grothendieck construction]] a section Adjoints to the Grothendieck construction

There I talk about the left adjoint to the Grothendieck construction the way it is traditionally written in the literature, and then make a remark on how one can look at this from a slightly different perspective, which then is the perspective that seamlessly leads over to Lurie's realization of the (oo,1)-Grothendieck construction.

There is a CLAIM there which is maybe not entirely obvious, but straightforward to check. I'll provide the proof later.

]]>Todd,

you added to Yoneda lemma the sentence

In brief, the principle is that the identity morphism $id_x: x \to x$ is the universal generalized element of $x$. This simple principle is surprisingly pervasive throughout category theory.

Maybe it would be good to expand on that. One might think that the universal property of a genralized element is that every other one factors through it uniquely. That this is true for the generalized element $id_x$ is a tautological statement that does not need or imply the Yoneda lemma, it seems.

]]>am starting something here, to be expanded…

]]>for completeness, to go with the other items in *coset space structure on n-spheres – table*

for completeness, to go with the other entries in *coset space structure on n-spheres – table*

summary table, to be `!include`

ed into relevant entries, for purposes of cross-linking

I have added pointer to

- Paul de Medeiros, José Figueroa-O’Farrill, Sunil Gadhia, Elena Méndez-Escobar,
*Half-BPS quotients in M-theory: ADE with a twist*, JHEP 0910:038,2009 (arXiv:0909.0163, pdf slides)

to the entries *7-sphere*, *ADE classification*, *Freund-Rubin compactification*.

This article proves the neat result that the finite subgroups $\Gamma$ of $SO(8)$ such that $S^7/\Gamma$ is smooth and spin and has at least four Killing spinors has an ADE classification. The $\Gamma$s are the the “binary” versions of the symmetries of the Platonic solids.

]]>I came to think that the term *geometric type theory* for the type theory internal toi sheaf toposes should exists. Thanks to Bas Spitter for pointing out that Steve Vickers had already had the same idea (now linked to at the above entry).

Also created *geometric homotopy type theory* in this vein, with some evident comments.

added to quantum anomaly

an uncommented link to Liouville cocycle

a paragraph with the basic idea of fermioninc anomalies

the missing reference to Witten’s old article on spin structures and fermioninc anomalies.

The entry is still way, way, stubby. But now a little bit less than a minute ago ;-

]]>I was looking again at this entry, while preparing my category theory notes elsewhere, and I find that this entry is really bad.

With the co-Yoneda lemma in hand (every presheaf is a colimit of representables, and that is dealt with well on its page), the statement of free cocompletion fits as an easy clear Idea into 2 lines, and as a full proof in maybe 10.

The entry should just say that!

Currently the section “technical details” starts out right, but somehow forgets along the way what it means to write a proof in mathematics.

On the other hand, the section “Gentle introduction” seems to be beating about the bush forever. Does this really help newbies?

]]>I have added to the beginning of the category:people entry *Jacob Lurie* a little bit of actual text. Please feel invited to further expand and fine-tune. Right now it reads as follows:

]]>After an early interest in formal logic (see Notices of the AMS vol 43, Number 7) Lurie indicated in his PhD thesis how the moduli stack of elliptic curves together with the collection of elliptic cohomology spectra associated to each elliptic curve is naturally understood as a geometric object in a homotopy theoretic refinement of algebraic geometry that has come to be known as derived algebraic geometry. He then embarked on a monumental work laying out detailed foundations of the subjects necessary for this statement, which is homotopy theory in its modern incarnations as higher category theory, higher geometry in terms of higher topos theory and finally higher algebra in terms of higher operads, all in principle very much along the lines originally developed by Alexander Grothendieck and his school for ordinary algebraic geometry, but now considerably further refined to the general context of homotopy theory. While some developments in these topics had been available before, Lurie’s comprehensive work has arguably led these subjects to an era of reinvigorated activity with a variety of further spin-offs. Among these most notable is maybe the formalization and proof of the cobordism hypothesis, which lays higher monoidal category theoretic foundations for (local, topological) quantum field theory.

I wrote something at meaning explanation, but I didn’t add any links to it yet because I’m hoping to get some feedback from type theorists as to its correctness (or lack thereof).

]]>Inserted two syntactic characterizations of cartesian theories, and references to the Palmgren-Vickers paper.

Steve Vickers

]]>added to *pure type system* in the Idea-section the statement

In other words a

pure type systemis

a system of natural deduction

with dependent types

and with the dependent product type formation rule.

and to the *Related concepts*-Section the paragraph

Adding to a pure type sytstem

rules for introduing inductive types

possibly a type of types hierarchy

makes it a

calculus of inductive constructions.

Finally I added to the References-section a pointer to these slides

]]>Finally made a page for the concept mentioned by Mike in a 2016 n-Café discussion.

I’d be interested in examples that weren’t already relevance monoidal categories (ie, not symmetric).

]]>brief `category:people`

-entry for hyperlinking references at *differential geometry*, *smooth manifold*, *Gauss-Bonnet theorem*, *Euler form* and elsewhere

started Euler class

]]>I decided it would be a good idea to split off realizability topos into a separate entry (it had been tucked away under partial combinatory algebra). I’ve only just begun, mainly to get down the connection with COSHEP. A good (free, online) reference is Menni’s thesis.

]]>Wrote an article Eudoxus real number, a concept due to Schanuel.

]]>Page created, but author did not leave any comments.

Ramkumar Ramachandra

]]>I have started a category:reference page

such as to be able to point to it for reference, e.g. from Kontsevich 15 etc.

]]>