# 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.

• CommentRowNumber1.
• CommentAuthorAli Caglayan
• CommentTimeDec 6th 2018

Page created, but author did not leave any comments.

• CommentRowNumber2.
• CommentAuthorUrs
• CommentTimeDec 7th 2018

• CommentRowNumber3.
• CommentAuthorAli Caglayan
• CommentTimeDec 7th 2018

I have written $f\, a\,b$ as $f(a,b)$ like in the HoTT book for readability

• CommentRowNumber4.
• CommentAuthorAli Caglayan
• CommentTimeDec 7th 2018

added Baez and Dolan reference from video

• CommentRowNumber5.
• CommentAuthorUrs
• CommentTimeDec 7th 2018

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).

• CommentRowNumber6.
• CommentAuthorDavid_Corfield
• CommentTimeDec 7th 2018

Slide 4

simplicial types are definable in MLTT with coinduction

Any developments to report at coinductive types?

• CommentRowNumber7.
• CommentAuthorUrs
• CommentTimeDec 7th 2018
• (edited Dec 7th 2018)

added pointer to the slides pdf

• CommentRowNumber8.
• CommentAuthorAli Caglayan
• CommentTimeDec 7th 2018

Thanks Urs for point time to the correct paper. Fixed link now.

• CommentRowNumber9.
• CommentAuthorUrs
• CommentTimeDec 7th 2018

Okay, I have added before that the line

The idea of opetopic sets (nlab) that Finster 18 is inspired by goes back to…

• CommentRowNumber10.
• CommentAuthorUrs
• CommentTimeDec 7th 2018
• (edited Dec 7th 2018)

changed “Leave” to “Leaves” in the section headline.

• CommentRowNumber11.
• CommentAuthorUrs
• CommentTimeDec 7th 2018

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.

• CommentRowNumber12.
• CommentAuthorAli Caglayan
• CommentTimeDec 7th 2018
• (edited Dec 7th 2018)

@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:

• Fix styling and stick to it
• Write out main ideas in the talk
• Try and relate ideas to Baez-Dolan and elsewhere
• CommentRowNumber13.
• CommentAuthorAli Caglayan
• CommentTimeDec 7th 2018

Changing style

• CommentRowNumber14.
• CommentAuthorAli Caglayan
• CommentTimeDec 7th 2018

Fixed phrasing as Urs pointed out.

• CommentRowNumber15.
• CommentAuthorAli Caglayan
• CommentTimeDec 7th 2018
• (edited Dec 7th 2018)

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 $\phi$ is defined there is talk of $J$ I am assuming this means $I$.

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)

• CommentRowNumber16.
• CommentAuthorAli Caglayan
• CommentTimeDec 7th 2018

Added an example of polynomial, and discussed how these get more complicated as we relax the conditions on types.

• CommentRowNumber17.
• CommentAuthorAli Caglayan
• CommentTimeDec 24th 2018

added small overview of talk, and started definition of frame.

• CommentRowNumber18.
• CommentAuthorAli Caglayan
• CommentTimeJan 10th 2019

• CommentRowNumber19.
• CommentAuthoratmacen
• CommentTimeFeb 19th 2019
Does anyone know the news with this project? Have algebras been defined successfully? (If I recall, that was the next thing to happen at the time of the HoTTEST talk.) Is this looking like a shot at autophagy?
• CommentRowNumber20.
• CommentAuthorAli Caglayan
• CommentTimeFeb 19th 2019

@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.

• CommentRowNumber21.
• CommentAuthorAli Caglayan
• CommentTimeMar 16th 2019

added Eric’s notes on his definition of higher structure.