Understanding cubical type theory

[Richard Williamson]

I would like to understand the details of cubical type theory, but am having some difficulty in getting started! Would somebody be able to, say, 'walk through' this note of Thierry's? This note is the other one that I'm particularly interested in.

My background is that I have worked a lot on cubical sets, and I am also thoroughly acquainted with Martin-Löf type theory, with Coq, Haskell, etc. But my work on cubical sets has a somewhat different, more category-theoretic flavour to that used in Thierry's notes and all other work that I have seen on cubical type theory. I would like to try to understand things from the point of view I usually work with, and it is getting started with making this translation that I am having some difficulty with. 

I can understand the original work of Bezem, Coquand, and Huber from the point of view that I usually work in (and, excluding univalence, which I haven't thought about in this setting, believe to be able to do the same kind of thing in a different and more general way). But with the more heavy emphasis on nominal sets, etc, in more recent work, it is harder for me to get a feeling for things.

To be more concrete, I can begin with the second note that I linked to above. I would like to understand the category C that Thierry defines in the section 'Base (pre)category' in a way more familiar to me. I would like to define C 'structurally', that is to say as a 'free strict monoidal category'-like construction on a category Base with, say, three objects I^0, I^1, and I^2, and various arrows between. The only operations named by Thierry are connections and face maps. We can certainly define a category Base which encodes connections and face maps, and define C universally from Base (it is not simply the free strict monoidal category on Base, but I know how to define the relevant universal property). A presheaf on C would then be what I would call a 'semi-cubical set with connections'. My question is: are connections and face maps the only things that are important in Thierry's category C? In the first note that I linked to (the first section 'Interval'), it would seem that 'involutions' (aka 'reversals') should be built in as well? I have also seen some talk of including 'diagonals', but these do not seem to be explicitly used in either note?

My next questions regarding the second note is to do with the 'composition structure'. I wonder if this is related to work of Brown and Higgins on 'commutative n-cubes' in strict cubical infinity-groupoids, and to be able to see whether or not that is the case, it would be very helpful to understand visually what is going on in Thierry's note in low dimensions. What do the possible 'open boxes' used in Thierry's note to define fibrant cubical sets look like for 1-cubes, 2-cubes, and 3-cubes? It seems that they are more general than just 'horns'?

Finally, to get started with understanding the first note linked to above: could someone be so kind as to spell out the semantics of the 'basic typing rules' (being as geometric and low-dimensional as possible!)?

[Bas Spitters]

A few quick notes.

The cubical sets also contain diagonals. Hence we obtain a free
Cartesian category. We had a discussion here:
http://nforum.ncatlab.org/discussion/6528/cubes-with-diagonals/

The reversals are somewhat orthogonal, I believe. They provide extra
judgemental equalities, but do not clarify the presentation you are
looking at. I think they could be added without much changes.

The terminological overlap with Brown/Higgings "composition" is
accidental. They are looking at strict w-groupoids. I wondered about
that too before.

My own understanding of part of this model is here.
http://www.cs.au.dk/~spitters/TYPES15.pdf

It also works mutatis mutandis for the present model. I am currently
elaborating on the connection with Johnstone's topological topos, as I
presented it at Mittag-Leffler.

Best,

Bas

> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Richard Williamson]

Thank you for your reply, Bas! 

The cubical sets also contain diagonals. Hence we obtain a free
Cartesian category. We had a discussion here:
http://nforum.ncatlab.org/discussion/6528/cubes-with-diagonals/  

 

The reversals are somewhat orthogonal, I believe. They provide extra
judgemental equalities, but do not clarify the presentation you are
looking at. I think they could be added without much changes.

Yes, I understand how to include both diagonals and reversals from the 'structural' point of view that I mentioned. I was wondering whether or not they were needed for what Thierry is doing, because the category C is defined in a certain way in the second note, but only certain arrows are explicitly mentioned, and only certain things are included in the syntax in the first note. What I was looking for is exactly which arrows is needed, because this is important from a structural point of view. But, as you say, it seems that there is some freedom according to what one is looking to do as to whether to include diagonals, reversal, or neither. Connections seem indispensable, though. 

If one has connections, by the way, one cannot simply take a free cartesian category on some 'base category', as I think I mentioned in the discussion you linked to. But maybe you really meant 'free' in a more sophisticated sense. 

 

The terminological overlap with Brown/Higgings "composition" is
accidental. They are looking at strict w-groupoids. I wondered about
that too before.

Somebody else wrote to me in reply to say the same thing, so I'll copy what I wrote there here too! The aspect of the work of Brown and Higgins that I am referring to is not to do with the definition of an infinity-groupoid itself, but rather with certain techniques that they use to develop the notion of a 'commutative n-cube'. This is a non-trivial problem, as consideration even of the case of what a commutative 3-cube in a cubical 2-groupoid should be reveals (There is nothing specific to the cubical setting here: it is an equally non-trivial and important problem for any shape of higher category (globular, simplicial, etc), and in fact the cubical setting is, for me at least, the most natural one in which to consider it.) 

To solve this problem, Brown and Higgins introduce various ways to allow one to compose together faces of an n-cube (it is not obvious how to do this, especially in a way which leads to manageable combinatorics in higher dimensions). These ways are extremely closely related to the ability to fill in horns in cubical sets, and in particular are not necessarily only of interest in a strict setting.

It seems that Thierry and collaborators have found a way to relate some kind of composition/glueing to filling in horns in cubical sets too. Connections are crucial to this, and are also crucial in the work of Brown and Higgins. Thus I am very interested to find out what this composition/glueing involves, and if there is any resemblance to the work of Brown and Higgins. But I find the description in terms of sieves, etc, in Thierry's work hard to appreciate, and would find it much more helpful to see what is going in low dimensions! 

My own understanding of part of this model is here.
http://www.cs.au.dk/~spitters/TYPES15.pdf

Thank you very much for this! Could you elaborate (feel free to do so in private) upon how your Moore path category is in fact a category internal to cubical sets, i.e. what is the cubical set of objects, and what is the cubical set of arrows)? Also, a couple of remarks:

1) I think, for completely independent reasons, that higher groupoids in which reversals are not strict inverses, but everything else is strict, or at least most other things are strict, are very significant, and have not been investigated enough, even though this is the kind of higher groupoid that appears in the very first work on the homotopy hypothesis, in Kapranov-Voevodsky. 

2) The work of van den Berg and Garner can be carried out directly using connections (i.e. there is no need for a 'strength' if one has connections). I explain this in my thesis. Sometimes one does not have connections, as with the Moore path space in Top, but if one does have connections, then there is no need to use them to build a 'strength', as you say that you, following Simon Docherty, do. 

 

Best wishes,

Richard

[Martin Escardo]

I am watching this discussion with interest, and I look forward to
further discussion in this direction, which so far has been rather
illuminating (and mathematically entertaining).

But I think we should not forget the original motivation for Thierry
et. al. constructions.

HoTT (as in the book) is MLTT plus (1) an axiom, and (2) a new form of
inductive definition (whose new feature is the ability of define
equalities between points, in addition to points).

As soon as you add an axiom to MLTT, the computational content is
lost.

Both the cubical models developed by Thierry et al., and the
corresponding cubical type theories, have the virtue of (1) giving
computational content to the new axiom, and (2) giving computational
content to the new form of induction. And they were explicitly
developed for that purpose.

Now HoTT (as a formal theory) can be embedded into cubicalltt (except
for a minor wart discussed in other threads, which perhaps can be
fixed: cubicaltt doesn't validate a judgemental rule for path
induction, although it validates it up to a path).

In this sense, modulo the wart, cubicaltt is a solution to the
computational problem of HoTT.

From this, it shouldn't be inferred that cubical sets (of whatever
form) are the "preferred" model of HoTT. They are a way of getting the
computations (in formal HoTT) going.

And, moreover, the fact that the cubical model is presented in
unfamiliar terms to homotopy theorists is to be expected: it is
explicitly presented in such a way as to make its constructive content
explicit, for people familiar with constructivity, which, as expected,
is not necessarily the presentation that classical mathematicians
would favour.

Having said that, I think the contributions, in the form of questions,
discussions and challenges, about the cubical model(s) are very
interesting.

Perhaps, eventually, all this will be fully understood both
computationally and mathematically, without the need of making the
distinction between the two.

Martin

On 31/07/15 21:53, Richard Williamson wrote:
> Thank you for your reply, Bas!
>
> The cubical sets also contain diagonals. Hence we obtain a free
> Cartesian category. We had a discussion here:
> http://nforum.ncatlab.org/discussion/6528/cubes-with-diagonals/

