How about this as a basic framework?

- Every mathematical object has a type, which is another mathematical object. We write $x:A$. “Being a type” is a property of mathematical objects.
- There is an operation taking every type $A$ to a type $P A$ that is its type, i.e. $A:P A$.
- The objects of type $P A$ are called subsets of $A$, and there is a specified relation $\in$ between them and objects of type $A$, which satisfies the separation axiom. Moreover, for every $x:A$ we have $x\in A$; the latter is well-typed since $A:P A$.
- There is a monoid structure $(-,-)$ on all mathematical objects, and a monoid structure $\times$ on all sets (i.e. objects whose type is of the form $P A$) that preserves types (i.e. if $A$ and $B$ are types, so is $A\times B$). If $x:A$ and $y:B$, then $(x,y):A\times B$; and if $S:P A$ and $T:P B$ then $S\times T : P(A\times B)$. Note that these are associative, so that $S\times (T\times U) = (S\times T)\times U$ (and is written $S\times T\times U$), and $(x,(y,z)) = ((x,y),z)$ (and is written $(x,y,z)$). The elements of $S\times T$ (for any sets $S,T$, including but not restricted to types) are exactly those of the form $(x,y)$ for a unique $x\in S$ and $y\in T$, and $()$ is the unique element of $\mathbf{1}$ (the unit of $\times)$.
- Mathematical objects are equipped with three partial binary operations $+$, $inl$ and $inr$. The object $S+T$ is defined iff $S$ and $T$ are sets, preserves types, and if $S:P A$ and $T:P B$ then $S+T:P(A+B)$. The object $inl_T(x)$ is defined iff $T$ is a set, and if $x:A$ and $T:P B$ then $inl_T(x):A+B$ and moreover $inl_T(x)=inl_B(x)$. Similarly, $inr_S(y)$ is defined iff $S$ is a set, and if $S:P A$ and $y:B$ then $inr_S(y):A+B$ and $inr_S(y)=inr_A(y)$. For any sets $S:P A$ and $T:P B$, the elements of $S+T$ are exactly those of the form $inl_B(x)$ or $inr_A(y)$ (but not both) for a unique $x\in S$ or $y\in T$. In addition, $+$ has a two-sided unit $\emptyset$. (I suppose we could consider making $+$ associative too.)
- Mathematical objects are equipped with two partial binary operations denoted by $S,T \mapsto PF(S,T)$ (“the set of partial functions”) and application $f,x \mapsto f(x)$. The object $PF(S,T)$ is defined iff $S$ and $T$ are sets, preserves types, and if $S:P A$ and $T:P B$ then $PF(S,T):P(PF(A,B))$. If application $f(x)$ is defined, then $f:PF(A,B)$ and $x:A$ and $f(x):B$ for some types $A,B$. Moreover, for any sets $S:P A$ and $T:P B$, the elements of $PF(S,T)$ are precisely those $f:PF(A,B)$ such that if $f(x)$ is defined, then $x\in S$ and $f(x)\in T$. Partial function comprehension holds: for any property $\phi(x,y)$ relating elements $x:A$ with $y:B$ such that for any $x$ there is at most one $y$ such that $\phi(x,y)$, there exists a unique $f:PF(A,B)$ such that $f(x)$ is defined iff there exists a $y$ such that $\phi(x,y)$ in which case $\phi(x,f(x))$. We write $T^S$ for the subset of $PF(S,T)$ consisting of the total functions.

You get the idea. I haven’t written out quotient sets in this style yet, but you can guess how they would go; they could take as input either an equivalence relation on a set, or a partial equivalence relation on a type (both defined as a particular subset of a cartesian product).

]]>In the nLab article on the universal enveloping algebra, the section describing the Hopf algebra structure originally stated that “the coproduct $\Delta: U L \to U(L \coprod L)\cong U L\otimes UL$ is induced by the diagonal map $L \to L \coprod L$.”

I assume that this is a mistake, and I have since changed the coproduct $\coprod$ to a product $\times$. However, I don’t know a great deal about Hopf algebras, so please correct me if I’ve made a mistake here.

]]>Right, thanks, I am concerned with the op-ed version of 1-mono.

This came from thinking about the definition of formally smooth *stacks*. How do people usually define formally smooth stacks?

A formally smooth scheme $X$ is one for which the map $X \to \Im X$ to its de Rham space “infinitesimal shape modality” is an epimorphism in the 1-topos.

The question is what is the right way to generalize this from schemes to stacks.

I came to think that a key property of a would-be formally smooth stack $X$ is that the 0-section of its cotangent stack is a 1-mono. This turns out to be implied if $X \to \Im X$ is the op-ed version of a 1-mono.

Now i know for some situations of intrest that $X \to \Im X$ is an effective epi. I was hoping that I could add a little bit of something to see that it’s an op-ed 1-mono. But I gather I should instead re-think the whole situation in terms of op-ed 1-monos in the first place.

]]>It looks like Lurie only discusses the projective versions so far (5.4 and 19.2.6 in SAG). Presumably discussion of the affine versions will also be added at some point, but who knows. Have you seen his new paper Elliptic Cohomology I, though? That might have what you’re looking for, see especially Example 3.5.4.

]]>There should be $Spec$ continuing on the right? So also at spectral super-scheme.

]]>Speaking categorically, the corresponding statement for the external-hom is essentially the definition of 1-monomorphism, and the internal part internalizes in the same way this sort of stuff usually does: $Hom(Y,[X,f]) = Hom(Y\times X, f)$.

