added pointer to:

- Mitchell Riley,
*A Bunched Homotopy Type Theory for Synthetic Stable Homotopy Theory*, PhD Thesis (2022) [doi:10.14418/wes01.3.139]

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

]]>Yes, that sentence seems like it should probably be moved to the “Semantics” section.

]]>After the “great split” where much of this page was sent over to indexed monoidal (infinity,1)-category, the links in

What should be the categorical semantics of dependent linear type theory was discussed in (Shulman 08, Ponto-Shulman 12, Shulman 12, Schreiber 14)

no longer work.

A simple fix is possible, but without wishing to provoke the tensions which tend to arise in these parts from differences of opinion on the necessity for syntax when one speaks of a type theory, is the page due a make-over? Why was that quoted sentence in the section ’Syntax’ in any case?

Alternatively we wait for the roll out of the LSR program when all modal dependent type theories will be given their proper setting.

]]>I added this recent reference

- Martin Lundfall,
*A diagram model of linear dependent type theory*, (arXiv:1806.09593)

I wish I had time to read Vákár’s thesis carefully. It looks like he may be solving the problem in the non-homotopy case, specifying a syntax and a semantics and proving that they match up (p81):

The structure we obtain is that of a strict indexed symmetric monoidal category with comprehension

We also get a mention (p71):

Although in the last while some suggestions have been made on the nLab and nForum of possible connections between the syntactic and semantic work, no account of the correspondence was published.

(-:

]]>Thanks for the alert. I had not seen that yet.

]]>Matthijs Vákár’s thesis is out, so I’ve added that to his page. I don’t know whether its separate strands supersede individual publications, such as the one in #48.

]]>Have added two new references to *dependent linear type theory*:

Matthijs Vákár has new talk notes [2] expanding on his article [3] and Neelakantan Krishnaswami with Pierre Pradic and Nick Benton have an article in preparation [4].

[2] http://users.ox.ac.uk/~magd3996/research/10-11-2014-Oxford-Linear%20dependent%20types.pdf

[3] http://arxiv.org/abs/1405.0033

[4] http://www.cs.bham.ac.uk/~krishnan/dlnl-paper.pdf

]]>Have edited a bit more.

I’ll have to leave it the way it is for the moment, have to rush off now. I am going to use part of this as a script for a talk to the type theory group at Paris-Diderot today, around Paul-André Melliès. My goal is to

first convince the audience that six-functor Yoga in Wirthmüller style is precisely what ought to be regarded as the semantics for dependent linear (homotopy-)type theory (i.e. any proposed syntax ought to have that as its semantics),

then to indicate that in such contexts one may elegantly axiomatize “secondary integral transforms”,

point out that these capture/generalize the exponential modality construction,

highlight that it is manifestly a path-integral-like construction

and finally to indicate that in the model of parameterized modules this gives matrix calculus,

and to claim that in the model of parameterized spectra it gives pull-push in bivariant tiwsted generalized cohomology.

We’ll see how it works.

(I’ll duly highlight Mike’s many contributions to this. )

]]>Have edited a good bit more at *dependent linear type theory*. Will continue tomorrow.

The main new addition so far is maybe that I added the definition of *fundamental classes* and of *secondary integral transforms* in terms of dependent linear type theory. Added also the example which shows (or states at least) that for parameterized modules this reproduces matrix calculus.

Maybe I’ll further expand the included table *twisted generalized cohomology in linear homotopy type theory – table* now, but then I need to quit for today.