> <http://www.google.com/url?q=http%3A%2F%2Fnforum.ncatlab.org%2Fdiscussion%2F6528%2Fcubes-with-diagonals%2F&sa=D&sntz=1&usg=AFQjCNFgfewYK3d1FhI5P7j6l-P8TAV47Q>

> <http://rwilliamson-mathematics.info/cylindrical_model_structures.html>.

> Sometimes one does not have connections, as with the Moore path space in

> Top, but if one /does/ have connections, then there is no need to use

> them to build a 'strength', as you say that you, following Simon
> Docherty, do.
>
> Best wishes,
> Richard
>

> --
> You received this message because you are subscribed to the Google
> Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to HomotopyTypeThe...@googlegroups.com

> <mailto:HomotopyTypeThe...@googlegroups.com>.

> For more options, visit https://groups.google.com/d/optout.

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe

[Andrej Bauer]

On Sat, Aug 1, 2015 at 12:18 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> And, moreover, the fact that the cubical model is presented in
> unfamiliar terms to homotopy theorists is to be expected:

Were it presented *also* in terms familiar to homotopy theorists and
other forms of mathematical life then we could expect many further
benefits and insights from the mathematical side of things. Is there
such a presentation?

With kind regards,

Andrej

[Bas Spitters]

No, I don't think there is. I've been trying to understand it also
from that perspective, too. I was glad to build a van den Berg/Garner
model on cubical sets, but I am not sure yet whether it is equivalent
to Thierry's model.
It seems reasonable to suspect that it is, as it uses similar ideas,
but I don't have a proof.

Also, I've shown that the Grothendieck-Cisinski model structure on
these cubical sets is the standard one. (Probably not a big surprise
to the homotopy theorists, but reassuring nevertheless). However,
again, we don't know that that's the one Thierry uses.

> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.

> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.

[Bas Spitters]

Thierry is clear, I think: he uses the full subcategory.
The presentation is not dissimilar from the one in Jardine (cubical
homotopy) who uses a similar category, but with fewer maps.

The free Cartesian perspective has been pushed by Steve Awodey.
However, he does not use connections and I have not carefully checked
that the connections can also be presented freely. Although other
people may have.

