Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

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 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 internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure 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 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

1. • CommentRowNumber1.
   • CommentAuthorAli Caglayan
   • CommentTimeDec 6th 2018
   • (edited Dec 6th 2018)
   • PermaLink
   Author: Ali Caglayan
   Format: MarkdownItexEric gave a very cool talk today. [E. Finster, "Towards Higher Universal Algebra in Type Theory"](https://www.youtube.com/watch?v=hlCVHVtAlqQ) He says that he might have a definition of a *cartesian polynomial monad* in HoTT. Special cases of this definition give: * $(\infty, 1)$-operad * $(\infty, 1)$-category * $\infty$-groupoid all in HoTT! This may be a solution to the infinite cohereance problem in HoTT. Now Eric hasn't actually written up any details however there is a [work in progress formalisation in agda](https://github.com/ericfinster/higher-alg). It would be good to go through the video, and the agda formalisation and see if we can play with the definitions here on the nlab.

   Eric gave a very cool talk today.

   E. Finster, “Towards Higher Universal Algebra in Type Theory”

   He says that he might have a definition of a cartesian polynomial monad in HoTT.

   Special cases of this definition give:

   • $(\infty, 1)$-operad
   • $(\infty, 1)$-category
   • $\infty$-groupoid

   all in HoTT!

   This may be a solution to the infinite cohereance problem in HoTT.

   Now Eric hasn’t actually written up any details however there is a work in progress formalisation in agda.

   It would be good to go through the video, and the agda formalisation and see if we can play with the definitions here on the nlab.

2. • CommentRowNumber2.
   • CommentAuthorAli Caglayan
   • CommentTimeDec 6th 2018
   • (edited Dec 6th 2018)
   • PermaLink
   Author: Ali Caglayan
   Format: MarkdownItexI have created a page on the HoTT wiki: [[homotopytypetheory:Eric Finster, Towards Higher Universal Algebra in Type Theory]]

   I have created a page on the HoTT wiki: Eric Finster, Towards Higher Universal Algebra in Type Theory (homotopytypetheory)

3. • CommentRowNumber3.
   • CommentAuthorAli Caglayan
   • CommentTimeDec 6th 2018
   • PermaLink
   Author: Ali Caglayan
   Format: MarkdownItexMy first comments would be that these trees are simply just abstract syntax trees, for example as in Harper?

   My first comments would be that these trees are simply just abstract syntax trees, for example as in Harper?

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeDec 7th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexWell, I think ASTs are generally restricted to be finitary, and to have a *set* (indeed, usually a finite set) of sorts and operations. Polynomial monads can have operations of infinite arity, and when defined in HoTT as in Eric's approach the types of sorts and operations can have unbounded h-level. Moreover I think the treatment of variables may be somewhat different, haven't thought about it carefully. However, in principle, yes, ASTs are a syntactic way of talking about free things of this sort. I'm very excited about Eric's definition; he shared a few of the details with me before his talk, so I've had a little longer to think about it, and I still find it the most believable proposal for solving the infinite coherence problem that I've ever heard. Time will tell whether it actually works.

   Well, I think ASTs are generally restricted to be finitary, and to have a set (indeed, usually a finite set) of sorts and operations. Polynomial monads can have operations of infinite arity, and when defined in HoTT as in Eric’s approach the types of sorts and operations can have unbounded h-level. Moreover I think the treatment of variables may be somewhat different, haven’t thought about it carefully. However, in principle, yes, ASTs are a syntactic way of talking about free things of this sort.

   I’m very excited about Eric’s definition; he shared a few of the details with me before his talk, so I’ve had a little longer to think about it, and I still find it the most believable proposal for solving the infinite coherence problem that I’ve ever heard. Time will tell whether it actually works.

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeDec 7th 2018
   • PermaLink
   Author: Urs
   Format: MarkdownItexFrom the talk it looks like Eric succeeded in formalizing his [[opetopic type theory]] within dependent type theory.

   From the talk it looks like Eric succeeded in formalizing his opetopic type theory within dependent type theory.

6. • CommentRowNumber6.
   • CommentAuthorDavidRoberts
   • CommentTimeDec 7th 2018
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexFor what it's worth, others are working on other approaches to opetopes: [opetopy](https://github.com/altaris/opetopy), written in Python.

   For what it’s worth, others are working on other approaches to opetopes: opetopy, written in Python.

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeDec 7th 2018
   • (edited Dec 7th 2018)
   • PermaLink
   Author: Urs
   Format: MarkdownItexDo you have a pointer to something that tries to be more like a message than the git-hub pages? (Being sent to git-hub always feels like somebody is pointing me to their root directory without further comment.)

   Do you have a pointer to something that tries to be more like a message than the git-hub pages? (Being sent to git-hub always feels like somebody is pointing me to their root directory without further comment.)

8. • CommentRowNumber8.
   • CommentAuthorAli Caglayan
   • CommentTimeDec 7th 2018
   • PermaLink
   Author: Ali Caglayan
   Format: MarkdownItex@Urs In the doc folder there is a file called index.rst which has some documentation.

   @Urs In the doc folder there is a file called index.rst which has some documentation.

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeDec 7th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI don't think it's quite opetopic type theory (although maybe Eric can comment). The pictures look similar, and the slice construction on multicategories is also what was used by Baez-Dolan to formalize opetopes, but the "relations" that arise are all essentially "graphs of functions" and so all the higher structure here is actually algebraic. Perhaps an $\infty$-(pre)category in Eric's new sense could be described as an opetopic space in which every horn has a contractible space of fillers?

   I don’t think it’s quite opetopic type theory (although maybe Eric can comment). The pictures look similar, and the slice construction on multicategories is also what was used by Baez-Dolan to formalize opetopes, but the “relations” that arise are all essentially “graphs of functions” and so all the higher structure here is actually algebraic.

   Perhaps an $\infty$-(pre)category in Eric’s new sense could be described as an opetopic space in which every horn has a contractible space of fillers?

10. • CommentRowNumber10.
    • CommentAuthorericfinster
    • CommentTimeDec 7th 2018
    • PermaLink
    Author: ericfinster
    Format: MarkdownItexYes, opetopic type theory was an attempt to implement directly the theory of opetopic $(\infty,\infty)$-categories. This proposal is certainly inspired by many of the same ideas, but is really just the $(\infty,1)$ "fragment". On the other hand, I think that starting from this fragment, we should fairly easily be able to import Baez and Dolan's notion of n-coherent algebra, and hence have a definition of $(\infty,n)$-category. @Mike: Yes, this was actually the approach that I took first: an infinite sequence of what I called "polynomial relations" (serving as a notion of opetopic type) such that every horn had a contractible space of fillers. So I think your intuition is right on. There turn out to be some subtleties with this approach which are a bit annoying, though it is probably possible to give a reasonable definition along these lines. It occurred to me, however, that after finishing such a definition, one would be able to *prove* that the filling spaces were equivalent to identity types for a multiplication definable from the fact that the spaces of fillers were contractible. So it seems much more natural (and it ends up avoiding the subtleties I mentioned) to just use the identity types directly.

    Yes, opetopic type theory was an attempt to implement directly the theory of opetopic $(\infty,\infty)$-categories. This proposal is certainly inspired by many of the same ideas, but is really just the $(\infty,1)$ “fragment”.

    On the other hand, I think that starting from this fragment, we should fairly easily be able to import Baez and Dolan’s notion of n-coherent algebra, and hence have a definition of $(\infty,n)$-category.

    @Mike: Yes, this was actually the approach that I took first: an infinite sequence of what I called “polynomial relations” (serving as a notion of opetopic type) such that every horn had a contractible space of fillers. So I think your intuition is right on. There turn out to be some subtleties with this approach which are a bit annoying, though it is probably possible to give a reasonable definition along these lines. It occurred to me, however, that after finishing such a definition, one would be able to prove that the filling spaces were equivalent to identity types for a multiplication definable from the fact that the spaces of fillers were contractible.

    So it seems much more natural (and it ends up avoiding the subtleties I mentioned) to just use the identity types directly.

11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeDec 7th 2018
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexHi Eric, glad you could join the conversation. Yes, I agree that the way you've phrased the definition now is simpler and better for HoTT purposes. But the other description is also nice to have; in particular I am wondering whether it would be a helpful route to a semantic comparison with existing notions of $\infty$-category. For instance, the opetope category $\mathbb{O}$ is a direct category, so there is a Reedy model structure on $sSet^{\mathbb{O}^{op}}$, which one might hope to localize in order to make the fibrant objects be the ones for which every horn has a contractible space of fillers. Then one could try to build a Quillen equivalence relating this model category to some other model structure for $(\infty,1)$-categories.

    Hi Eric, glad you could join the conversation. Yes, I agree that the way you’ve phrased the definition now is simpler and better for HoTT purposes. But the other description is also nice to have; in particular I am wondering whether it would be a helpful route to a semantic comparison with existing notions of $\infty$-category. For instance, the opetope category $\mathbb{O}$ is a direct category, so there is a Reedy model structure on $sSet^{\mathbb{O}^{op}}$, which one might hope to localize in order to make the fibrant objects be the ones for which every horn has a contractible space of fillers. Then one could try to build a Quillen equivalence relating this model category to some other model structure for $(\infty,1)$-categories.

12. • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeDec 7th 2018
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexBy the way, I missed this during the talk or I would have commented on it at the time, but now looking at the slides and formalization I see that you are actually using Agda's primitive notion of "coinductive definition", which is an extension of MLTT/Book-HoTT. However, it seems that most or all coinductive definitions of this sort can also be written in an equivalent (though perhaps slightly less convenient) form as an internal limit of a tower indexed by the natural numbers type. In your case I think the way this would go is to first define *recursively* an "$(n+1)$-coherence structure" for $M$ to consist of a witness $\Psi : SubInvar(M)$ that $M$ is subdivision-invariant together with an $n$-coherence structure on the slice $SlcMgm(M,\Psi)$ (while a $0$-coherence structure is trivial). Then prove by induction that every $(n+1)$-coherence structure $C$ has an underlying $n$-coherence structure $U(C)$ on the same magma, and finally define an ($\infty$-)coherence structure to consist of an $n$-coherence structure $C_n$ for every $n$ together with equalities $U(C_{n+1})=C_n$.

    By the way, I missed this during the talk or I would have commented on it at the time, but now looking at the slides and formalization I see that you are actually using Agda’s primitive notion of “coinductive definition”, which is an extension of MLTT/Book-HoTT. However, it seems that most or all coinductive definitions of this sort can also be written in an equivalent (though perhaps slightly less convenient) form as an internal limit of a tower indexed by the natural numbers type. In your case I think the way this would go is to first define recursively an “$(n+1)$-coherence structure” for $M$ to consist of a witness $\Psi : SubInvar(M)$ that $M$ is subdivision-invariant together with an $n$-coherence structure on the slice $SlcMgm(M,\Psi)$ (while a $0$-coherence structure is trivial). Then prove by induction that every $(n+1)$-coherence structure $C$ has an underlying $n$-coherence structure $U(C)$ on the same magma, and finally define an ($\infty$-)coherence structure to consist of an $n$-coherence structure $C_n$ for every $n$ together with equalities $U(C_{n+1})=C_n$.

13. • CommentRowNumber13.
    • CommentAuthorericfinster
    • CommentTimeDec 8th 2018
    • PermaLink
    Author: ericfinster
    Format: MarkdownItexYes, so the approach of trying to link this definition with some kind of "opetopic spaces" seems natural. I agree. Since I do not think I have seen this concept studied in the literature, I guess the theory would need to be developed from scratch. Not that I think it's at all impossible, just that it will probably take a bit of work. Christian Sattler and I at one point had started to think about some comparisons between opetopic-sets and semi-simplicial sets. He had some nice ideas, so maybe it would be useful to revisit some of this. With regard to coinduction: yes, I meant to mention this during my talk but I guess it slipped my mind. I agree that I don't at all think it is fundamentally necessary, but just really convenient. Indeed, I was planning to introduce the notion of n-coherence structure anyway: one clearly wants a theorem along the lines of "if the space of operations is n-truncated then any (n+1)-coherence structure is $\infty$-coherent."

    Yes, so the approach of trying to link this definition with some kind of “opetopic spaces” seems natural. I agree. Since I do not think I have seen this concept studied in the literature, I guess the theory would need to be developed from scratch. Not that I think it’s at all impossible, just that it will probably take a bit of work. Christian Sattler and I at one point had started to think about some comparisons between opetopic-sets and semi-simplicial sets. He had some nice ideas, so maybe it would be useful to revisit some of this.

    With regard to coinduction: yes, I meant to mention this during my talk but I guess it slipped my mind. I agree that I don’t at all think it is fundamentally necessary, but just really convenient. Indeed, I was planning to introduce the notion of n-coherence structure anyway: one clearly wants a theorem along the lines of “if the space of operations is n-truncated then any (n+1)-coherence structure is $\infty$-coherent.”

14. • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeDec 8th 2018
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexCertainly, however we slice it (no pun intended) there's work to be done. Another idea would be to try to somehow mimic the slice construction semantically. Can we say for instance that for any polynomial $P$ and relations $R$ there is some kind of equivalence of homotopy theories between something over $P$ and something over the slice $P\sslash R$? This is very vague, but I have some vision of starting with a "classical" presentation of $(\infty,1)$-categories (or operads or whatever) and slicing it over and over again to get a tower of equivalent homotopy theories, then taking the limit to get a presentation using something like your definition. If this can be made sense of, it might be easier than trying to deal with the rather-complicated opetope category all at once.

    Certainly, however we slice it (no pun intended) there’s work to be done.

    Another idea would be to try to somehow mimic the slice construction semantically. Can we say for instance that for any polynomial $P$ and relations $R$ there is some kind of equivalence of homotopy theories between something over $P$ and something over the slice $P\sslash R$? This is very vague, but I have some vision of starting with a “classical” presentation of $(\infty,1)$-categories (or operads or whatever) and slicing it over and over again to get a tower of equivalent homotopy theories, then taking the limit to get a presentation using something like your definition. If this can be made sense of, it might be easier than trying to deal with the rather-complicated opetope category all at once.

15. • CommentRowNumber15.
    • CommentAuthorAli Caglayan
    • CommentTimeDec 11th 2018
    • PermaLink
    Author: Ali Caglayan
    Format: MarkdownItexI've started writing a coq version of Eric's library. I have it on a branch on my fork [here](https://github.com/Alizter/HoTT/tree/higher-alg/contrib/higher-alg). I have managed to define slicing, but I need to spend some more time understanding the Substritution.agda file. I started with annotating the universes, but it seems coq is okay doing that by itself so I removed them later.

    I’ve started writing a coq version of Eric’s library. I have it on a branch on my fork here. I have managed to define slicing, but I need to spend some more time understanding the Substritution.agda file. I started with annotating the universes, but it seems coq is okay doing that by itself so I removed them later.

16. • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeDec 11th 2018
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexGreat! If you're open to experimenting with alternatives, I would suggest trying out the style of polynomials where the sorts of parameters are assigned by a function rather than given by an index. That is, instead of Param {i : I} : Op i -> I -> Type; there would be something like Param {i : I} : Op i -> Type; SortOf {i : I} {f : Op i} : Param f -> I; I suspect that this would make some things in the development simpler (though there are a couple that it would make more complicated), and it would be nice to have it written down to compare with Eric's version.

    Great! If you’re open to experimenting with alternatives, I would suggest trying out the style of polynomials where the sorts of parameters are assigned by a function rather than given by an index. That is, instead of

    Param {i : I} : Op i -> I -> Type;
    

    there would be something like

    Param {i : I} : Op i -> Type;
    SortOf {i : I} {f : Op i} : Param f -> I;
    

    I suspect that this would make some things in the development simpler (though there are a couple that it would make more complicated), and it would be nice to have it written down to compare with Eric’s version.

17. • CommentRowNumber17.
    • CommentAuthorAli Caglayan
    • CommentTimeDec 11th 2018
    • PermaLink
    Author: Ali Caglayan
    Format: MarkdownItex@Mike I have tried your definition. I now have a file called Polynomial2.v, it seems to want less parameters which can help but I won't see its true utility until I prove some things about my definitions (or even see if they are really correct yet). For this I will need the notions of substitution but I haven't really understood how this works yet. There is a small corollary in Eric's Polynomial.agda file called corolla-frm which I am trying to write in coq but I haven't been able to power through it yet.

    @Mike I have tried your definition. I now have a file called Polynomial2.v, it seems to want less parameters which can help but I won’t see its true utility until I prove some things about my definitions (or even see if they are really correct yet). For this I will need the notions of substitution but I haven’t really understood how this works yet. There is a small corollary in Eric’s Polynomial.agda file called corolla-frm which I am trying to write in coq but I haven’t been able to power through it yet.

18. • CommentRowNumber18.
    • CommentAuthorAli Caglayan
    • CommentTimeDec 25th 2018
    • (edited Dec 25th 2018)
    • PermaLink
    Author: Ali Caglayan
    Format: MarkdownItexI have tried a [third attempt](https://github.com/Alizter/HoTT/blob/higher-alg/contrib/higher-alg/Polynomial3.v). I am getting stuck at formalising flatten however. It will require some more brainpower. I think I agree with Mike that SortOf helps the formalisation however.

    I have tried a third attempt. I am getting stuck at formalising flatten however. It will require some more brainpower. I think I agree with Mike that SortOf helps the formalisation however.