# Start a new discussion

## 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.

• started bracket type, just for completeness, but don’t really have time for it

• Correct the characterization of nerves of groupoids.

• The way of writing the adjunction in locale in Prop 4. and Corollary 1. is a bit misleading: When you explicit the adjunction symbol you normally write the domain of the right adjoint on the left and its codomain on the right (e.g., as in reflective subcategory). I didn't do the change myself as I might be missing a convention here.
• This page should be merged with “essentially algebraic theory”, as the two notions are equivalent. Since the “cartesian theory” has little in it, I’m attempting to redirect to “essentially algebraic theory”. There is also relevant stuff at “cartesian logic”, though I’m not sure how best to organize that and link to it.

Steve Vickers

• Page created, but author did not leave any comments.

• added pointer to conference this month: here

• stub for confinement, but nothing much there yet. Just wanted to record the last references there somewhere.

• Added comment regarding propositional logic as that with no sorts.

Steve Vickers

• 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.

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

Steve Vickers

• added some actual text to the category:people entry Roger Penrose

• created this in part to help answer query from Beppe here on the forum. It is very stubby and needs more work! (I copied and pasted from a preprint so it is not optimised for the Lab.)

• It would be nice if the entry were a little more explicit about the slicing theorem

$PSh_\infty(\mathcal{C}_{/p}) \stackrel{\simeq}{\to} PSh_\infty(\mathcal{C})_{/y p} \,.$

(here)

In the special case that the small $\infty$-category $\mathcal{C}$ happens to be a small $\infty$-groupoid and that $p$ is constant on an object $X \in \mathcal{C}$, it ought to be true that an explicit form of this equivalence is given in semi-HoTT notation by

$\left( (c \overset{\gamma}{\to}X) \;\mapsto\; \mathcal{F}(\gamma) \right) \;\mapsto\; \left( c \;\mapsto\; \array{ \underset{c \underset{\gamma}{\to}X}{\sum} \mathcal{F}(\gamma) \\ \downarrow \\ \underset{c \underset{\gamma}{\to}X}{\sum} \ast } \right) \,.$

This must be an easy theorem in HoTT?

• Created page, mainly to record my understanding of the issue involving strong normalization, or lack thereof, for explicit substitutions.

• I have added links to a new page on Grace Orzech’s notion of Category of Interest, and a new reference to Phil Higgins paper on Omega groups.

• am starting something. Nothing to be seen yet, but need to save for the moment