Yes, the work by Brown and Higgings certainly seems related, although
I have been unable to make a precise connection. (We were going
through Brown's book at CMU).

> Could you elaborate upon how your Moore path category is in fact a category internal to cubical sets

It is a category internal to cubical sets because I defined it in the
internal logic/type theory. However, maybe you want me to unfold the
definitions? I have not done this yet, but I expect one would obtain
something similar to the constructions in Docherty's master thesis.

Dochtery, who builds substantially on your work, emphasizes that one
does not need strength. However, in the presence of diagonals and
connections, there does not seem to be a problem to define them, IIRC.

Best,

Bas

[Andrea Vezzosi]

On Fri, Jul 31, 2015 at 10:53 PM, Richard Williamson
<rwilli...@gmail.com> wrote:
> ...

>
> Yes, I understand how to include both diagonals and reversals from the
> 'structural' point of view that I mentioned. I was wondering whether or not
> they were needed for what Thierry is doing, because the category C is
> defined in a certain way in the second note, but only certain arrows are
> explicitly mentioned, and only certain things are included in the syntax in
> the first note. What I was looking for is exactly which arrows is needed,
> because this is important from a structural point of view. But, as you say,
> it seems that there is some freedom according to what one is looking to do
> as to whether to include diagonals, reversal, or neither. Connections seem
> indispensable, though.

Some structure of the category C might be needed implicitly though,
e.g. the rules rely on C(2,-) ~= C(1,-)xC(1,-) as far as I understand,
where 1 and 2 are some finite sets of that cardinality and C(1,-)
being the semantics of "I", is that still the case without diagonals?

This is exploited by the typing rules for Id: the introduction rule
can simply add an extra (i : I) to the context with a cartesian
product, which allows the similarity with lambda expressions.

[Peter LeFanu Lumsdaine]

Neither connections (in the index category) nor the fact C(2,–) ~= C(1,–) x C(1,–) seem to be entirely indispensible.  The first public version of the cubical model (as presented in Bezem/Coquand/Huber [1]) doesn’t have either of these, and gives a model of type theory with 0, 1, Sigma, Pi, and Id (with propositional Id-comp).  They also suggest/sketch there that it should have a universe, possibly univalent, and propositional truncation, but I don’t know how much of that ended up working out.

In this variant, the identity types are not a categorical exponential, but they are right adjoint to a different monoidal structure (generated by Kan-extension from y(I) • y(J) := y(I+J)), so the similarity with lambda-expressions is still not coincidental.

–p.

[1] Bezem, Coquand, Huber 2014, A model of Type Theory in Cubical Sets http://www.cse.chalmers.se/~coquand/mod1.pdf

[Richard Williamson]

Some structure of the category C might be needed implicitly though,

Exactly, this is precisely why I asked the question: I would like to know exactly what 'structures' actually are used. I understand of course Thierry's actual definition of C as a full subcategory of the category of posets. This kind of point of view on cubical sets is really the standard one, used by Grothendieck, Jardine (as Bas suggested), and Cisinski. The more category-theoretic point of view on categories of cubes is something that until recently I was only aware of having used myself, though I am now happy to know that Steve Awodey also, I think completely independently from my work, been working in this way for some time.

If really all the arrows of Thierry's category are needed, then no doubt it can be built in a structural way, but I would prefer to build from the ground up. 

 

e.g. the rules rely on C(2,-) ~= C(1,-)xC(1,-) as far as I understand,
where 1 and 2 are some finite sets of that cardinality and C(1,-)
being the semantics of "I", is that still the case without diagonals?

If C(2,-) corresponds to the 'free standing 2-cube/square', then this does not hold without diagonals. One has to replace the categorical product x with a non-cartesian tensor product. 

 

This is exploited by the typing rules for Id: the introduction rule
can simply add an extra (i : I) to the context with a cartesian
product, which allows the similarity with lambda expressions.

That's a very helpful comment for me, thanks!

[Richard Williamson]

Neither connections (in the index category) nor the fact C(2,–) ~= C(1,–) x C(1,–) seem to be entirely indispensible.  The first public version of the cubical model (as presented in Bezem/Coquand/Huber [1]) doesn’t have either of these, and gives a model of type theory with 0, 1, Sigma, Pi, and Id (with propositional Id-comp).  

Yes, I agree that neither connections nor diagonals are needed for the Bezem-Coquand-Huber paper, but connections seem to be indispensable to more recent work. They correspond to the phi and psi in Thierry's syntax, and are used throughout in the formulation of the 'composition/glueing' rules. And, as I intimated in earlier posts, that connections should appear in this setting is very natural to me, and I would be extremely surprised if one could do without them.

 

In this variant, the identity types are not a categorical exponential, but they are right adjoint to a different monoidal structure (generated by Kan-extension from y(I) • y(J) := y(I+J)), so the similarity with lambda-expressions is still not coincidental

If I understand your notation, this is the standard closed monoidal structure on cubical sets (arising by Day convolution from the monoidal structure on the category of cubes). 

I have argued before that it is inevitable that identity types should be modelled in this way when working with cubical sets. It is absolutely clear (to me at least) that the homotopy theory of cubical sets is to be carried out with respect to the monoidal structure and the cubical interval, and in particular the co-cylinder (thus identity types) will have to be defined in this way in order to be homotopically correct. One of the very nice things with the cubical sets with diagonals approach is that one has the best of both worlds: one can work in a homotopically correct way with the cartesian product, because the latter can be used to construct the category of cubes in this case.

Before the Bezem-Coquand-Huber paper came out, I had a brief discussion with Thierry and another homotopy type theorist about whether a non-cartesian monoidal structure could be of use in modelling type theory. I argued that it could be, for exactly the reason of the previous paragraph that one would have to do so in order to model identity types correctly, whereas the other homotopy type theorist was skeptical when it came to modelling dependent products. The Bezem-Coquand-Huber paper shows that we were both essentially correct: the non-cartesian monoidal structure is used for identity types, but it is also shown that cartesian exponentials can be used for the modelling of dependent products, if one restricts to Kan complexes. The latter restriction is very natural:  the non-cartesian monoidal structure coincides with the cartesian one after fibrant replacement. 

I will write a bit more later, in reply to Bas, about the Bezem-Coquand-Huber paper.

[Andrea Vezzosi]

On Sat, Aug 1, 2015 at 12:40 PM, Peter LeFanu Lumsdaine
<p.l.lu...@gmail.com> wrote:
> Neither connections (in the index category) nor the fact C(2,–) ~= C(1,–) x
> C(1,–) seem to be entirely indispensible. The first public version of the
> cubical model (as presented in Bezem/Coquand/Huber [1]) doesn’t have either
> of these, and gives a model of type theory with 0, 1, Sigma, Pi, and Id
> (with propositional Id-comp). They also suggest/sketch there that it should
> have a universe, possibly univalent, and propositional truncation, but I
> don’t know how much of that ended up working out.

The univalent universe for that model is shown in Simon's lic:

http://www.cse.chalmers.se/~simonhu/misc/lic.pdf

and indeed also paths in A as a "linear" exponential (I -o A), that
structure is only used to describe the model though.

> In this variant, the identity types are not a categorical exponential, but
> they are right adjoint to a different monoidal structure (generated by
> Kan-extension from y(I) • y(J) := y(I+J)), so the similarity with
> lambda-expressions is still not coincidental.

For the cartesian structure we already know what the typing rules look
like though, while e.g. currently there's no standard solution on how
to mix linear and dependent types. There might be a deeper reason for
requiring diagonals but this is at least a great simplification if one
wishes to expose paths as right adjoints in the theory.

[Bas Spitters]

Yes, I am using Moore paths/ nice path objects categories.
As you might remember we chatted a bit about this.
We found some indication that the construction could be equivalent,
but we did not find a conclusive proof either way.

On Sat, Aug 1, 2015 at 4:18 PM, steve awodey <steve...@icloud.com> wrote:

>
>> On Aug 1, 2015, at 5:39 AM, Bas Spitters <b.a.w.s...@gmail.com> wrote:
>>
>> No, I don't think there is. I've been trying to understand it also
>> from that perspective, too. I was glad to build a van den Berg/Garner
>> model on cubical sets, but I am not sure yet whether it is equivalent
>> to Thierry's model.
>> It seems reasonable to suspect that it is, as it uses similar ideas,
>> but I don't have a proof.
>

> Bas, doesn’t your/Dochtery's construction use Moore paths for the Id-type,
> while Thierry et al. use exponentiation by the 1-cube?
> I think this is a real difference.
>
> S

[Steve Awodey]

> On Aug 1, 2015, at 5:39 AM, Bas Spitters <b.a.w.s...@gmail.com> wrote:
>

> No, I don't think there is. I've been trying to understand it also
> from that perspective, too. I was glad to build a van den Berg/Garner
> model on cubical sets, but I am not sure yet whether it is equivalent
> to Thierry's model.
> It seems reasonable to suspect that it is, as it uses similar ideas,
> but I don't have a proof.

Bas, doesn’t your/Dochtery's construction use Moore paths for the Id-type,
while Thierry et al. use exponentiation by the 1-cube?
I think this is a real difference.

S

>

[Ed Morehouse]

Along with others here at CMU, I have also been thinking about
structural presentations of cube categories whose presheaves would
support a computational interpretation of a higher-dimensional type
theory. I'm sure that those who have been thinking about this already
realize, but it's worth stating explicitly, that it's not only the
generators of such a cube category (e.g. connections and reversals) that
are important, but also the relations.

In the recent work of Thierry and others, the proposed cubical theory is
that of some sort of bounded, distributive lattice. For example, in the
note cited earlier by Richard, it is a de Morgan algebra. To support
such a theory, the cube category must already have morphisms at least
parallel to diagonals in order to even state the distributive law: A ∧
(B ∨ C) = (A ∧ B) ∨ (A ∧ C) has a single A on the left, but two on the
right.

There are plausible reasons for wanting a relatively rich cubical theory
along these lines. The theories of Grandis's dioids, the de Morgan
algebras proposed by Thierry, and the Kleene algebras that Bas told us
about during his visit here last winter are all decidable. This would
endow a type theory built on such cube categories with more judgmental
equalities. Toward the other end of the spectrum, one could start with
a relatively simple cube category and rely on the Kan structure for most
of the work, resulting in fewer judgmental equalities. It's not clear
(at least to me) which strategy is ultimately preferable.

While on the subject, I'd like to pose a question about distributivity.
In order for a theory to be "cubical", it seems to me that the
relations should have a plausible geometric/homotopic interpretation
regarding operations on (some notion of) cubes of various dimensions.
For example, the boundary-degeneracy laws can be thought of as stating
that if you take the point, embed it into the interval at one of its
boundaries and then collapse the interval to the point, the result is
the same as having just left the point alone to begin with. The
distributive law should have an analogous interpretation as an
equivalence between two particular maps from the interval to the
(3-dimensional) cube. One of these is easy enough to understand, but
the other one factors through the 4-dimensional cube and is thus more
difficult to think about. Does anybody know of a good
geometric/homotopic justification for accepting this relation in a
candidate theory of cubes?

-Ed

> --
> You received this message because you are subscribed to the Google
> Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to HomotopyTypeThe...@googlegroups.com

> <mailto:HomotopyTypeThe...@googlegroups.com>.

[Ulrik Buchholtz]

On Sat, Aug 1, 2015 at 1:53 PM, Ed Morehouse <emore...@wesleyan.edu> wrote:

While on the subject, I'd like to pose a question about distributivity.  In order for a theory to be "cubical", it seems to me that the relations should have a plausible geometric/homotopic interpretation regarding operations on (some notion of) cubes of various dimensions. For example, the boundary-degeneracy laws can be thought of as stating that if you take the point, embed it into the interval at one of its boundaries and then collapse the interval to the point, the result is the same as having just left the point alone to begin with.  The distributive law should have an analogous interpretation as an equivalence between two particular maps from the interval to the (3-dimensional) cube.  One of these is easy enough to understand, but the other one factors through the 4-dimensional cube and is thus more difficult to think about.  Does anybody know of a good geometric/homotopic justification for accepting this relation in a candidate theory of cubes?

Doesn't this follow from the fact that the equational theory of the topological interval with the operations from the distributive algebra signature is exactly the theory of Kleene algebras, combined with the trivial observation that these operations are continuous? Or perhaps I'm misunderstanding the question?

Cheers,

Ulrik

[Richard Williamson]

I was glad to build a van den Berg/Garner model on cubical sets, but I am not sure yet whether it is equivalent to Thierry's model. It seems reasonable to suspect that it is, as it uses similar ideas, but I don't have a proof.

One of the main aspects of Bezem-Coquand-Huber's work is the modelling of dependent products. They need to restrict to Kan complexes to carry this out. A first question with regard to extending your model/the model of Simon Docherty to a full model of Martin-Löf type theory would be: is your Moore co-cylinder of a Kan complex also a Kan complex? Have you thought about this?

 

A second question, the obvious one, is whether the Moore co-cylinder that you construct is weakly homotopy equivalent to the usual one (with respect to the non-cartesian monoidal structure). Now it is true for topological spaces that the Moore co-cylinder is homotopy equivalent to the usual one, and there is a lot that one can do with that observation: it is useful, for instance, for establishing the Strøm model structure on topological spaces. I would be surprised if it were the case for your Moore co-cylinder, or the simplicial one, but I have not thought about it in depth.

Of course, it might be possible to extend your model to a full model of Martin-Löf type theory even if it does not agree with the model of Bezem-Coquand-Huber. But then one has to figure out in particular how to model dependent products, and the difficulty of this should not be underestimated!

 However, again, we don't know that that's the [model structure which] Thierry uses. 

Is it at all clear that there is a model structure corresponding to the Bezem-Coquand-Huber model?

Where I wrote in my original post that I believe to be able to do something similar to the Bezem-Coquand-Huber paper, but in a different and more general way, it is this kind of thing that I was referring to (using model structures, etc). I can give a flavour of what I have in mind.

Begin with cubical sets with connections and diagonals (for simplicity). Localise (monoidally) this category at the morphism (arbitrary choice of letters!)

A -> B,

where A is obtained by glueing (i.e. take a pushout involving) two copies of the cubical interval together at the end of one and the beginning of the other, and B is obtained by glueing three copies of the cubical interval together to obtain a triangle. 

Localise it monoidally also at the morphism

C ---> D,

where C is the cubical interval, and D is the cubical interval with a 1-cube going the other way. 

By 'localise' here, I mean in the ordinary (monoidal) categorical sense, not in the sense of Bousfield localisation (I am not working with any model structure on cubical sets with connections and diagonals).

The point of these localisations is that the localised category has an interval that has an 'involution' structure (although involutions/reversals could have been thrown in to begin with) and, crucially, also a 'subdivision' structure (there is no way to obtain this when working simply with a presheaf category). Moreover, this subdivision structure should have 'strictness of identities' in the sense of my thesis, and one can I think ensure that the rest of the 'structures' on an interval needed for the methods of my thesis are straightforwardly built in.

I think that (there are various results in category theory which imply that) this localised category is in addition locally cartesian closed. 

The methods of my thesis (with respect to this interval and the cartesian monoidal structure) then give immediately a model structure on this localised category with extremely strong properties. Every object is fibrant and cofibrant, and the factorisation axioms are as strong as those in the work of van den Berg and Garner, i.e., can be used to model identity types. 

Since we have diagonals, the cartesian monoidal structure is also the correct one homotopically. One should be able to do it in a non-cartesian setting, but one then has to check that the closed monoidal structure descends to the localised category.

Whilst I would need to check some things, I am confident that dependent products and sums work out correctly with this model structure.

The question is to what extent this model of type theory is an interesting one. My feeling would be that one is not killing off much homotopical information: one is making cubical sets a little bit closer to being infinity-groupoids, but there are no kind of truncations, etc. Thus I suspect that it would be interesting. But I have not thought about it in much depth.

This is a bit off the cuff and does not explain the way in which I think to be able to construct Bezem-Coquand-Huber-type models in a general setting, but it serves to illustrate one aspect that I think is important: because of the way in which identity types should be modelled, one should I think be looking for interesting 'Hurewicz-type' model structures. My thesis gives a general way to construct these given a structured, exponentiable interval, so one should, I think be looking for interesting structured, exponentiable intervals. In the setting of presheaf models of homotopy types, this is intimately related to the homotopy hypothesis (constructing algebraic models of weak higher groupoids), so it is not an easy quest, but maybe it at least suggests an approach.

One might also be able to use the kind of model structure that I describe here to construct one on cubical sets themselves, but that is a different story.

 

[Richard Williamson]

The free Cartesian perspective has been pushed by Steve Awodey.
However, he does not use connections and I have not carefully checked
that the connections can also be presented freely. Although other
people may have.

There are two ways that I am aware of to build up variants of categories with cubes with connections in a canonical way.

For both, one begins with a category with three objects, I^0, I^1, and I^2, and arrows between them corresponding to faces, degeneracies, and connections, with appropriate relations. 

 

One then can either:

1) First take the free strict monoidal/free Cartesian category on this category such that I^0 becomes the unit of the monoidal structure. Note the latter condition: taking just the free strict monoidal/free Cartesian category gives the wrong unit. One can take the bare free strict monoidal/free Cartesian category, but then one has to take a 'monoidal/Cartesian quotient' afterwards which identifies the unit with I^0. 

