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.
Steiner gave a beautiful description of the so-called Crans-Gray tensor product in the paper that I linked which gives a simple description of the tensor product of strict ω-categories that admit a basis with certain loop-freeness assumptions.
Among these objects are the objects of Θ, the orientals, the qbicals (defined by Crans), and a ton of other families of primitive shapes.
I’m surprised that this hasn’t gotten more coverage, especially since it’s about a trillion times easier to make sense of than Crans’s original paper, which is made obsolete by this paper, which is better in every way. It should be the standard reference.
I have added this link and a short description to Crans-Gray tensor product.
Also, not to disrespect Crans, but other mathematicians gave constructions of this tensor product before him (I believe there is an earlier construction using orientals by Street), and the nLab is the only place that calls it the Crans tensor product, so therefore, I recommend a name change to something like that “Lax Gray Tensor Product”.
It might also be instructive to show that the 2-categorical version is obtained by taking the 2-category whose 2-cells are connected 2-components and similarly that the same holds for the cartesian product of 1-categories.
I have added this link and a short description
Thanks. I have added added author name and links to the bib item.
I recommend a name change to something like that “Lax Gray Tensor Product”.
I’d have no objection to this change. I guess it may have been me who called this the “Crans-Gray tensor product”.
I’d like to hear what Tim Porter thinks of the suggested change; I expect he may have known Sjoerd better than anyone else here, and whether such a move would be just. (I’d also like to remind everyone to mind the possibility that Sjoerd could be listening in.) Me, I don’t have any particular objections.
I sort of do not like ascribing ideas to people anyhow. Perhaps a gloss added to an entry is a good idea, something along the lines:
The original tensor product seems first to have appeared in Gray’s 19?? lecture notes in the particular case of a …. It tends to be called the Gray tensor product and that usage has been adopted here. This construction was adapted and extended by Crans to handle the lax case in his paper / thesis, in 199? (I am guessing dates) The construction has over the years become simplified in its presentation and one of the clearest versions is probably in the work of Steiner.
The terminology of ’Gray tensor product’ is not that useful, but is now established. Attaching personal names to concepts fairly gives silly strings of names none of which really explain what the concept is. This is true even for theorems! As long as Sjoerd’s contribution to the development is fully acknowledged in the entry, and in the references, then my preference would be for Lax Gray tensor or something like that (although I do not really like that either. :-( )
Moreover, it seems that Crans is more famous for his construction of the tensor product of teisi, which is probably the correct thing to give him credit for (Batanin, Cisinski, and Weber have published papers on multitensors to generalize his work on the tensor product of teisi.
It’s also worth noting that Steiner’s construction allows us to define the lax join of strict ω-categories.
The name “Gray tensor product” is coincidentally evocative of its meaning, as being halfway between the “black tensor product” (the cartesian product, with all naturality squares filled in by identities) and the “white tensor product” (the “funny product” with all naturality squares filled in by nothing). (-:
I always have trouble remembering which is “black” and which is “white”. :-)
I don’t think it really matters; no one calls them that anyway. All that matters is that “gray” is in between. (-: I’m not even sure I got it “right” (whatever that means), but I always say that black is the one that’s “filled in” with an equality.
Is the original 2-pseudo Gray tensor product symmetric (even up to an equivalence)?
@Harry, I think so.
Hmm.. I wonder if there’s a way to construct an ω-pseudo Gray tensor product that is symmetric up to ω-equivalence in the sense of LMW.
I took “Coherence for Tricategories” out from the library. I’m interested to hear input from you guys!
An idea I have is as follows: There should exist an adjoint factorization of a morphism in str-ω-cat into an LMW cofibration followed by an LMW trivial fibration (I’m thinking of the paper about comonadic cofibrant replacements by Richard Garner). Then the Pseudo-tensor should be a universal factorization of the canonical map from the Lax Gray tensor to the cartesian product into an LMW cofibration followed by a LMW trivial fibration. This should be a relative form of the polygraph replacement. The universality of this factorization should yield a symmetry map.
Gray’s original tensor product was lax — the 2-cell filling the square was not even invertible. I believe Gordon-Power-Street were the first to call it the “Gray tensor product” and specialize to the pseudo version, which is symmetric up to isomorphism.
Yup, the lax Gray tensor product of ω-categories is lax as well. And I have a reasonable idea how to find a pseudo version.
The trick is to find the relative version of the polygraphic resolution of Métayer.
That is, for a strict ω-category X, one must define a relative polygraph under X, then show that there is a universal way to form a resolution under X of any map .
This should also work if we replace the lax Gray tensor product with the “white” tensor product and take relative resolutions.
However, I’m not sure how to define the “white” tensor product or relative polygraphs.
Oh, hmm.. Check this out:
Suppose we have a “white” tensor product of strict ω-categories, which we denote by . There is a natural map for every pair and , and moreover, the symmetry morphisms commute with these transformations.
Then for some choices of functorial factorization in the category of strict ω-categories into a cofibration followed by a trivial fibration, we obtain a symmetric-monoidal pseudo-Gray tensor product. I’m not sure that it will be closed, but maybe there’s a way to show that it will always be closed!
Also, I think that the “white” tensor product might be induced by taking a special subcomplex of Steiner’s tensor product of augmented directed complexes.
Is it associative?
I can give you the formula for the white tensor product, but the whole idea of using factorizations doesn’t seem to work in an obvious way:
We define the white tensor product of augmented directed complexes to be the subcomplex of the tensor product given by the “extremal” submodules:
This can be seen to define a symmetric monoidal product on augmented directed complexes, and moreover, that it extends to a symmetric monoidal product of strict ω-categories.
Yes, sure. But I’ll be impressed if the Gray version defined by a factorization comes out to be associative; I spent quite a while going down that route in a similar situation once and never got anywhere. (-:
The page describes the tensor product on strict -groupoids by Brown-Higgins. Is this relevant to type theory? Michael Warren showed that we can interpret a (non-univalent) type theory in that category.
By a funny coincidence, I have been thinking about exactly this question. I will work with strict cubical -groupoids in what follows instead of their globular cousins.
It is certainly the case that strict cubical -groupoids model at least the fragment of intensional Martin-Löf type theory involving identity types that is described in this paper of van den Berg and Garner.
One can indeed go further: it is easy to see that the category of strict cubical -groupoids has an interval equipped with all the structures discussed in VI of my thesis. Using the closed monoidal structure on strict cubical -groupoids, one therefore obtains immediately, from the main result of my thesis, a model structure on strict cubical -groupoids. This model structure has very strong properties, and in particular the factorisations have the same strong properties as those in the paper of van den Berg and Garner: thus one obtains a model of the fragment of Martin-Löf type theory mentioned above.
I make use of a slight reworking of van den Berg and Garner’s ideas in my thesis: one point of difference, relevant when discussing cubical sets or structures upon them, is that I use ’connection structures’ instead of a ’strength’. The principal reason that van den Berg and Garner use ’strengths’ are that the Moore co-cylinder type gadgets that they work with do not have connections (although I think there are other ways around this than using strengths).
As an intriguing aside, one of the key ideas in the paper of van den Berg and Garner is the use of what I refer to as ’strictness of identities’: I had arrived at the significance of this in the course of demonstrating that the lifting axioms for a model structure hold, and van den Berg and Garner independently arrived at it in the course of demonstrating the existence of factorisations!
Back to the type theory. Obviously a full model structure is much more than just factorisations. The question is: does this model structure capture more of Martin-Löf type theory than just the fragment mentioned above? I am optimistic about this, and it is this that I have been thinking about.
I am optimistic that one might be able to obtain a model of a large part of Martin-Löf type theory in any ’cylindrical homotopy theory’: that is, a category equipped with the kind of structures considered in my thesis. As discussed above, one will always be able to model identity types. The main point that I am interested in at the moment is in demonstrating that dependent products can be modelled. I conjecture that, in any cylindrical homotopy theory, fibrations behave as in , namely that they are exponentiable, as needed to model dependent products.
I have not thought about, and am indeed not particularly interested in (!), the univalence axiom in this setting. However, the model in strict cubical -groupoids should at least be a good place to look to model universes.
Also, whilst I do not know much about it, the existence of a full model structure might open the possibility that higher inductive types could be modelled.
To be continued in the next post (reached the character limit)…
Continued from above…
A few more thoughts. One thing that is very important in the ’cylindrical homotopy theory’ approach is the use of ’strictness’ of certain structures, as already mentioned. I think that it may be better to try to construct the model of Martin-Löf type theory in cylindrical homotopy theory directly from the syntax, without passing through an algebraisation such as Pitts’ type categories, or any of the other variants. Indeed, such algebraisations of course introduce difficulties with ’coherence’, and it may be that the strictness that one has in a cylindrical homotopy theory can better model directly the ’strictness’ of the syntax that causes the difficulties in the categorical algebraisations.
Secondly, I think that the point of view of cylindrical homotopy theory could be used to rework the cubical set model of Bezem, Coquand, and Huber in what I would consider to be a more conceptual way. Everything in their paper up to univalence should be understandable through the lens of cylindrical homotopy theory modulo one difficulty: constructing a closed monoidal structure on the category of cubical algebraic Kan complexes. This category is perfectly suited to cylindrical homotopy theory (it has, for instance, unlike the category of cubical sets or the ordiinary category of Kan complexes, a subdivision structure), except that it is not at all obvious to me how to construct the correct monoidal structure: if anyone does not believe me that it is tricky, I invite you to give it a go! If you can see how to do it, I would love to know: there are many purposes to which I would like to put this monoidal structure to use! I have some vague ideas that using a monoidal structure similar to that on strict cubical -groupoids, but on something weaker (say ’cubical -magmas’, a little bit as in Penon’s approach to algebraic higher categories), might be useful.
I discussed with Thierry Coquand a little when he was working on the cubical set model whether one could use algebraic Kan complexes, and he mentioned that he had thought about something like this. One certainly needs to add some ’compatibility conditions’, such as that ’degenerate horns’ lift to degeneracies.
Thirdly, whilst I have written this before and do not wish to sound like a broken record, I think that in general there are many aspects of the theory of cubical sets and cubical higher categories that have not yet been appreciated amongst homotopy theorists or amongst type theorists. One fundamental one, related to your question, is that it is the ’topological’ monoidal structure that should be used if one wishes to do anything conceptual, not the cartesian one. Bezem, Coquand, and Huber use the cartesian one, which they get away with because they are working with Kan complexes, but, as above, I think the theory would look much nicer if re-worked to use the topological structure.
Fourthly, I think that the closed monoidal structure on strict cubical -groupoids can be understood in a simple way conceptually, as follows. Essentially by definition, the category of cubes is strict monoidal. By Day convolution, the category of cubical sets is thus closed monoidal. Cubical strict -groupoids are algebras for a monad on cubical sets. One should be able to transfer this closed monoidal structure ’across the monad’. I believe that old work of Anders Kock explains how to do this.
Fifthly, perhaps it is worth mentioning that the cylindrical homotopy theory approach would also give for example a model of (at least part of) Martin-Löf type theory in chain complexes, a model in groupoids, and so on: thus, most of the existing models that I am aware of.
I haven’t yet been able to think of any way to use non-cartesian monoidal structures to model the cartesian structures (product and exponential) of ordinary type theory (as opposed to, say, some linear-logic-like type theory, which would be interesting but not exactly what we want).
Richard, thanks for all these interesting remarks! The strict model is quite well understood; see the discussion here. It is not so clear how useful HITs are without univalence, but it may serve as an interesting counter model.
I believe this work by Cheng and Leinster is a start to generalize the monad you describe to weak structures.
Thank you for the links, Bas. Yes, it does seem that many of the ways in which a model in strict -groupoids might be investigated from a type theoretical point of view seem to be understood to a good degree. Just a few remarks related to my thoughts above after skimming the discussion.
1) It seems that there might be an interest in a full model structure on strict -groupoids.
2) The model structure that I mentioned is different from any that would be constructed along the lines of the model structure of Lafont, Metayer, and Worytkiewicz on strict -categories. In the model structure that I described, every object is both cofibrant and fibrant, whereas this is not the case for a model structure constructed à la Lafont, Metayer, and Worytkiewicz.
3) ’Normality’ (a strictness condition on lifting of identities) is also crucial for obtaining the kind of ’cylindrical model structure’ that I discussed. It can however be required of the cofibrations instead of the fibrations: there are usually two model structures that come from a cylindrical homotopy theory.
4) I feel that to understand a strict -groupoid model in a broader setting of models in ’cylindrical homotopy theory’ would be probably the most interesting aspect of the picture I described above.
Thank you for mentioning the paper of Cheng and Leinster, I had not thought before about its relevance to what I was describing: I will do so!
Regarding Mike’s comment: I would like to say more, but will wait until such a time as I can give more details. For now, just a couple of remarks.
1) One can at least model the fragment of Martin-Löf type theory involving identity types, that van den Berg and Garner consider, in the cylindrical setting that I described, regardless of whether it comes from a cartesian or an arbitrary monoidal structure.
2) It is of course possible that one could use a non-cartesian monoidal structure for ’building the model (i.e. the homotopy theory)’, whilst specific types might be able to be modelled by cartesian structures. In some circumstances, of course, a cartesian product (or something more general) will have ’the correct homotopy type’ if one works with fibrant objects: this is exactly the case for the cubical set model that Bezem, Coquand, and Huber consider. Thus I see no reason that one should not be able to ’build’ the cubical set model of Bezem, Coquand, and Huber using the ’correct’ monoidal structure from a homotopical point of view, even if one ultimately needs to work with the cartesian monoidal structure and fibrant objects for some purposes.
Why do you claim that the correct monoidal structure is non-cartesian? It’s something that comes up regularly, but it would be nice to have some precise arguments.
For me it just comes from the simple fact that the category of cubes (in its various flavours) is the free strict monoidal category on an interval (with various degrees of structure). The category of semi-cubes is the free strict monoidal category on a bare interval; the category of cubes is the free strict monoidal category on an interval with a ’contraction’ structure; the category of cubes with connections is the free strict monoidal category on an interval with a ’contraction’ structure and ’connection’ structures; and so on.
An interval is precisely what one needs to define a notion of homotopy. The additional structures correspond to extra structure in the homotopy theory: a ’contraction’ structure allows one to define constant homotopies; an ’involution’ structure allows one to reverse homotopies; connection structures allow one to construct double homotopies with certain specific boundary faces; and so on. Taking the free strict monoidal category extends in a canonical way this structure to all dimensions.
Thus I see the various flavours of categories of cubes as universal for defining a notion of homotopy. For more on this point of view, you may like to take a look at these notes. I am not entirely happy with them: there are some minor errors/typos, and I now think about some aspects in a slightly different way. Nevertheless it seems that some people have found them helpful, so maybe you will get something out of them.
The canonical way to work with the category of cubes is to make use of its universal property (actually its 2-universal property is also extremely useful). Thus one constructs the geometric realisation functor to topological spaces just by saying where the (structured) interval goes, etc. In particular, the category of cubical sets (of various flavours) inherits a (closed) monoidal structure and a structured interval from the category of cubes itself. In other words, I see the category of cubical sets as defined by two universal constructions, which happily interact nicely due to Day convolution: one first constructs the universal example of a category equipped with a structured interval, and then universally adds colimits. In particular, I see the structured interval in cubical sets as the canonical choice for defining homotopy theory (and it is necessary to make this choice for compatibility with the canonical definition of the geometric realisation functor to topological spaces that I mentioned, and any other functor defined in a similar way).
There are also innumerable places, when one works with cubical sets in a ’canonical way’, where one can carry out arguments much more cleanly, constructively, and conceptually, due to the fact that one can use a universal property: the corresponding arguments for simplicial sets are much more intricate, and usually difficult to make constructive. Essentially anything to do with products or exponentials will illustrate this: however this is something that I think one needs to work with in practise to fully appreciate.
Just to summarise what I wrote in a slightly different way, in case it wasn’t clear how what I wrote answers your question: the ’correct’ monoidal structure on cubical sets, from a homotopical point of view, is for me clearly the one which agrees on representable presheaves with the defining universal property of the category of cubes.
One example which might be helpful is the following. An important property of the geometric realisation functor from simplicial sets to topological spaces is that it preserves products. However, this result is messy (I am aware of this paper of Drinfeld and similar work of others, but it does not change my opinion!), and does not hold if one works with , the category of all topological spaces.
By contrast, it is entirely formal that the geometric realisation functor from cubical sets to , the category of all topological spaces, commutes with the tensor product coming from Day convolution. It is not even true (not even up to homotopy) that the geometric realisation of the cartesian product of two copies of the representable 1-cube is (although this is corrected if one works instead with cubes with connections).
Somehow the product of the representable 1-simplex is pretty poorly behaved: it is the degeneracies that save the day from the point of view of geometric realisation. It is not good from a constructive point of view to rely upon degeneracies in an important way: a significant difficulty with working with simplicial sets from a constructive point of view is that one cannot separate simplices into those which are degenerate and those which are not.
A recent example of difficulties with working with products of simplicial sets is this paper of Fjellbo and Rognes. Their Theorem 1.2 is entirely formal, with a one sentence proof, if one instead works with cubical sets, the tensor product on them instead of the cartesian product, and the obvious notion of cubical subdivision. Compare this to the extremely intricate combinatorial constructions which Fjellbo and Rognes use. Of course, one of their applications is to simple homotopy theory, which is phrased in the language of simplicial sets, but there is no reason that I see that it could not instead be approached cubically.
The real reason why geometric realization of simplicial sets commutes with finite limits is that simplicial sets are a classifying topos and geometric realization is the inverse image part of the geometric morphism that classifies . The fact that is is not strictly true because topological spaces are not a topos and thus there is messy point-set-topology involved should be blamed on topological spaces, not on simplicial sets!
Well, it takes quite a lot of work to show that simplicial sets are a classifying topos in the required sense. I also don’t find the fact that simplicial sets are a classifying topos for linear orders to be a good conceptual explanation for why they might be of significance in homotopy theory, or to abstract in a satisfactory way the properties of the unit interval that are relevant for homotopy theory. I would also say that topological spaces (or a constructive replacement) are a perfectly reasonable category, even if not a topos: I have not found any topos theoretic variant that I would consider to be more natural.
Moreover, as I wrote, the issue with products of simplicial sets is more fundamental than the difficulties with showing that geometric realisation commutes with them: this was just as an example to illustrate how, when working cubically, the result is entirely formal and holds for conceptual reasons which come immediately from the universal construction of cubical sets.
Topological spaces are indeed a perfectly reasonable category in their own right, but as a model for -groupoids I think they leave something to be desired. There are topos-theoretic variants, like the topological topos, which are certainly not less natural from the perspective of modeling -groupoids (a purpose for which I think using any kind of topological space is arguably a sort of kludge anyway).
I don’t dispute that there are plenty of nice things about cubical sets, although I’m not yet convinced that the benefits of the non-cartesian monoidal structure outweigh its non-cartesian-ness (likely it depends on the purpose one has in mind).
Yes, I certainly agree that topological spaces are not good models of -groupoids! However, I see the homotopy hypothesis as asserting the equivalence of three homotopy theories: that of -groupoids to the left, that of a presheaf model of homotopy types (say simplicial sets or cubical sets) in the middle, and something like topological spaces to the right.
I do think that the right hand side of this picture is important: to be able to demonstrate a Quillen equivalence (or the appropriate analogue for whatever notion of abstract homotopy theory one is working with) between a category of presheaf models of homotopy types and a category similar to topological spaces. For me, it is also important to demonstrate this Quillen equivalence (and indeed construct the homotopy theories) in a constructive way.
The reason that I think this important is because there are so many more maps between the geometric realisations of simplical/cubical sets than between simplicial/cubical sets themselves, which gives the homotopy theory of topological spaces an a priori much richer structure: it is important to justify why we do not in fact lose anything up to homotopy by working only with simplicial/cubical sets.
I agree, though, that even for many topological purposes, it is better to work with some other category. I am very interested in knot theory (and higher dimensional analogues) for instance, and like to work with cubical sets ’up to subdivision’ instead of topological spaces themselves, thinking of this as a good category in which to do ’piecewise linear topology’. But even so I feel this should be justified: this is why I think that the simplicial approximation theorem (or a cubical analogue) is really absolutely fundamental.
Regarding the non-cartesian monoidal structure on cubical sets, yes, I of course agree that its appropriateness may depend on the purpose at hand. However, I do think that if one wishes to have a notion of cubical homotopy with respect to an interval (just like we have a notion of simplicial homotopy with respect to the simplicial interval), not only a notion of weak equivalence, then it is absolutely clear that one has to use the non-cartesian monoidal structure. As will be evident, I myself would go much further, but I think this much is indisputable.
I do think that if one wishes to have a notion of cubical homotopy with respect to an interval… then it is absolutely clear that one has to use the non-cartesian monoidal structure.
Isn’t it true that if we’re willing to restrict to fibrant cubical sets, then we can use the cartesian monoidal structure and a fibrant replacement of the cubical interval?
Yes, that is true. However, one should be careful: one needs a model structure on (the whole category of) cubical sets and a proof that it is Quillen equivalent to that on simplicial sets, or to the Serre model structure on topological spaces, or at least some other way of justifying the passage to cubical Kan complexes and the use of the cartesian monoidal structure.
For this it seems to me crucial to use the non-cartesian monoidal structure. This work of Cisinski (section 8.4) is the only way (there are a couple of papers of Jardine, but they are closely related to Cisinski’s work) that is in the literature to put a model structure on cubical sets, and prove that it is Quillen equivalent to the model structure on simplicial sets. It uses the non-cartesian monoidal structure heavily. I have a different way to put the model structure on, but this also uses the non-cartesian monoidal structure heavily.
In addition, the category of cubical Kan complexes is, like many categories of fibrant or cofibrant objects of a model category, not particularly nice. I would be very skeptical that one could do much serious homotopy theory working in this category alone, without passing to and from the whole category of cubical sets: and then one will need the non-cartesian monoidal structure even if one begins with using the cartesian one amongst Kan complexes.
Well, a model of type theory sees only the fibrant objects, so anything we can do in type theory we can do with only the cubical Kan complexes… (-:
That is an interesting point. It seems to me that the way to think about this is that the model of type theory in cubical Kan complexes somehow needs only those aspects of cubical Kan complexes that are relevant for homotopy theory, and of course we know that Kan complexes are good models of homotopy types, that Kan fibrations are good notions of fibrations, etc. However, the work typically carried out to establish that Kan complexes have these good homotopical properties is typically not very category theoretic: it doesn’t rely significantly on the properties of the category of Kan complexes.
From this point of view, one way to think of what I am proposing with regard to a ’more conceptual’ approach to the model in cubical sets is that using the non-cartesian monoidal structure should allow for a more category theoretic construction: the properties demonstrated by Bezem, Coquand and Huber should be able to understood generally in the setting of a cylindrical homotopy theory, or similar, which is an entirely category theoretic framework.
Thus I see the point you make as follows: the type theory gives some kind of ’replacement’ for the poor category theoretic properties of the category of Kan complexes. In other words, it turns out, rather interestingly, that even though a priori the category of Kan complexes seems poorly behaved, one can work ’internally’ to it in a much nicer way.
I have two points of caution about going too far with this point of view, though. Firstly, for higher inductive types and the like, doesn’t one need something more like a full model structure?
Secondly, it is very important to remember that Bezem, Coquand, and Huber add some extra conditions to the notion of a cubical Kan complex in order to be able to work with cubical Kan complexes constructively. The only natural way to define the category of Kan complexes in a constructive setting is to ask that all structure be respected by the maps. This kind of thing dramatically improves the category of Kan complexes. This was exactly a point I made in my original message: it is my opinion that the category of algebraic cubical Kan complexes (where horn fillings are a structure which one asks to satisfy certain compatibility conditions, and, crucially, the arrows are those morphisms of cubical sets that respect the structure of the horn fillings) is an excellent category to work in. Given the construction of the closed monoidal structure on it that I mentioned to be tricky, it would admit a cylindrical homotopy theory, and I conjecture that the model structure that results would be Quillen equivalent to the usual one on cubical sets/simplicial sets/topological spaces (the Serre version). This would be a very strong result, of a homotopy hypothesis-like nature.
I would say, rather, that type theory shows that the category of Kan complexes, while poorly behaved in ways that we’ve come to expect from classical homotopy theory, is well behaved in certain other ways that can serve as a replacement. For instance, in my paper “Univalence for inverse diagrams and homotopy canonicity”, I showed that a type-theoretic fibration category (an abstraction of the structure possessed by any model of type theory) has many properties that are familiar from model categories, but whose model-categorical proofs require things like colimits and cofibrations that are not present in a type-theoretic fibration category.
It’s true that our main current way to construct HITs uses a full model structure, but it also uses the cartesian nature of that model structure, so it wouldn’t work in cubical sets anyway. However, the cubical model of BCH is explicit enough that one might hope to be able to construct HITs more directly rather than by invoking the sort of abstract transfinite constructions currently used.
Regarding the first paragraph: yes, that was the kind of thing I was getting at.
Regarding the second paragraph: I don’t know much about higher inductive types (my interest in intensional type theory so far tends in different directions), but it would certainly be nice to avoid transfinite constructions and the like!
1 to 39 of 39