# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• created computational trinitarianism, combining a pointer to an exposition by Bon Harper (thanks to David Corfield) with my table logic/category-theory/type-theory.

• Following discussion in some other threads, I thought one should make it explicit and so I created an entry

Currently this contains some (hopefully) evident remarks of what “dependent linear type theory” reasonably should be at least, namely a hyperdoctrine with values in linear type theories.

The entry keeps saying “should”. I’d ask readers to please either point to previous proposals for what “linear dependent type theory” is/should be, or criticise or else further expand/refine what hopefully are the obvious definitions.

This is hopefully uncontroversial and should be regarded an obvious triviality. But it seems it might be one of those hidden trivialities which deserve to be highlighted a bit more. I am getting the impression that there is a big story hiding here.

Thanks for whatever input you might have.

• I had given it an $n$Lab page already a while back, so that I could stably link to it without it being already there:

Now it’s even “there” in the sense of being incarnated as a pdf.

• Updating reference to cubical type theory. This page need more work.

• brief category:people-entry for hyperlinking references

• a bare list of references, to be !includ-ed into the list of references of relevant entries, such as at quantum computing and quantum programming, for ease of updating and syncing

• a stub

• Aleks Kissinger has contacted me about his aims to start a collection of nLab entries on quantum information from the point of view of the Bob Coecke school.

Being very much delighted about this offer, I created a template entry quantum information for his convenience.

• a stub, for the moment just to make links work

• a stub, to make links work

(This used to be a stub “quantum circuit” which I just quasi-duplicated at a more extensive entry quantum circuit diagram. But since quantum gate was already redirecting here – which is how I discovered/remembered that this entry exists – no harm is done by making that it’s new title.)

• starting something

• Add a reference for string diagrams in closed monoidal categories

Anonymous

• separate page created

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

• Decidable language =/= decidable type checking.

Arvid Marx

• It should be clarified that type checking is decidable, not e.g Type inhabitation or some other property.

Anonymous

• changed page name to make it fit more systematic naming pattern

• Started something.

• Page created, but author did not leave any comments.

Anonymous

• Page created, but author did not leave any comments.

• I started an article about Martin-Löf dependent type theory. I hope there aren't any major mistakes!

One minor point: I overloaded $\mathrm{cases}$ by using it for both finite sum types and dependent sum types. Can anyone think of a better name for the operation for finite sum types?

• I created a stub certified programming.

That’s motivated from me having expanded the Idea-section at type theory. I enjoyed writing the words “is used in industry”. There are not many $n$Lab pages where I can write these words.

I am saying this only half-jokingly. Somehow there is something deep going on.

Anyway, in (the maybe unlikely) case that somebody reading this here has lots of information about the use and relevance of certified programming in industry, I’d enjoy seeing more information added to that entry.

• brief category:people-entry for hyperlinking references at QWIRE and related entries

• brief category:people-entry for hyperlinking references at QWIRE and related entries

• brief category:people-entry for hyperlinking references at QWIRE and related entries

• starting something

• Page created, but author did not leave any comments.

• am starting some minimum here. Have been trying to read up on this topic. This will likely become huge towards beginning of next year

• Had a look at some literature and found of course that it’s vast, so have added some findings.

• I am trying to collect citable/authorative references that amplify the analog of the mass gap problem in particle phenomenology, where it tramslates into the open problem of computing hadron masses and spins from first principles (due to the open problem of showing existence of hadrons in the first place!).

This is all well and widely known, but there is no culture as in mathematics of succinctly highlighting open problems such that one could refer to them easily.

I have now created a section References – Phenomenology to eventually collect references that come at least close to making this nicely explicit. (Also checked with the PF community here)

• I have made explicit the example of involutive Hopf algebras, and how most of the other examples previously listed here are special cases of this one. Also expanded a little and organized it all into a new Examples-subsection (here)

• changed “involution” to “anti-involution”

• Switch commuting reasoning to use an implication for clarity.

• Page created, but author did not leave any comments.

• An old query at twisting cochain which was reaction to somebody putting that the motivation is the homological perturbation lemma:

It is equally true that it is related to 20 more areas like that one (which is not the central). Brown’s paper on twisting cochains, is much earlier than homological perturbation theory. basic idea was to give algebraic models for fibrations. Nowedays you have these things in deformation theory, A-infty, gluing of complexes on varieties, Grothendieck duality on complex manifolds (Toledo-Tong), rational homotopy theory etc. One should either give a fairly balanced view to all applications or not list anything, otherwise it is not fair. This should be done together with massive expansion of Maurer-Cartan equation what is almost the same topic. The same with literature: Smirnov’s book on simplicial and operadic methods in algebraic topology is the most wide reference for twisting cochains and related issues in algebraic topology setup; Keller wrote much and well about this and Lefèvre-Hasegawa thesis (pdf) is very good, and the first reference is E. Brown’s paper from 1959. For applications in deformation theory there are many references, pretty good one from dg point of view and using 2-categorical picture of def functors is a trilogy of Efimov, Lunts and orlov on the arXiv. Few days ago Sharygin wrote a long article on twisting cochains on the arXiv, with more specific purposes in index theory. Interesting is the application of Baranovsky on constructing universal enveloping of L infty algebra. – Zoran

Urs: concerning the “either give a fairly balanced view to all applications or not list anything”, I can see where you are coming from, Zoran, but I would still prefer here to have a little bit of material than to have none. The $n$Lb is imperfect almost everywhere, we’ll have to improve it incrementally as we find time, leisure and energy. But it’s good that you point out further aspects in a query box, so that we remember to fill them in later.

Zoran Skoda My experience is that correcting a rambling and unbalanced entries takes more time than writing a new one at a stage when you really work on it. Plus all the communication explaining to others who made original entry which is hastily written. When it becomes very random and biased I stopped enjoying it at all to work on it.

Ronnie Brown It may not possible for one person to give a “balanced entry” and is certainly not possible for me in this area. On the other hand, this may be endemic to the description of an area of maths for students and research workers.

An advantage of the Homological Perturbation Lemma (HPL) is that it is an explicit formula, and this has been exploited by various writers, especially Gugenheim, Larry Lambe and collaborators, Huebschmann, and others, for symbolic computations in homological algebra. It is good of course to have the wide breadth of applications of twisting cochains explained.

For me, an insight of the HPL was the explicit use of the homotopies in a deformation retract situation to lead to new results. This has been developed to calculate resolutions of groups, where one is constructing inductively a universal cover of a $K(G,1)$ with its contracting homotopy.

So let us continue to have various individually “unbalanced” points of view explained in this wiki, to let the readers be informed, and decide.

Toby: Knowing basically nothing about this, I prefer to see various people explain their own perspectives. Even if they don't try to take the work to integrate them.