Second, take a 'monoidal/Cartesian quotient' which identifies the tensor product/cartesian product of I^1 with itself with I^2.

2) Define what I call a 'monoidal/Cartesian datum' on this category, and take the 'free strict monoidal/Cartesian category' on this 'monoidal/Cartesian datum' such that I^0 becomes the unit. As far as I know, the notion of a 'monoidal/Cartesian datum' and the 'free strict monoidal/Cartesian category' on it are not in the literature (though they are straightforward), but they are very useful for several things. I wrote a little about it here, although I have since changed things to work purely in the category of categories (without making use of directed graphs). The current definition can be found in the thesis of a master student of mine, Marte Lovise Nilsen, which is available on request (and will eventually be made public), but is about knots/braids and 2-knots/2-braids, so maybe not of so much interest to most of you! But maybe what I wrote at the link is enough to give the idea.

> Could you elaborate upon how your Moore path category is in fact a category internal to cubical sets

It is a category internal to cubical sets because I defined it in the
internal logic/type theory. However, maybe you want me to unfold the
definitions? I have not done this yet, but I expect one would obtain
something similar to the constructions in Docherty's master thesis.

Actually, I was just asking for more details about how you write down your internal definition. The idea is clearly correct, and it would be very nice if one can just say in one line internally that one is working with 'lists of paths', so I'm wondering if you've come up with some nice way of expressing that, that I haven't come across before.

 

Dochtery, who builds substantially on your work, emphasizes that one
does not need strength. However, in the presence of diagonals and
connections, there does not seem to be a problem to define them, IIRC.

What I was referring to is I think more of a radical difference. The only thing that one needs to carry out the work of van den Berg and Garner are a co-cylinder with a 'contraction structure', a 'subdivision structure', and 'connections', such that these are compatible. In other words, if one has connections, then Axiom 2, Axiom 3, and some of Axiom 1 (as van den Berg and Garner remark) are not needed. 

As far as I can see from Simon Docherty's thesis, his Moore co-cylinder does have connections. What I was suggesting was that it would be more natural and conceptually simpler to make use of this, rather than using Axiom 2 and Axiom 3, etc, of van den Berg and Garner. 

[Richard Williamson]

Thank you for the helpful contribution, Martin!

I just wanted to mention that I am probably not a 'classical mathematician' in the sense you had in mind! I would be happy to describe myself as a 'committed constructivist', and all of my work for a long time has been within constructive mathematics. I am also in general entirely happy with syntactical presentations such as that of Thierry. So my questions are specific to trying to understand aspects of Thierry's syntax and semantics partly for their own sake, and partly because I think there might be some ideas introduced that could be of wider significance.

I am very interested in finding constructively acceptable ways to work with cubical sets, abstract homotopy theory, etc. This necessitates quite radical departures from the traditional theory. A more 'syntactical' approach à la Thierry is a very interesting new direction that ties in with some things I am working on myself, so it would be great to understand more of the details.

[Bas Spitters]

Paige North claims that one obtains Pi-types for this model from the
construction of the path object category and Pi-types in the topos. I
have not seen the details yet, but I trust her statement.

It is not clear that BCH comes from a model structure, so it would be
interesting to see whether your proposal below works out. Emily Riehl
has shown BCH fits in the framework of awfs. I am trying to understand
how this can be applied to the new model.

It's nice to see that things seem to fit.

[Bas Spitters]

Thanks. That seems like a nice way of phrasing the universal property.

Regarding the "lists of paths", it's a free category. In this way is
it also easy to unfold the internal definitions.

I do not see immediately how to obtain the subdivision from the
interval (generic free DM-algebra), but I may well be overlooking
something.

Best,

Bas

[Richard Williamson]

Thank you for the interesting comments, Bas!

Paige North claims that one obtains Pi-types for this model from the
construction of the path object category and Pi-types in the topos. I
have not seen the details yet, but I trust her statement.

I have been working on a similar kind of result (but almost certainly using different techniques), so this is plausible to me too. Maybe I can elaborate a little to say that the techniques that I mentioned earlier in this thread as relevant from my thesis/the work of van den Berg and Garner immediately give a weak factorisation system à la the Hurewicz model structure on Top, if one has a sufficiently nice Moore co-cylinder. As far as I can see from Paige's webpage, she extends the work of Barthel and Riehl on factorisations coming from a Moore co-cylinder to do the same thing. The techniques of Tobias and Emily are of quite a different flavour to the techniques I refer to from my thesis, so the two approaches should be complementary.

 

It is not clear that BCH comes from a model structure, so it would be
interesting to see whether your proposal below works out. Emily Riehl
has shown BCH fits in the framework of awfs. 

Presumably the 'fibrations' are Kan fibrations in the sense of Bezem-Coquand-Huber? What are the 'trivial cofibrations'? Possibly unjustly, as I haven't seen anything of Emily's argument, I would be somewhat sceptical that it is constructively valid, which after all is one of important aspects of Bezem-Coquand-Huber.

Maybe I can also say that I myself do not really regard working with a constructively better notion of Kan complex/Kan fibration, such as that of Bezem-Coquand-Huber (there are other possibilities too), as making it harder to find a model structure. The hard thing is to equip cubical sets with any model structure at all in a constructively valid way. This will inevitably necessitate re-working Kan fibrations, etc, in such a way as to ensure that they are better from a constructive point of view.

[Richard Williamson]

Regarding the "lists of paths", it's a free category. In this way is
it also easy to unfold the internal definitions.

There are more details that I would need to see to be convinced by your approach, but I'll take your word for it for now! Please let me know if you write up more details at some point, as I would be very keen to see them.

 

I do not see immediately how to obtain the subdivision from the
interval (generic free DM-algebra), but I may well be overlooking
something.

By a subdivision structure, I meant in the sense of III.11 and III.12 here. The ordinary interval in cubical sets does not have a subdivision structure; this why I carry out one of the two localisations in the way I suggested to obtain a cubical model of type theory earlier in the thread. What I mean is that the Moore co-cylinder that you and Simon Docherty are working with has a subdivision structure (indeed a very nice one, with good strictness properties): this is of course one of the main points of it (just concatenate the paths), corresponding to composition when thinking of it as an internal category. 

[Bas Spitters]

Here's the construction by Emily. I seem to recall that it is constructive.
http://www.math.harvard.edu/~eriehl/made-to-order.pdf

[Richard Williamson]

 I'm sure that those who have been thinking about this already
realize, but it's worth stating explicitly, that it's not only the
generators of such a cube category (e.g. connections and reversals) that
are important, but also the relations.

