Regarding #79 and its mention of ’synthetic stable homotopy theory’, presumably the idea here is to prove theorems in linear HoTT which will then be true in every tangent $\infty$-topos. Can we think of some nice low-hanging fruit as targets for this synthetic stable homotopy theory?

Say might we expect some kind of general linear representation theory?

]]>Indexed monoidal categories as intended semantics for dependent linear types is discussed in the section “Semantics”.

]]>added pointer also to

- Conor McBride,
*I Got Plenty o’ Nuttin’*, in:*A List of Successes That Can Change the World*, Lecture Notes in Computer Science**9600**, Springer (2016) [doi:10.1007/978-3-319-30936-1_12]

and fixed up a bunch of other references that were added by others in the past, restoring chronological order

]]>added publication data for:

- Neelakantan Krishnaswami, Pierre Pradic, Nick Benton,
*Integrating Dependent and Linear Types*, ACM SIGPLAN Notices**50**1 (2015) 17–30 [pdf,doi:10.1145/2775051.2676969]

Just received a reply from `wesscholar@wesleyan.edu`

: the link doi:10.14418/wes01.3.139 has been fixed now.

I have emailed them again (`wesscholar@wesleyan.edu`

). Let’s hope this can still be fixed.

Thanks for pointing this out. A related glitch happened before, some months back, when the DOI would be a dead link. Back then I had emailed some web-host who responded by asking for patience until some server migration was completed, and indeed the problem was fixed a few days later. But now it looks like that previous glitch may have caused the same DOI to be re-used.

]]>Re #84: doi now redirects to some chemistry thesis from just this past May. Seems, at least according to the uni webpage, both have the same doi.

]]>added pointer to:

- Mitchell Riley,
*A Bunched Homotopy Type Theory for Synthetic Stable Homotopy Theory*, PhD Thesis (2022) [ir:3269]

That seems to have an obvious answer: Yes, worth exploring. :-)

First thing we are aiming at (as laid out in my PlanQC talk today) is implementing the dependent type family of $\mathfrak{su}(2)_k$-conformal blocks into Agda. The formula laid out here gives this as a plain dependent type. But of course it is (or ought to be) a linear dependent type. Hence an application of $\Sigma^\infty \Omega^\infty$ must be “undone”. This will be a consequence of understanding the Eilenberg-MacLane type entering the formula as the image under $\Sigma^\infty \Omega^\infty$ of the EM-spectrum type.

Once the resulting (linear) dependent type of conformal blocks is coded into Agda, we have a first (not so-)rudimentary “anyon-hardware-aware topological quantum simulator”. I’ll keep you all posted about progress.

]]>One question at least, for linear HoTT, is it worth exploring the idea of $\Sigma^\infty \Omega^\infty$ as exponential, $!$, by looking at that synthetic treatment of the component maps in arXiv:2102.04099?

$\Omega^{\infty} E := \natural (\mathbb{S} \to E)$ and $\Sigma^{\infty} E := E \wedge \mathbb{S}$, then $! E = \Sigma^\infty \Omega^\infty E = \mathbb{S} \wedge \natural (\mathbb{S} \to E).$

One line of thought here, given the adjunction of pointed maps they mention under definition 3.17, $- \wedge A \vdash A \to_{\ast} -$, the composite looks like a variation on the store comonad, $D X = W \times [W, X]$, (whose coalgebras are lenses).

]]>Yes, most CQTS researchers have arrived and settled in (only Marwa and Tatiana yet to arrive in person). Yesterday and today we had the initial researcher’s meeting, with everyone presenting their work. (10 min ago I just wrapped up the meeting here, after somewhat of a marathon session.)

I see that you are eager to get feedback on your remarks, but maybe help us a bit: Could you phrase a concrete question or proposal? I am still a little uncertain as to what kind of feedback to give.

]]>Mitchell’s at your Center now? I wonder what he thinks of that series of semi-thoughts I had on Twitter and at the nForum. Thought I was glimpsing something.

]]>expanded out more details:

Mitchell Riley,

*Linear Homotopy Type Theory*, talk at: HoTTEST Event for Junior Researchers 2022 (Jan 2022) [slides: pdf, video: YT]**Abstract.**Some ∞-toposes support constructions that are inherently ’linear’, such as the external smash product of parameterised spectra. These cannot be added axiomatically to ordinary HoTT, because there is no way to enforce this linearity: there are no restrictions on variable uses. This talk describes an extension of HoTT with linear tensor and hom type formers, as a kind of ’binary modality’ and its right adjoint. Trying to stay compatible with existing results in HoTT naturally leads us to a novel kind of bunched dependent type theory. Our type theory is intended to be as human-usable as possible, with an eye towards synthetic stable homotopy theory.

and linked to it from the beginning of the Idea-section where “linear homotopy type theory” is first mentioned.

]]>added pointer to:

- Mitchell Riley,
*Linear Homotopy Type Theory*, HoTTEST talk (Jan 2022) [pdf]

Provided links to slides at Bounded Linear Logic Workshop.

]]>added pointer to the thesis

- Martin Lundfall,
*Models of linear dependent type theory*, 2017 (pdf)

(which became the preprint Lundfall 18, arXiv:1806.09593 – both, apparently, unpublished)

]]>added these two pointer:

Matthijs Vákár,

*A Categorical Semantics for Linear Logical Frameworks*, In: A. Pitts (ed.),*Foundations of Software Science and Computation Structures*FoSSaCS 2015. Lecture Notes in Computer Science, vol 9034. Springer 2015 (arXiv:1501.05016, doi:10.1007/978-3-662-46678-0_7)Matthijs Vákár, Section 3 of:

*In Search of Effectful Dependent Types*(arXiv:1706.07997, uuid:e91e19b3-7e10-4fda-9433-f23b469e4049)

I seem to be seeing polynomial functors wherever I look these days.

]]>And one more:

- Mike Shulman,
*A type theory for fibred functors and polynomials*. Unfinished note, 2018. pdf

Added some references for other kinds of DLTT.

]]>Added arXiv number and comlete publication data to

- {#FKS20} Peng Fu, Kohei Kishida, Peter Selinger,
*Linear Dependent Type Theory for Quantum Programming Languages*, LICS ’20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer ScienceJuly 2020 Pages 440–453 (arXiv:2004.13472, doi:10.1145/3373718.3394765, pdf, video)

added pointer to:

- Peng Fu, Kohei Kishida, Neil Ross, Peter Selinger,
*A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper*, in I. Lanese, M. Rawski (eds.)*Reversible Computation*RC 2020. Lecture Notes in Computer Science, vol 12227 (arXiv:2005.08396, doi:10.1007/978-3-030-52482-1_9)

and added cross-links with the new entry *quantum programming language*

Added reference

]]>