Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory object of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > HoTT: Latest Changes: HoTT: Eric Finster, Towards Higher Universal Algebra in Type Theory

Bottom of Page

1 to 21 of 21

  1.  
    • CommentRowNumber1.
    • CommentAuthorAli Caglayan
    • CommentTimeDec 6th 2018

    Page created, but author did not leave any comments.

    v1, current

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeDec 7th 2018

    added an Idea-section and added “bibliographical” data for the reference

    diff, v2, current

    • CommentRowNumber3.
    • CommentAuthorAli Caglayan
    • CommentTimeDec 7th 2018

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

    diff, v3, current

    • CommentRowNumber4.
    • CommentAuthorAli Caglayan
    • CommentTimeDec 7th 2018

    added Baez and Dolan reference from video

    diff, v3, current

    • 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

    diff, v4, current

    • CommentRowNumber8.
    • CommentAuthorAli Caglayan
    • CommentTimeDec 7th 2018

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

    diff, v5, current

    • 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…

    diff, v6, current

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

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

    diff, v6, current

    • 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

    diff, v7, current

    • CommentRowNumber14.
    • CommentAuthorAli Caglayan
    • CommentTimeDec 7th 2018

    Fixed phrasing as Urs pointed out.

    diff, v7, current

    • 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 JJ I am assuming this means II.

    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)

    diff, v7, current

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

    diff, v8, current

    • CommentRowNumber17.
    • CommentAuthorAli Caglayan
    • CommentTimeDec 24th 2018

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

    diff, v10, current

    • CommentRowNumber18.
    • CommentAuthorAli Caglayan
    • CommentTimeJan 10th 2019

    Made and added a compact version of Eric’s slides without animation

    diff, v12, current

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

    diff, v14, current

1 to 21 of 21

  1.