Yes, indeed. There are some relations that have to be there for any purpose, and some which I usually refer to as 'compatibilities' between the various structures,. These say things like: the connection of a degeneracy is a degeneracy, etc.

  In order for a theory to be "cubical", it seems to me that the
relations should have a plausible geometric/homotopic interpretation
regarding operations on (some notion of) cubes of various dimensions.

Certainly, if one's cubical category does not admit a geometric realisation functor to Top, it is rather questionable that it bears much relationship to homotopy theory as usually understood when one speaks of 'homotopy type theory'!! (Of course, there could still be model structures, etc, so homotopy theory in a more abstract sense.)

 

Thank you for the interesting comments!

[Andrew Swan]

I also have a proof that there is an awfs corresponding to the BCH model (in fact 01-substitution sets which are equivalent), which is on the arxiv at http://arxiv.org/abs/1409.1829. I was fairly careful to write out the details explicitly so I'm confident it does work constructively.

More recently I've been looking at another awfs on 01-substitution sets that I expect to form the (cofibration)-(acyclic fibration) part of an algebraic model structure, so in particular I expect it's possible to prove constructively that there's a model structure on cubical sets along these lines.

[Richard Williamson]

Thank you for the link to your paper, Andrew! I had seen it before, but had forgotten about it! It certainly addresses directly some of the things that I expected to be problematic constructively. I would, naturally, have to work more closely through your paper to check whether I fully agree with you.

Perhaps it is in your paper, but could you say explicitly what the left class of morphisms ('trivial cofibrations') are, as I asked Bas earlier? One reason that I am keen to know is that it is a good way to see whether the argument is likely to be constructively valid. Typically, in my experience, when working constructively, one should be working with 'structured cofibrations' of some kind: one usually needs a non-constructive argument to characterise these as, say, monomorphisms. To get a constructively valid model structure on Cat for instance, one should not be working with functors that are injective on objects, but with a notion of iso-cofibration that is dual to the notion of iso-fibration.

With regard to your second paragraph, I would just caution that constructing one half of a model structure, or even the two halves separately, is much, much easier than establishing a full model structure, which requires a delicate balance between the two halves. But probably you know that from experience already!

[Andrew Swan]

Perhaps it is in your paper, but could you say explicitly what the left class of morphisms ('trivial cofibrations') are, as I asked Bas earlier?

In any awfs the left maps are coalgebras over a comonad given by the functorial factorisation. So a trivial cofibration is a map f:X -> Y together with a coalgebra map c:Y -> K f. Unfolding the definition for this particular awfs we get the following. c assigns to each element of the codomain an element of the set inductively generated by X and Kan filling and composition operations over Y. Roughly speaking, every element of Y is assigned an explanation how it could have been added by a sequence of Kan filling and composition operations starting with the image of f. Also, if we are given something in the image of f then we have to recognise it as such. In particular the image of every trivial cofibration is decidable (see the proof of theorem 6.4 in the preprint).

 

One reason that I am keen to know is that it is a good way to see whether the argument is likely to be constructively valid. Typically, in my experience, when working constructively, one should be working with 'structured cofibrations' of some kind: one usually needs a non-constructive argument to characterise these as, say, monomorphisms.

 

Yes, I certainly agree. In my (tentative) definition of cofibrations and trivial fibrations, every cofibration has decidable image so cofibration is (in general) strictly stronger than monomorphism. Surprisingly, allowing any monomorphism to be a cofibration is even problematic in classical logic. Using classical logic one can assign a cofibration structure to every monomorphism, but this cannot be done in a functorial way. That is, it's impossible to assign the structures so that every morphism between monomorphisms (ie commutative square with two opposite sides monomorphisms) is a morphism between cofibrations (ie morphism in the coalgebra sense).

[Richard Garner]

Constructively, the cofibrations in simplicial sets should be given by taking the Reedy awfs with respect to the awfs on Set for split epimorphisms---whose left class comprises the coproduct injections.

 

Even when Set happens to be boolean, something non-trivial happens here. The coalgebras are arbitrary monomorphisms, but the coalgebra morphisms are not just commuting squares. In particular, the category of coalgebras for the cofibrant replacement comonad Q is the category of simplicial sets and degeneracy-reflecting maps. It turns out that this category is, in fact, a presheaf category. I wrote up some notes on this a while ago:

 

http://science.mq.edu.au/~rgarner/cofibrant-simplicial-sets.pdf

 

Something else that is quite interesting in the algebraic context is Q(1). It's the free simplicial set in which each n-boundary contains a non-degenerate n-simplex. It gets pretty big pretty quickly; in low dimensions it has:

 

1 0-simplex

2 1-simplices (1 non-degenerate)

11 2-simplices (8 non-degenerate)

264 3-simplices (236 non-degenerate)

58,626 4-simplices (57,629 non-degenerate)

496,557,308 5-simplices (496,266,817 non-degenerate)

 

a sequence on which Sloane's is, unfortunately, silent.

 

Although all the above is about algebraic weak factorisation systems, you can see some trace of this stuff even in the world of ordinary non-algebraic weak factorisation systems when you look at the projective model structure on simplicial presheaves; the cofibrant objects in [C^op, [Delta^op, Set]] are those functors F for which each F(-, n) is projective in [C^op, Set] and each F(f, -): F(c,-) --> F(d,-) reflects degeneracies.

 

Richard

 

[Richard Garner]

Where I wrote in my original post that I believe to be able to do something similar to the Bezem-Coquand-Huber paper, but in a different and more general way, it is this kind of thing that I was referring to (using model structures, etc). I can give a flavour of what I have in mind.

 

Begin with cubical sets with connections and diagonals (for simplicity). Localise (monoidally) this category at the morphism (arbitrary choice of letters!)

 

A -> B,

 

where A is obtained by glueing (i.e. take a pushout involving) two copies of the cubical interval together at the end of one and the beginning of the other, and B is obtained by glueing three copies of the cubical interval together to obtain a triangle. 

 

Localise it monoidally also at the morphism

 

C ---> D,

 

where C is the cubical interval, and D is the cubical interval with a 1-cube going the other way. 

 

By 'localise' here, I mean in the ordinary (monoidal) categorical sense, not in the sense of Bousfield localisation (I am not working with any model structure on cubical sets with connections and diagonals).

 

The point of these localisations is that the localised category has an interval that has an 'involution' structure (although involutions/reversals could have been thrown in to begin with) and, crucially, also a 'subdivision' structure (there is no way to obtain this when working simply with a presheaf category). Moreover, this subdivision structure should have 'strictness of identities' in the sense of my thesis, and one can I think ensure that the rest of the 'structures' on an interval needed for the methods of my thesis are straightforwardly built in.

 

I think that (there are various results in category theory which imply that) this localised category is in addition locally cartesian closed. 

 

 

Certainly it's cartesian closed; that's direct, because the monoidal structure on the cubical site at issue is just coproduct, and so the Day convolution structure is product; when you monoidally localise it, it remains product, and so you have a cartesian closed category without any difficulty. Locally cartesian closed will require more work; the localisation needs to be semi-left-exact in the sense of Cassidy-Hebert-Kelly, and it's not immediately obvious that this is so (I don't know how you can divine semi-left-exactness of a reflection by looking at a generating left class of maps, unless you are in fact using them to generate a Grothendieck topology).

 

Note that if you call the cartesian closed category you construct above E, then to give a complete and cocomplete E-enriched category is to give a category equipped with an adjoint cylinder and cocylinder with subdivision, connections, diagonals, involution, etc.

 

The methods of my thesis (with respect to this interval and the cartesian monoidal structure) then give immediately a model structure on this localised category with extremely strong properties. Every object is fibrant and cofibrant, and the factorisation axioms are as strong as those in the work of van den Berg and Garner, i.e., can be used to model identity types. 

 

Now if given any category C equipped with an adjoint cylinder and cocylinder, there's the model structure constructed from this as in your thesis, but also an E-enrichment coming from the cylinder and co-cylinder. I would think that the model structure structure on C should then be an E-enriched model structure, and in fact the "canonical" model structure obtained by lifting from E.

 

Since we have diagonals, the cartesian monoidal structure is also the correct one homotopically. One should be able to do it in a non-cartesian setting, but one then has to check that the closed monoidal structure descends to the localised category.

 

Well, you have to do that in the cartesian case, too. But that's part of what it means to monoidally localise something: by the Day reflection theorem, the localisation is a monoidal localisation iff the generating left class is closed under tensor with arbitrary objects iff the subcategory is an exponential ideal iff the closed monoidal structure descends.

 

Whilst I would need to check some things, I am confident that dependent products and sums work out correctly with this model structure.

 

