Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 21 of 21
Alizter, that seems to be the wrong reference to me. The idea of opetopes that Eric Finster is working with orginates in “Higher-Dimensional Algebra III: n-Categories and the Algebra of Opetopes” (arXiv:q-alg/9702014).
Slide 4
simplicial types are definable in MLTT with coinduction
Any developments to report at coinductive types?
Okay, I have added before that the line
The idea of opetopic sets (nlab) that Finster 18 is inspired by goes back to…
Alizter,
since you do seem to care about making this material available, please allow me to offer advice.
(Last time I tried to give you advice on how to edit wiki entries it didn’t seem to be well received. But please consider it, it is meant in good spirit.)
The material you have in the entry, besides the lead-in sentences which i added, seems to have no beginning and no end. I am comparatively well versed in the matter that I can second guess what I am seeing facets of, but for many readers this may not be the case.
There must be some punchline here that you can articulate after the subsection (but is it really worth a subsection?) on “Leaves and Nodes”. It can’t be that this is the end of the story.
@Urs Your advice is always welcome. I am currently reading the nlab style, I want to structure this article a bit better before I start writing more. The sections thing is simply a temporary measure.
My current goals:
I may have gone a bit overboard with the bracketing, but there isn’t really any good way to write codey looking maths on the nlab without resorting to the code environment. Hopefully it is readable. I noticed a typo in Eric’s slide for example where is defined there is talk of I am assuming this means .
I want to work on adding some examples now. As Mike pointed out in another thread this definition of tree is kind of like abstract syntax trees where the sets are untruncated types instead of finite sets. It may be worth giving a few pictures like Eric has done.
The notion of a frame is more tricky to explain correctly so I will try to cook up some diagrams. They are called frames because if we take the Poincare dual (as Eric put it), a frame is literally an equivalent boundary between two poincare duals of the trees. (See slide 62)
@atmacen Eric is making steady progress in his GitHub repo. He says when its all working there will be a paper following.
As far as I can tell, algebras are still a work in progress.
I originally started following in coq however there are a few ideas I have found difficult to understand. When Eric manages to polish these ideas they ought to become clearer.
What Eric originally proposed in the HoTTEST seminar is very much a (very promising) work in progress, and so for questions like autophagy I would say it is too early to tell.
1 to 21 of 21