For the second part, I don’t think an effective epi should be called a 1-epi; a 1-epi should be a map that is 1-mono in the opposite category. As you know, unlike in the 1-categorical case, effective epis are not in general 1-epi in this sense, even for the external-hom, and I don’t know any natural conditions ensuring that they are.

]]>Internally, it *is* technically contrary, in the sense that if you have both of them you can construct an inhabitant of $\emptyset$. (This is the only possible internal meaning of “contrary”.) Externally, you are right that what this means is that only the trivial model satifies both.

There’s an unbound $n$ on the left, but it would appear not in the expressions on the right.

]]>Is UIP technically contrary to the univalence axiom, or does this “just” only leave trivial models?

]]>Somewhere else I wrote down an elaboration about constructively provable classical equivalents to LEM*. When I saw Urs made a page for the double negation I thought about writing down those for the nLab in a parallel fashion. Since the abstraction from $\bot$ to some generic proposition makes the case for LEM more clear, I was thinking if there’ a name for the above.

*An inhabitant of

$\left((A\to B)\times((A\to B)\to C)\right)\to C$

is

$eat=\lambda x.(\pi_2x)(\pi_1 x)$

which acts like e.g.

$eat\,(\,x\mapsto x^2,\, f\mapsto \int_1^3f(x)\,dx\,) = \int_1^3 x^2\,dx = \frac{26}{3}$

A less general type expression would be

$\left((A\to \bot)\times((A\to \bot)\to \bot)\right)\to \bot$

which in logic reads

$\neg\left(\neg A\wedge \neg \neg A\right)$

Classically: Using De Morgan’s law we get

$\neg\neg A \vee \neg \neg \neg A$

and with double negation we end up at LEM

$A\vee \neg A$

Made me think of what those laws used are when we don’t look at $\bot$ but general propositions.

]]>For the first part, this follows because the fiber of post-composition with $f : A \to B$ at some $h : X \to B$, $fib_{f\circ}(h)$, is equivalent to the Pi-type $\prod_{x : X} fib_f (h x)$.

]]>I have added a section here discussing how one may see, via $N = 2$ super Yang-Mills theory, why and how the finite subgroups of $SU(2)$ corresponding to some Dynking diagram are related to the compact simpl Lie groups corresponding to the same Dynkin diagram.

]]>Given an $\infty$-topos, an object $X$, and a $f$ 1-monomorphism (i.e. (-1)-truncated) is the internal hom $[X,f]$ again a 1-mono?

And dually for $f$ 1-epimorphism (i.e. effective epimorphism) do we have some extra conditions such that $[f,X]$ is 1-mono?

]]>I changed the link to your Stutz paper to `https://arxiv.org/abs/1703.03240`

. In the future please link to the `abs`

page not the `pdf`

one.

I also cleaned up the page a little, making inline references link to the list at the bottom.

[ I don’t know how to enclose such links in square brackets ]

]]>Nikolaj, personally I don’t know a name for this, other than saying that it’s the “$\Box$-translation of $\neg\neg P \Rightarrow P$”, where the $\Box$-translation for any modal operator $\Box$ is like the double negation translation, only putting $\Box$’s instead of $\neg\neg$’s all over the place. Here, the modal operator $\Box$ is given by $\Box\varphi \equiv (\varphi \vee Q)$.

Do you have a specific situation in mind where you’d want to have a name for this formula?

]]>``Of particular importance are convex spaces parametrized by the interval P=[0,1] or

the Boolean algebra P={0,1}.'' I find very odd. The Boolean algebra 2={0,1}, and more generally, ``discrete convex spaces'' I believe you are thinking about can be viewed within the context of parameterization over the unit interval. I am basing my ideas on the work of

J.Isbell,M. Klum, and S.Schanuel, Affine part of algebraic theories - which shows that Cvx is just the affine part of the

theory of K-modules, as detailed in Mengs thesis (which is referenced). ]]>

Presumably we’re in linear HoTT territory, the !-modality instantiating the bosonic Fock space construction. I wonder if there is a possible modal treatment of the fermionic Fock space.

]]>Thanks for the pointer. I have included this and some discussion at *spectral symmetric algebra*.

I think it makes sense to call any theorem of the sort “fundamental $n$-groupoid functor preserves some colimits” a “higher van Kampen theorem”.

]]>Moerdijk-Wraith might be what I was thinking of.

]]>Ah, yes! (In case anyone else has trouble finding it on the page, the mention of ∞-toposes just links to here. And we might hope to modify that argument to work in the elementary case too, by removing accessibility but checking other conditions as well. We should have pages about these.

]]>The spectral affine line over the sphere spectrum is denoted $\mathbf{I}$ in Adeel’s Brave new motivic homotopy theory I (3.2.1).

]]>A notable feature of the HHSvKTs with which I have been involved, and indeed in the traditional vKT, is the key notion of connected and its use in the statement and proof of the theorems, But this terms does not occur in some of the other statements of results labelled as in this class of theorems.

On this basis alone, the theorems would seem to be of very different types. ]]>

Since gluing is constructed by the topos+of+coalgebras+over+a+comonad, I guess the generalization to higher toposes stated there would give a variant of gluing.

]]>