This is a bit off the cuff and does not explain the way in which I think to be able to construct Bezem-Coquand-Huber-type models in a general setting, but it serves to illustrate one aspect that I think is important: because of the way in which identity types should be modelled, one should I think be looking for interesting 'Hurewicz-type' model structures.

 

 

I don't know if I'm visualising this right, but my hope is that for the model structure on cubical sets with connections subdivision etc as described above has the property that its (algebraic) trivial fibrations are closed under arbitrary colimits. This is an important property of the Hurewicz model structures on Cat and on chain complexes, and plays a role for things like constructing bar resolutions. I feel like, in general, it ought to be something to do with what is meant by a "Hurewicz-style" model structure.

 

One final comment which is maybe relevant. Above you generate the free monoidal category on a cograph with object of co-objects the monoidal unit equipped with a co-composition and co-reversion and co-diagonals and co-connections.

 

If instead you take the free cocomplete monoidal category on a co-category object with object of co-objects the monoidal unit, I think you get the category of edge-symmetric cubical omega-categories, with monoidal product the lax Gray tensor product. If you augment the generating data so as to involve a "Hopf cocategory" (i.e., by requiring a suitable monoid structure on the object of co-morphisms) then the resultant category is the category of edge-symmetric cubical omega-categories with connections --- and these are equivalent to globular omega-categories --- again with the lax Gray tensor product.

 

I don't know what use this is but I find it quite illuminating.

 

Richard

 

[Richard Williamson]

 I just wanted to say thank you very much for this, Richard, I greatly appreciate the time you have taken to think about the construction I suggested. Your interest motivates me to work on it further.

For now, the only thing I'll comment briefly upon is that, upon thinking a little more carefully, in the light of your comment, I would not be at all surprised if the localised category is not locally cartesian closed. A better guess would be that, as with the folk model structure on Cat, the fibrations are exponentiable, which is of course what we actually need for modelling type theory. In fact I think that this should be true for any model structure produced by the methods of my thesis, and I think I know how a proof of this should go (it is the result that I mentioned to Bas earlier in the thread that I had been working on), but I need to write it down carefully. 

Unfortunately I do not have time just now to respond to the rest of your thoughts, which interest me a lot, or to respond to Andrew's interesting last comment, but I will get back to you both once time permits.

[Thierry Coquand]

Thanks for your questions. I now have updated the second note  you are referring to.

One goal is present all required definitions in details, so that they can be formalized

and comments are very welcome.

I also added the proof of a key Lemma which shows how to reduce filling operations

to composition operations.  One should analyze this proof to see what are the abstract properties

needed for C (but it is clear that connections are crucial there). 

To use composition and connection is reminiscent of the work of Brown and Higgins, but, 

as mentioned already by Bas, they describe -strict- w-groupoid.

 The need of a diagonal operation appeared when implementing the elimination rule for

the circle in the first version of the cubical set model. They seem necessary in order to get

the desired computational equalities. 

 The use of the "reversal" operation is not essential and not used in this note.

  In any case, the same treatment should apply to simplicial sets as well (where we don't have a "reversal"

operation).

 The univalence axiom and the fact that the universe is fibrant are both reduced to one operation

which is called glueing (and the main objective of the note is to present this operation).

The fact that one can prove (internally) univalence from this operation has

been discovered by Anders and Simon, (I thought before that another operation would be needed)

and the proof is formalized in the file examples/univalence.ctt

On Jul 31, 2015, at 1:48 PM, Richard Williamson wrote:

I would like to understand the details of cubical type theory, but am having some difficulty in getting started! Would somebody be able to, say, 'walk through' this note of Thierry's? This note is the other one that I'm particularly interested in.

My background is that I have worked a lot on cubical sets, and I am also thoroughly acquainted with Martin-Löf type theory, with Coq, Haskell, etc. But my work on cubical sets has a somewhat different, more category-theoretic flavour to that used in Thierry's notes and all other work that I have seen on cubical type theory. I would like to try to understand things from the point of view I usually work with, and it is getting started with making this translation that I am having some difficulty with. 

