Am starting a write-up (here) of how (programming languages for) quantum circuits “with classical control and/by measurement” have a rather natural and elegant formulation within the linear homotopy type theory of Riley 2022.

Aspects of this have a resemblance to some constructions considered in/with “Quipper”, but maybe it helps clarify some issues there, such as that of “dynamic lifting”.

The entry is currently written without TOC and without Idea-section etc, but rather as a single top-level section that could be `!include`

-ed into relevant entries (such as at *quantum circuit* and at *dependent linear type theory*). But for the moment I haven’t included it anywhere yet, and maybe I’ll eventually change my mind about it.

When pointing somebody to it, I noticed that the entry *n-category* is in a rather sad state and in particular it used to start out in a rather unhelpful fashion. I have now tried to briefly fix at least the latter problem by expanding and editing the first two sentences a bit. Notably I made sure that a pointer to *(∞,n)-category* appears early on, for that is a place with more robust information, currently.

creating a stub entry in order to give a proper home to the reference

- Simona Paoli,
*Simplicial Methods for Higher Categories – Segal-type Models of Weak $n$-Categories*, Springer (2019) [doi:10.1007/978-3-030-05674-2, toc pdf]

(which was previously incorrectly listed at *n-fold complete Segal space*)

Somebody over lunch at the conference here said that the $n$-Lab somewhere leaves out a condition in the definition of n-fold complete Segal spaces, namely “it’s not just completeness, there is also a condition that many spaces are degenerate”.

We were offline and couldn’t quite determine which entry was meant. Now I am online but alone, and I checked at *n-fold complete Segal space*, which doesn’t really give any definition at all, but points to *(infinity,n)-category* and *n-category object in an (infinity,1)-category*. I *think* (am pretty sure) that there the correct definition is given, but I don’t really have the leisure to check in detail right now.

Instead, I suspect that everything on the nLab is correct but there is just a subtlety that maybe deserves to highligted more, namely for $n$-fold Segal spaces the completenss condition automatically involves more and more degeneracy condition due to the way that $\infty$-groupoids are regarded as degenerate cases of $(n-1)$-fold complete Segal spaces.

To hint at that (don’t have time for more right now), I have now added to *n-fold complete Segal space* the following paragraph:

]]>In analogy of how it works for complete Segal spaces, the completness condition on an $n$-fold complete Segal space demands that the $(n-1)$-fold complete Segal space in degree zero is (under suitable identifications) the infinity-groupoid which is the core of the (infinity,n)-category which is being presented. Since the embedding of $\infty$-groupoids into ($n-1$)-fold complete Segal spaces is by adding lots of degeneracies, this means that the completeness condition on an $n$-fold complete Segal space involves lots of degeneracy conditions in degree 0.

Page created, but author did not leave any comments.

Anonymous

]]>Just to record some references, prodded by discussion in another thread (here).

From people’s question around the fora (e.g. Physics.SE:q/15339) I gather that the principle is referenced prominently in popular physics books by “Penrose, Hawking, Greene, etc.”, but I haven’t tracked those paragraphs down yet.

]]>Brief profile page for Bruno Bentzen, whose paper is mentioned in https://ncatlab.org/nlab/show/cubical+type+theory

Anonymous

]]>I have given *necessity* and *possibility* (which used to redirect to *S4-modal logc*) an entry of their own.

The entry presently

first recalls the usual axioms;

then complains that these are arguably necessary but not sufficient to characterize the idea of necessity/possibility;

and then points out that if one passes from propositional logic to first-order logic (hyperdoctrines) and/or to dependent type theory, then there is a way to axiomatize modalities that actually have the correct interpretation, namely by forming the reflection (co)monads of $\exists$ and $\forall$, respectively.

You may possibly complain, but not necessarily. Give it a thought. I was upset about the state of affairs of the insufficient axiomatics considered in modal logic for a long time, and this is my attempt to make my peace with it.

]]>brief `category:people`

-entry for hyperlinking references

edited dualizable object a little, added a brief paragraph on dualizable objects in symmetric monoidal $(\infty,n)$-categories

]]>added to identity type a mentioning of the alternative definition in terms of inductive types (paths).

]]>Notation correction for A=C_0(Y) to A=C_0(X).

