Thanks! I didn’t know about the weaker notion of “union allegory.”

]]>This reminds me that there are still some loose ends in the alternative account of power allegories (“original research”). I should get back to that.

]]>I think you’re right. I’ve fixed it, mentioning also the weaker notion under the name “union allegory” (which is used in the Elephant).

]]>Hopefully the experts here can help a newbie trying to understand allegories. The current definition of distributive allegory says:

A distributive allegory is an allegory whose hom-posets have finite joins that are preserved by composition. Thus a distributive allegory is locally a lattice.

Based on Freyd-Scedrov I wonder whether it should say something like:

A distributive allegory is an allegory whose hom-posets have finite joins that are preserved by composition and that satisfy the distributivity law. Thus a distributive allegory is locally a distributive lattice.

Is this a mistake?

]]>If we consider the enveloping as the quotient of the tensor algebra, recall that the tensor algebra is the infinite direct sum of tensor powers. Then $(V\coprod W)^{\otimes n}\cong \coprod_{m=0}^n \left(V^{\otimes m}\otimes W^{\otimes (n-m)}\right)$ in the classical case.

$\coprod_n (V\coprod W)^{\otimes n} \cong \coprod_n V^{\otimes n}\otimes \coprod_m W^{\otimes m}$ ]]>In vector spaces finite sums and finite products are the same. Still, I think that viewing it as a direct sum is better here.

]]>FWIW, this wasn’t intended to be a rigorous presentation of any formal system, just an informal description of how such a system might look.

]]>Looks nice, but I can’t make any mathematically informed comments/criticism.

]]>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). ]]>