I can understand the original work of Bezem, Coquand, and Huber from the point of view that I usually work in (and, excluding univalence, which I haven't thought about in this setting, believe to be able to do the same kind of thing in a different and more general way). But with the more heavy emphasis on nominal sets, etc, in more recent work, it is harder for me to get a feeling for things.

To be more concrete, I can begin with the second note that I linked to above. I would like to understand the category C that Thierry defines in the section 'Base (pre)category' in a way more familiar to me. I would like to define C 'structurally', that is to say as a 'free strict monoidal category'-like construction on a category Base with, say, three objects I^0, I^1, and I^2, and various arrows between. The only operations named by Thierry are connections and face maps. We can certainly define a category Base which encodes connections and face maps, and define C universally from Base (it is not simply the free strict monoidal category on Base, but I know how to define the relevant universal property). A presheaf on C would then be what I would call a 'semi-cubical set with connections'. My question is: are connections and face maps the only things that are important in Thierry's category C? In the first note that I linked to (the first section 'Interval'), it would seem that 'involutions' (aka 'reversals') should be built in as well? I have also seen some talk of including 'diagonals', but these do not seem to be explicitly used in either note?

My next questions regarding the second note is to do with the 'composition structure'. I wonder if this is related to work of Brown and Higgins on 'commutative n-cubes' in strict cubical infinity-groupoids, and to be able to see whether or not that is the case, it would be very helpful to understand visually what is going on in Thierry's note in low dimensions. What do the possible 'open boxes' used in Thierry's note to define fibrant cubical sets look like for 1-cubes, 2-cubes, and 3-cubes? It seems that they are more general than just 'horns'?

Finally, to get started with understanding the first note linked to above: could someone be so kind as to spell out the semantics of the 'basic typing rules' (being as geometric and low-dimensional as possible!)?

[Richard Williamson]

Thank you for the update, Thierry. I will try to explain the kind
of result that I think you may be proving in the lemma that you
mention, and maybe you or another could let me know whether or
not this is the case. I have not actually worked through the
details of your approach, just read over it and attempted to
re-construct the geometric intuition behind it/translate it into
terms more familiar to me.

Let us begin with what we might call a cubical ∞-magma: it has an
underlying cubical set; and we can compose n-cubes in n different
directions. What I claim is that, with reversals, compositions,
and strict identities, we can fill in horns in the underlying
cubical set.

Let us see how this works for filling in a 2-horn. Suppose we
have the following.

f_0
x_0 -----> x_1
| |
f_2 | | f_1
↓ ↓
x_2 x_3

We can fill in the 'missing face' by the arrow


f_1 ∘ f_0 ∘ v(f_2)
x_2 ----------------------> x_3,

where v(f_2) denotes the reversal of f_2. Actually, since I am
not asssuming associativity, we need to choose a bracketing. I'll
denote this arrow by g for short.

We can then fill in the square

f_0
x_0 -----> x_1
| |
f_2 | | f_1
↓ ↓
x_2 -----> x_3
f_3

by composing together (in one of the several possible ways, it
doesn't matter which, which are compatible with the bracketing we
chose for

f_1 ∘ f_0 ∘ v(f_2)

above) the following 2-cubes.

id f_0 id
-------> --------> ------->
| | | |
| | | |
f_2 | | id | id | f_1
| | | |
↓ ↓ ↓ ↓
--------> -------> ------>
| v(f_2) | f_0 | f_1 |
| | | |
id | id | id | | id
| | | |
↓ ↓ ↓ ↓
-------> -------> ----->
v(f_2) f_0 f_1

All these 2-cubes are either connections or degeneracies: there
is only one possible choice in each case.

It would take a little ingenuity to figure out how to write down
a similar argument in higher dimensions, but I am certain that it
is possible.

What I think that you may be doing, Thierry, is that you take as
an axiom that missing faces in horns can be filled in (or rather
a generalisation of this), and then perhaps do something a little
akin to what I have done above to fill in the 'inside' of the
horns (or generalisations). Could you possibly comment on this?
In particular, would it be possible to give a geometric
explanation of how you fill in the inside, similar to what I did
above?

Note that there is no strictness assumption, except for
strictness of identities, in what I did above: no associativity,
no interchange axioms, no strict inverses, no compatibilities
between the connections ('transport axioms'), etc. As I have
already mentioned, I am entirely aware that Brown and Higgins
work with strict ∞-groupoids, but, as I have tried to explain,
feel that their techniques are not restricted to this setting.

What I did above can (of course) be thought of as part of a proof
that the nerve of a cubical ∞-groupoid (in whatever sense, as
long as it has an underlying cubical ∞-magma as above) is a
cubical Kan complex.

Best wishes,
Richard

On Tue, Aug 11, 2015 at 08:16:34PM +0000, Thierry Coquand wrote:
>
> Thanks for your questions. I now have updated the second note<http://www.cse.chalmers.se/~coquand/vv.pdf> you are referring to.

> One goal is present all required definitions in details, so that they can be formalized
> and comments are very welcome.
> I also added the proof of a key Lemma which shows how to reduce filling operations
> to composition operations. One should analyze this proof to see what are the abstract properties
> needed for C (but it is clear that connections are crucial there).
> To use composition and connection is reminiscent of the work of Brown and Higgins, but,
> as mentioned already by Bas, they describe -strict- w-groupoid.
>
> The need of a diagonal operation appeared when implementing the elimination rule for
> the circle in the first version of the cubical set model. They seem necessary in order to get
> the desired computational equalities.
> The use of the "reversal" operation is not essential and not used in this note.
> In any case, the same treatment should apply to simplicial sets as well (where we don't have a "reversal"
> operation).
>
> The univalence axiom and the fact that the universe is fibrant are both reduced to one operation
> which is called glueing (and the main objective of the note is to present this operation).
> The fact that one can prove (internally) univalence from this operation has
> been discovered by Anders and Simon, (I thought before that another operation would be needed)
> and the proof is formalized in the file examples/univalence.ctt
>
>
> On Jul 31, 2015, at 1:48 PM, Richard Williamson wrote:
>

> I would like to understand the details of cubical type theory, but am having some difficulty in getting started! Would somebody be able to, say, 'walk through' this note<http://www.cse.chalmers.se/~coquand/rules7.pdf> of Thierry's? This note<http://www.cse.chalmers.se/~coquand/vv.pdf> is the other one that I'm particularly interested in.

>
> My background is that I have worked a lot on cubical sets, and I am also thoroughly acquainted with Martin-Löf type theory, with Coq, Haskell, etc. But my work on cubical sets has a somewhat different, more category-theoretic flavour to that used in Thierry's notes and all other work that I have seen on cubical type theory. I would like to try to understand things from the point of view I usually work with, and it is getting started with making this translation that I am having some difficulty with.
>
> I can understand the original work of Bezem, Coquand, and Huber from the point of view that I usually work in (and, excluding univalence, which I haven't thought about in this setting, believe to be able to do the same kind of thing in a different and more general way). But with the more heavy emphasis on nominal sets, etc, in more recent work, it is harder for me to get a feeling for things.
>
> To be more concrete, I can begin with the second note that I linked to above. I would like to understand the category C that Thierry defines in the section 'Base (pre)category' in a way more familiar to me. I would like to define C 'structurally', that is to say as a 'free strict monoidal category'-like construction on a category Base with, say, three objects I^0, I^1, and I^2, and various arrows between. The only operations named by Thierry are connections and face maps. We can certainly define a category Base which encodes connections and face maps, and define C universally from Base (it is not simply the free strict monoidal category on Base, but I know how to define the relevant universal property). A presheaf on C would then be what I would call a 'semi-cubical set with connections'. My question is: are connections and face maps the only things that are important in Thierry's category C? In the first note that I linked to (the first section 'Interval'), it would seem that 'involutions' (aka 'reversals') should be built in as well? I have also seen some talk of including 'diagonals', but these do not seem to be explicitly used in either note?
>
> My next questions regarding the second note is to do with the 'composition structure'. I wonder if this is related to work of Brown and Higgins on 'commutative n-cubes' in strict cubical infinity-groupoids, and to be able to see whether or not that is the case, it would be very helpful to understand visually what is going on in Thierry's note in low dimensions. What do the possible 'open boxes' used in Thierry's note to define fibrant cubical sets look like for 1-cubes, 2-cubes, and 3-cubes? It seems that they are more general than just 'horns'?
>
> Finally, to get started with understanding the first note linked to above: could someone be so kind as to spell out the semantics of the 'basic typing rules' (being as geometric and low-dimensional as possible!)?
>
> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.

> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com<mailto:HomotopyTypeThe...@googlegroups.com>.

[Thierry Coquand]

Thanks for your explanations.

> What I think that you may be doing, Thierry, is that you take as
> an axiom that missing faces in horns can be filled in (or rather
> a generalisation of this), and then perhaps do something a little
> akin to what I have done above to fill in the 'inside' of the
> horns (or generalisations). Could you possibly comment on this?
> In particular, would it be possible to give a geometric
> explanation of how you fill in the inside, similar to what I did
> above?

I will try to draw some pictures corresponding to the case you
presented. (This corresponds to the proof of reduction of filling to composition in the note.)
For interpreting in a constructive way dependent function types,
we introduced a generalization of "Kan composition".
For a square, the "usual" Kan composition can be seen as forming
a square from 5 given squares, something like

b1 --------------------------------- d1
|\ / |
| \ / |
| \ / |
| b--------------------------d |
| | | |
| a--------------------------c |
| / \ |
| / \ |
|/ \ |
a1-----------------------------------c1

which builtds the square a1b1c1d1 from the 5 squares abcd,
aba1b1, aca1ca, bdb1d1, cdc1d1

(This is different from yours and Ronnie Brown composition, which is more natural
geometrically.)

The generalization was to have compositions like


b1 --------------------------------- d1
\ /
\ /
\ /
b--------------------------d
| |
a--------------------------c
/ \
/ \
/ \
a1-----------------------------------c1

where we build a1b1c1d1 from only 3 squares abcd, aca1c1, bdb1d1
together with an uniformity condition: the line a1b1 should be the composition
of ab, aa1, bb1 and the line c1d1 the composition of cd, dd1, cc1

and we even allow composition like


b1 --------------------------------- d1
|\ /
| \ /
| \ /
| b--------------------------d
| | |
| a--------------------------c
| / \
| / \
|/ \
a1-----------------------------------c1

where we build the square a1b1c1d1 from 4 squares.
(In this case, the uniformity condition states that the line c1d1 in the resulting square
is the composition of the lines cd, cc1, dd1).

Using connections and this composition, we can now describe the filling of



b----------d
|
|
a --------- c

as the composition

b --------------------------------- d
|\ /
| \ /
| \ /
| b--------------------------b
| | |
| a--------------------------a
| / \
| / \
|/ \
a -----------------------------------c

which builds the square abcd from the 4 squares are abab, aaac, abab, bbbd

Uniformity in this case gives us that the line cd in this square is the composition of
ab, ac, bd


Like what you describe, there is no strictness assumption, but we don't even
have strictness of identities (we tried to impose strictness of identities which would
reduce the previous composition to only 3 squares, but there was then a problem
in the composition of the universe).

Best regards,
Thierry

[Richard Williamson]

Thank you very much, Thierry, for taking the time to explain
this. It is extremely helpful. I understand now your
construction, and have a few comments.

> For a square, the "usual" Kan composition can be seen as forming
> a square from 5 given squares, something like
>
> b1 --------------------------------- d1
> |\ / |
> | \ / |
> | \ / |
> | b--------------------------d |
> | | | |
> | a--------------------------c |
> | / \ |
> | / \ |
> |/ \ |
> a1-----------------------------------c1
>
> which builtds the square a1b1c1d1 from the 5 squares abcd,
> aba1b1, aca1ca, bdb1d1, cdc1d1
>
> (This is different from yours and Ronnie Brown composition,
> which is more natural geometrically.)

Actually, I do not think that there is any difference. If one
begins with a cubical n-groupoid, or cubical n-magma in the sense
I described, where n can be ∞, one can associate to it a 'nerve',
which is a cubical Kan complex. Showing that this nerve is indeed
a cubical Kan complex involves, for 3-horns, demonstrating that,
when we have five 2-cubes in the cubical ∞-magma arranged as you
describe, we can fill in the back face, and then fill in the
inside, to obtain a 3-cube.

Using connections, reversals, and strictness of identities, one
can do this. The work of Brown and Higgins on commutative n-cubes
that I mentioned in an earlier message in this thread concerns
exactly this. They figure out a way to do it in all dimensions.

> Using connections and this composition, we can now describe
> the filling of
>
>
>
> b----------d
> |
> |
> a --------- c
>
> as the composition
>
> b --------------------------------- d
> |\ /
> | \ /
> | \ /
> | b--------------------------b
> | | |
> | a--------------------------a
> | / \
> | / \
> |/ \
> a -----------------------------------c
>
> which builds the square abcd from the 4 squares are abab, aaac, abab, bbbd
>
> Uniformity in this case gives us that the line cd in this square is the composition of
> ab, ac, bd

Again, for the purpose of comparison, such a filling can be
constructed in exactly this way for cubical Kan complexes coming
from cubical ∞-groupoids or ∞-magmas, and will agree with the
construction that I gave in my previous email.

I guess that you do not require that the back 2-cube and right
2-cube which are 'filled in' by your composition operation are
the same? This holds for the nerve of a cubical
∞-groupoid/cubical ∞-magma, so this would be one way in which a
cubical Kan complex in the sense you describe would be more
general than nerves of cubical ∞-groupoids/∞-magmas.

I find these conditions very natural. One will be able to fill in
these generalised horns in the nerve of a cubical
∞-groupoid/cubical ∞-magma, and the uniformity condition will
hold.

In summary, the structure that you and collaborators require of a
fibrant cubical set is one with which the nerve of a cubical
∞-groupoid/magma will be able to equipped. This will be the case
also for fully strict ∞-groupoids. Thus I feel that we have an
answer to one of my original questions, regarding the
relationship of your notion of composition to the work of Brown
and Higgins: the structure being axiomatised is one with which
the nerve of a cubical ∞-groupoid/∞-groupoid (in any degree of
weakness or strictness, as long as it has strictness of
identities) can be equipped, and demonstrating this is the kind
of thing that the work of Brown and Higgins can be used for.

If I am correct in what I have written above, then a consequence
of your work, if I understand corrrectly, is that univalence will
be able to be demonstrated for models of type theory built upon
flavours of cubical ∞-groupoid which are quotients of the notion
of cubical ∞-magma that I described.

It is quite easy to construct model structures on categories of
these kinds of cubical ∞-groupoids. These can be described as a
category of algebras for a monad on cubical sets. It follows
immediately, if I am not overlooking something, from work of
Anders Kock that one 'transfer' the closed monoidal structure on
cubical sets 'across' this monad, to obtain a closed monoidal
structure on cubical ∞-groupoids. In addition, one has an
interval with all the properties needed for my thesis (at least
under some minor additional requirements on the cubical
∞-groupoids). So we obtain a Hurewicz-type model structure, in
which every object is both fibrant and cofibrant. I claim also
that fibrations will be exponentiable, an argument for which I
can outline if anybody is interested. So we will have a model of
type theory, as claimed.

Having come this far, I might mention that I think it possible to
demonstrate that some these cubical ∞-groupoids satisfy the
homotopy hypothesis, in an extremely strong sense.

1) The model structure will be Quillen equivalent to the standard
model structure on cubical sets (this is the main part of the
claim).

2) The model structure is 'algebraic' in the sense that every
object is fibrant and cofibrant, so that one can work 'on the
nose' in a homotopically correct way with objects, without having
to make fibrant and cofibrant replacements.