Anonymous

]]>somebody on the nForum thread on the identity type article brought up objective type theory so I thought I would start an article on that subject

Anonymous

]]>I gave regular cardinal its own page.

Because I am envisioning readers who know the basic concept of a cardinal, but might forget what “regular” means when they learn, say, about locally representable category. Formerly the Lab would just have pointed them to a long entry cardinal on cardinals in general, where the one-line definition they would be looking for was hidden somewhere. Now instead the link goes to a page where the definition is the first sentence.

Looks better to me, but let me know what you think.

]]>A little entry, to make links work.

]]>A little entry, to make links work.

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

Anonymous

]]>I was involved in some discussion about where the word “intensional” as in “intensional equality” comes from and how it really differs from “intenTional” and what the point is of having such a trap of terms.

Somebody dug out Martin-Löf’s lecture notes “Intuitionistic type theory” from 1980 to check. Having it in front of me and so before I forget, I have now briefly made a note on some aspects at *equality* in the section *Different kinds of equalits* (below the first paragraph which was there before I arrived.)

Anyway, on p. 31 Martin-Löf has

intensional (sameness of meaning)

I have to say that the difference between “sameness of meaning” and “sameness of intenTion”, if that really is the difference one wants to make, is at best subtle.

]]>Added reference

- Benno van den Berg, Martijn den Besten,
*Quadratic type checking for objective type theory*(arXiv:2102.00905)

Anonymous

]]>Adding reference

- Benno van den Berg, Martijn den Besten,
*Quadratic type checking for objective type theory*(arXiv:2102.00905)

Anonymous

]]>copied from HoTT wiki

Anonymous

]]>brief `category:people`

-entry for hyperlinking references

stub for *quantum computation*

starting something, just some references so far

]]>The following sentence was at inaccessible cardinal:

A weakly inaccessible cardinal may be strengthened to produce a (generally larger) strongly inaccessible cardinal.

I have removed it after complaints by a set theorist, and in light of the below discussion box, which I have copied here and removed.

Mike: What does that last sentence mean? It seems obviously false to me in the absence of CH.

Toby: It means that if a weakly inaccessible cardinal exists, then a strongly inaccessible cardinal exists, but I couldn't find the formula for it. Something like $\beth_\kappa$ is strongly inaccessible if $\kappa$ is weakly inaccessible (note that $\aleph_\kappa = \kappa$ then), but I couldn't verify that (or check how it holds up in the absence of choice).Mike: I don’t believe that. Suppose that the smallest weakly inaccessible is not strongly inaccessible, and let $\kappa$ be the smallest strongly inaccessible. Then $V_\kappa$ is a model of set theory in which there are weakly inaccessibles but not strong ones. I’m almost certain there is no reason for the smallest weakly inaccessible to be strongly inaccessible.

JCMcKeown: Surely $\beth_\kappa$ has cofinality at most $\kappa$, so it can’t be regular. Maybe the strengthening involves some forcing or other change of universe? E.g., you can forcibly shift $2^\lambda = \lambda^+$ for $\lambda \lt \kappa$, and then by weak inaccessibility, etc… I

think. Don’t trust me. —- (some days later) More than that: since the ordinals are well ordered, if there is any strongly inaccessible cardinalgreaterthan $\kappa$, then there is aleastone, say $\theta$. Then $V_\theta$ is a universe with a weakly inaccessible cardinal and no greater strongly inaccessible cardinal. Ih! Mike said that already… So whatever construction will have to work the other way around: if there is a weakly inaccessible cardinal that isn’t strongly inaccessible, and if furthermore a weakly inaccessible cardinal implies a strongly inaccessible cardinal, then the strongly inaccessible cardinal implied must be less than $\kappa$. And that sounds really weird.

I was also supplied with a AC-free proof that weakly inaccessibles are $\aleph_{(-)}$-fixed points:

First, a quick induction shows that $\alpha\leq\omega_\alpha$ is always true. If $\kappa$ is a limit cardinal, then the set of cardinals below $\kappa$ is unbounded; but since it’s also regular there are $\kappa$ of them. So $\omega_\kappa\leq\kappa\leq\omega_\kappa$, and equality ensues.

I can edit this into the page if desired.

]]>