3) The category of cubical ∞-groupoids itself is algebraic: it is
locally presentable (and if one truncates to n-groupoids, is
locally finitely presentable); it is the category of algebras for
a monad.

4) In the fully strict case, one can recovers a category which is
equivalent to the category of strict globular ∞-groupoids.

This is the kind of thing I have been working on for a long time,
and have understood in principle how to carry out the proof for a
long time too; but have not written it up because I would like to
carry out in a foundations which satisfy extremely strong
philosophical requirements. I am happy to discuss a proof with
anyone interested.

There is a piece of folklore wisdom which says that it should not
be possible to find model structures on higher categories in
which all objects are cofibrant. It is based on the fact that the
model structures that have been exhibited on 2-categories, etc,
(by Lack, etc), do not have all objects cofibrant. But these are
'Serre-like' model structures; it is, I am pretty certain, also
possible to construct 'Hurewicz-like' model structures on
2-categories, etc, and the model structure I work with above is
of this kind. In other words, I am not convinced that this piece
of folklore wisdom actually holds true.

Best wishes, Richard

[Thierry Coquand]

 Hello,

 I have updated this note on the presentation of a cubical type theory

with hopefully a more complete presentation of the operational semantics.

I also included a description in this framework of Andrew's Swan idea

of how to obtain an identity type with good computational property

from the path type (by a factorization argument, valid constructively).

 Best regards,

 Thierry

 PS: The main idea underlying this presentation is the following. In any presheaf

model we can associate to a presheaf A another presheaf Partial(A) of partial

elements of A. In general an element of Partial(A)(I), if I is an object of the

category, is given by a sieve on I and an element defined on this sieve

(a compatible family of elements indexed by element of the sieve).

We can say that such a partial element is "connected" if it is the restriction of

a total element. We consider only in this model partial elements where

the sieve is given by a union of faces of I.  To be fibrant is then defined

by the fact that any partial path connected at 0 is also connected at 1.

 This definition applies to types as well (a partial type at level I is given

by a family of sets indexed by element of the sieve with transition functions).

 The glueing operation in the note is then an algorithm proving that to be

connected is preserved by isomorphisms.

[Thierry Coquand]

I have updated further this note with a description of propositional truncation. Two other remarks

 -Andrew Swan's operation for adapting the identity type to one that satisfies the proper judgmental

computation rule is an adaptation of Richard Garner's small object argument for weak factorization 

systems, which defines an object and a map by induction. In this setting, the inductive step disappears

and one gets an explicit definition.

 -I introduced an explicit distinction between the interval II, and the lattice of faces, which is the lattice

generated by truth-values i = 0 and i = 1. With this formulation what is needed of the interval is that it

has a max and min operation. Since this is the case for the interval for simplicial  sets, I expect that the

same rules are also validated using simplicial sets.

On Jul 31, 2015, at 1:48 PM, Richard Williamson wrote:

I would like to understand the details of cubical type theory, but am having some difficulty in getting started! Would somebody be able to, say, 'walk through' this note of Thierry's? This note is the other one that I'm particularly interested in.

My background is that I have worked a lot on cubical sets, and I am also thoroughly acquainted with Martin-Löf type theory, with Coq, Haskell, etc. But my work on cubical sets has a somewhat different, more category-theoretic flavour to that used in Thierry's notes and all other work that I have seen on cubical type theory. I would like to try to understand things from the point of view I usually work with, and it is getting started with making this translation that I am having some difficulty with. 

I can understand the original work of Bezem, Coquand, and Huber from the point of view that I usually work in (and, excluding univalence, which I haven't thought about in this setting, believe to be able to do the same kind of thing in a different and more general way). But with the more heavy emphasis on nominal sets, etc, in more recent work, it is harder for me to get a feeling for things.

To be more concrete, I can begin with the second note that I linked to above. I would like to understand the category C that Thierry defines in the section 'Base (pre)category' in a way more familiar to me. I would like to define C 'structurally', that is to say as a 'free strict monoidal category'-like construction on a category Base with, say, three objects I^0, I^1, and I^2, and various arrows between. The only operations named by Thierry are connections and face maps. We can certainly define a category Base which encodes connections and face maps, and define C universally from Base (it is not simply the free strict monoidal category on Base, but I know how to define the relevant universal property). A presheaf on C would then be what I would call a 'semi-cubical set with connections'. My question is: are connections and face maps the only things that are important in Thierry's category C? In the first note that I linked to (the first section 'Interval'), it would seem that 'involutions' (aka 'reversals') should be built in as well? I have also seen some talk of including 'diagonals', but these do not seem to be explicitly used in either note?

My next questions regarding the second note is to do with the 'composition structure'. I wonder if this is related to work of Brown and Higgins on 'commutative n-cubes' in strict cubical infinity-groupoids, and to be able to see whether or not that is the case, it would be very helpful to understand visually what is going on in Thierry's note in low dimensions. What do the possible 'open boxes' used in Thierry's note to define fibrant cubical sets look like for 1-cubes, 2-cubes, and 3-cubes? It seems that they are more general than just 'horns'?

Finally, to get started with understanding the first note linked to above: could someone be so kind as to spell out the semantics of the 'basic typing rules' (being as geometric and low-dimensional as possible!)?

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.

To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.

[Alexander Kuklev]

What is known about the universe hierarchy and validity of resizing rules in this model?

Thanks,

Alex

2015-09-01 @ 21:28, Thierry Coquand:

[Thierry Coquand]

On Sep 2, 2015, at 12:42 AM, Alexander Kuklev wrote:

What is known about the universe hierarchy and validity of resizing rules in this model?

Thanks,

Alex

 If we consider the universe U of types with a composition operation built from one given

Grothendieck universe (as described in this note), then we can interpret the judgement

G |- A as a mapping from a cubical set (interpretation of G) to U.

 So for each r in [[ G ]] (I)   we have   [[ A ]] r in U(I), and so  [[ A ]] r is a family of sets (X_f) indexed

by maps f : J -> I of codomain I with transition maps X_f -> X_{fg} for g : K -> J.

  G |- t : A is then interpreted by giving [[ t ]] r   element of the set  X_{id_I}.

 If we start instead from a cumulative sequence of w+1 Grothendieck universes we can in the same

way interpret a cumulative sequence of universes U(n) a la Russell.

 For interpreting the resizing rule that all propositions are in U(0), a new idea is needed (but at least we 

have a way to compute with it and we can conjecture normalization).

 Best,

 Thierry