a cubical type theory

[Thierry Coquand]

 We would like to announce an updated version of our implementation of cubical sets 

which can be found at

 https://github.com/mortberg/cubicaltt

 This is now an implementation of a type theory where the user manipulates directly

points, lines, squares, cubes,… which provide an intuitionistic realization of

homotopy types. Identity type is defined as a type of paths, and all properties

of intensional equality are provable. Besides, function extensionality is also provable, and

we can transform any isomorphism in an equality.  We also have some simple examples of

higher inductive types (e.g. a proof that the circle and the suspension of the type Bool are 

equal, which illustrates further the use of the cubical syntax).

 Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg

[Urs Schreiber]

On 4/13/15, Thierry Coquand <Thierry...@cse.gu.se> wrote in small part:

> we can transform any isomorphism in an equality.

This sounds very promising. Could you give me a little bit of prose as
to what this means regarding the status of making univalence compute?

Once I quizzed somebody who worked on homotopy theoretic proofs in
HoTT whether the cubical type theory would make his proofs easier in
that the univalence terms would finally compute. But he said
(recollecting from my memory) that he wouldn't believe so, since while
the expressions would compute, they would compute to terms in the
ambient type theory in which the cubical complexes are encoded, and
these may not have any obvious meaning in the actual homotopy type
theory, he said.

Maybe I am not recalling that accurately enough to make sense, but
maybe you see what might have been meant and could comment on that.

Maybe I could cast my question like this: would your "we can transform
any isomorphism in an equality" help to make some of the existing
proofs that are heavy on the univalence axiom, such as that of
Blakers-Massey, any easier?

Best wishes,
Urs

[Thierry Coquand]

 Thanks for the comments.

Once I quizzed somebody who worked on homotopy theoretic proofs in
HoTT whether the cubical type theory would make his proofs easier in
that the univalence terms would finally compute. But he said
(recollecting from my memory) that he wouldn't believe so, since while
the expressions would compute, they would compute to terms in the
ambient type theory in which the cubical complexes are encoded, and
these may not have any obvious meaning in the actual homotopy type
theory, he said.

Maybe I am not recalling that accurately enough to make sense, but
maybe you see what might have been meant and could comment on that.

 Indeed the terms may not have an obvious meaning in the

present version of homotopy type theory (based on intensional equality

and univalence as an axiom), but they have a meaning in this cubical 

type theory. For instance, there is a simple and rather intuitive proof of

function extensionality in this cubical type theory  (which however does not have

an obvious meaning in the present version of homotopy type theory). We can

look at proofs of function extensionality from univalence and compute the 

normal form of these proofs. We did this for two such proofs (in the files

uafunext1, uafunext2), corresponding respectively more or less to the proof suggested by

Dan Licata and the proof in the book, and in both cases, the normal form we get is a slight

variation of the direct proof (and all occurrences of univalence have disappeared).

Maybe I could cast my question like this: would your "we can transform
any isomorphism in an equality" help to make some of the existing
proofs that are heavy on the univalence axiom, such as that of
Blakers-Massey, any easier?

 For the small examples we have tried

the use of the cubical syntax does seem to simplify the proofs. For instance

the proof that S1 -> A is equal to (Sigma x:A) Id A x x  in the file ex1.ctt seems simpler

than the proof in the book Lemmas 6.2.5-6.2.9. The same holds for the proof that S1

is equal to the suspension of Bool.  It would indeed be interesting to see if the fact that 

"univalence computes" simplify some more complex argument.

 Best regards,

 Thierry

[Dan Licata]

Hi Urs,

I think that cubical type theories, of the kind developed by Thierry and his group, by me and Guillaume Brunerie, by Thorsten Altenkirch and Ambrus Kaposi, and by Andrew Polonsky, are a major improvement on "book HoTT" for synthetic homotopy theory:

(1) A lot of equations that always felt like they should be definitional are in fact definitional, such as ap (f o g) = ap f o ap g, ap (\x->x) = (\x->x), ap f refl = refl, the beta and eta rules for higher intro and elim rules for each type (pairing of paths, function extensionality,…), beta reduction for higher inductive types, etc.

(2) The proliferation of "dependent" and "non-dependent" versions of things goes away: the homogeneous identity type is literally a degenerate heterogeneous identity type, simple ap is literally a special case of dependent ap, higher cube types can be defined by iterating the pathover type and they behave well.

(3) transport reduces in a type-directed manner, including on UA

(4) It is posible to pattern-match on HITs with a nice notation, which extends to matching on tuples of HITs.

A nice example of all of this is the the torus = S1 * S1 proof in these slides from a couple of talks at CMU in March:
http://dlicata.web.wesleyan.edu/pubs/lb14cubical/lb14cubes-cmu-march-2015.pdf
which you can contrast with the amount of administrative overhead in the version in Agda here:
http://dlicata.web.wesleyan.edu/pubs/lb15cubicalsynth/lb15cubicalsynth.pdf
All of the manual beta reduction goes away and the proof for each case is just reduction---there is no noise left whatsoever.
(The rules for the Kan operation in those slides are based on Thierry's preliminary note on the Kan condition for the faces/degeneracies/symmetries/diagonals/but-not-connections-or-involutions cube category… we still haven't gotten the universe and univalence to work for that cube category yet, but I hold out hope that it can be done.)

-Dan

[Martin Escardo]

In addition to what Thierry and Dan say, it has to be emphasized that in
this cubical type theory (and in its Haskell implementation), every
closed term of type Nat reduces to a numeral.

In particular, the famous "Brunerie constant" should evaluate to 2 in
cubicaltt (after it is formalized in cubicaltt).

M.

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

[Thierry Coquand]

Here is a much simpler example that this system can now handle without any optimization.

One defines S1 as the HIT with base and loop, and susp A as the HIT with north, south
and merid a: north ---> south, for a : A. One can prove that S1 is isomorphic and hence equal to susp bool
(Lemma 6.5.1 in the book).
Following the proof of Theorem 7.3.12 in the book, one proves that the set truncation
of an equality type is equal to the equality of the corresponding groupoid truncation. One
also proves that the groupoid truncation of S2 = susp S1 is trivial. It follows that pi_1(S2)
which is the set truncation of the loop space S2,north is trivial. Since S1 = susp bool
we get a proof that the set truncation of the loop space susp (susp bool),north is trivial.

Given two concretely given element in this loop space, one can then ask the system to compute
a concrete homotopy between these two paths, by computing the normal form of this proof
applied to these two paths. Interestingly in the two examples we tried (in the file pi1S2), this homotopy happens
already at the level of the loop space, and not of its set truncation.

Thierry

[Martin Escardo]

On 30/04/15 15:09, Thierry Coquand wrote:
>
> Here is a much simpler example that this system can now handle without any optimization.
>
> One defines S1 as the HIT with base and loop, and susp A as the HIT with north, south
> and merid a: north ---> south, for a : A. One can prove that S1 is isomorphic and hence equal to susp bool
> (Lemma 6.5.1 in the book).
> Following the proof of Theorem 7.3.12 in the book, one proves that the set truncation
> of an equality type is equal to the equality of the corresponding groupoid truncation. One
> also proves that the groupoid truncation of S2 = susp S1 is trivial. It follows that pi_1(S2)
> which is the set truncation of the loop space S2,north is trivial. Since S1 = susp bool
> we get a proof that the set truncation of the loop space susp (susp bool),north is trivial.
>
> Given two concretely given element in this loop space, one can then ask the system to compute
> a concrete homotopy between these two paths, by computing the normal form of this proof
> applied to these two paths. Interestingly in the two examples we tried (in the file pi1S2), this homotopy happens
> already at the level of the loop space, and not of its set truncation.

Interesting.

Can an non-trivial computation of a number or a boolean be extracted
from this example or something like it, that would get stuck in HoTT
with postulates for univalence and HIT's?

Martin

>
> Thierry
>
>
>
>
> On Apr 15, 2015, at 12:59 AM, Martin Escardo wrote:
>
>> In addition to what Thierry and Dan say, it has to be emphasized that in
>> this cubical type theory (and in its Haskell implementation), every
>> closed term of type Nat reduces to a numeral.
>>
>> In particular, the famous "Brunerie constant" should evaluate to 2 in
>> cubicaltt (after it is formalized in cubicaltt).
>>
>> M.
>

[Thierry Coquand]

>
> Can an non-trivial computation of a number or a boolean be extracted
> from this example or something like it, that would get stuck in HoTT
> with postulates for univalence and HIT's?

This rather illustrates the following form of canonicity for HIT: any canonical element
(of any dimension) is built using only constructors and "composition"
(where we can replace some faces of an object along equality, an equality being itself
some higher dimensional element of the HIT).
In this way we have an a priori purely combinatorial description of normal form of
closed terms of an HIT such as susp S1, or susp (susp bool).
This can be seen as a generalization of canonicity for nat, where we can describe
a priori the normal form of closed terms of type nat.
For this example, we build a closed term (a square) of type the set truncation of S2, and
we check that the normal form of this term is built only using constructors and composition.

[Martin Escardo]

Very nice! M.

On 02/05/15 16:05, Dan Licata wrote:

> On Apr 30, 2015, at 4:54 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
>
>> Can an non-trivial computation of a number or a boolean be extracted
>> from this example or something like it, that would get stuck in HoTT
>> with postulates for univalence and HIT's?
>

> Here is a description of a function of type ((Z * Z) * (Z * Z)) -> (Z * Z):
>
> (1) start with four numbers
> (2) turn them into four loops on the circle, using Omega(S1) = Z componentwise
> (3) turn those into two loops on the torus, using T = S1 * S1 componentwise
> (4) compose these loops on the torus
> (5) convert the resulting loop on the torus to two loops on the circle using T = S1 * S1
> (6) convert the resulting loops on the circle to two integers using Omega(S1) = Z componentwise
>
> There is code for this "mysterious" function in the attached file. (Put it in the examples directory of the current head of the cubicaltt repository; it imports some of the other example files.)
>
> The implementation was able to calculate e.g.
>
> mystery ((0,1),(2,3)) = (2,4)
> mystery ((1,2),(2,3)) = (3,5)
>
> but bigger examples ran out of stack space.
>
> I think this function may have some applications in linear algebra ;-)
>
> -Dan

[Dan Licata]

[I accidentally sent this from the wrong email address over the weekend, and didn't notice it had been rejected.]

On Apr 30, 2015, at 4:54 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

> Can an non-trivial computation of a number or a boolean be extracted
> from this example or something like it, that would get stuck in HoTT
> with postulates for univalence and HIT's?

Here is a description of a function of type ((Z * Z) * (Z * Z)) -> (Z * Z):

(1) start with four numbers
(2) turn them into four loops on the circle, using Omega(S1) = Z componentwise
(3) turn those into two loops on the torus, using T = S1 * S1 componentwise
(4) compose these loops on the torus
(5) convert the resulting loop on the torus to two loops on the circle using T = S1 * S1
(6) convert the resulting loops on the circle to two integers using Omega(S1) = Z componentwise

There is code for this "mysterious" function in the attached file. (Put it in the examples directory of the current head of the cubicaltt repository; it imports some of the other example files.)

The implementation was able to calculate e.g.

mystery ((0,1),(2,3)) = (2,4)

mystery ((1,2),(3,4)) = (4,6)

[Thierry Coquand]

  Dan Licata found a mistake in the definition of the composition of the universe

underlying this version of cubical type theory (with diagonal and connections).

 This version was an attempt to combine univalence and definitional equality for

the computation rule for J. In order to achieve this, I tried to add a condition called

"regularity" on the filling operation. In turn, this condition simplifies the definition

of this filling operation and allows for a smooth addition of a diagonal operation

and connections. Cubical sets satisfying this condition are closed by dependent

product, sums,  identity types, data types, inductive-recursive universe, propositional truncation,

and one can define HITs satisfying this condition. Function extensionality has a simple

proof. If we call U the universe of such 

cubical sets, it is also the case that for any A B : U and T : U -> U, we have

T A -> T B as soon A and B are isomorphic (e.g. unary and binary numbers).

U itself has a composition operation, but the one used in this implementation is not regular

and it is open (but seems unlikely) if U has a regular composition operation.

 Several examples we tried don't use the composition in the universe, and so are correct

w.r.t. this model. However, the underlying type theory is much weaker than one with univalence.

 

 Actually all computations tried in this implementation worked (even the one involving univalence)...

 Dan did not find the problem by experimenting with the system, but by considering a consequence

of regularity for a closely related model.

His counter-example is very simple and involves only the composition of two lines E : A -> B and

F : B -> C in the universe. The problem is then to find a definition of A -> C in a uniform way that 

should be (strictly) equal to E when F is a constant line. Because of this simplicity, it shows well the

difficulty  of combining univalence and definitional equality for the computation rule of J  (following

this approach of giving a constructive version of the Kan filling condition).

  As shown by the work on the simpler cubical set model (without diagonals and connections)

not having definitional equality for the computation rule of J does not seem to be an issue for the development

of consequences of univalence.  Hopefully the convenient notation of equality proofs suggested by

the present implementation can be preserved for this simpler version of cubical sets.

However, not having a diagonal operation is a serious issue for HITs, and it not clear at this stage how 

to have a diagonal operation and univalence, and how to justify HITs + univalence constructively.

 Thierry

 

 

 

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

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

<mystery.ctt>

[Dan Licata]

Hi all,

It's quite disappointing that there is a problem with this cubical type theory, since a bunch of examples work very nicely (e.g. before realizing there was a problem, I did the proof that the total space of the Hopf fibration = S3 in less than 500 lines of code! and other proofs about higher inductives that are prohibitively annoying in "book HoTT" become easy).  

For the diagonals-but-no-connections version of cubical type theory that Guillaume Brunerie, Bob Harper, Carlo Angiuli, Ed Morehouse, and I have have been working on, we have tried to define a universe with Kan operations that satisfy the regularity conditions, and some related cancellation definitional equalities (which when translated to the connections version are instances of regularity).  We've tried many things and have not been successful.  To understand why the connections version seemed to work and the diagonals version didn't, on Friday, Bob and Carlo and Ed and I tried translating the diagonals Kan operation to the connections version (it can be encoded) to see why the desired equations held under translation.  It turned out that they didn't, and the reason was that regularity failed.  In case anyone is curious, code for the problematic example is here:

https://github.com/dlicata335/cubicaltt/blob/master/examples/drl/transportcompreg.ctt

Here is a short summary of my understanding of the technical details of the problem:

1) Write transport A (a : A0) : A1 for the Kan operation of coercing a point along the line A from the type A0 to the type A1.

2) The regularity condition says that transport A a = a when A is degenerate.  There is a corresponding regularity condition for higher box fillers, which says (for example) that when you compose a path with a reflexivity path, it's definitionally equal to the path you started with.  These correspond to having definitional equality for transport/J on refl.  

3) Write comp A B for the composite of two lines in the universe.  For the universe, the regularity equations say that

(a) comp A B is definitionally equal to A if B is degenerate

(b) the Kan operations for the type comp A B respect this definitional equality, in particular

transport (comp A B) v = transport A v 

if B is degenerate in the direction in which A and B are composed

(c) the Kan operations for the type comp A B are themselves regular, in particular

transport (comp A B) v = v 

if A and B are degenerate in the direction you are transporting

(You need A and B to be squares to see both (b) and (c), e.g. where A and B are glued together on the y axis and you are transporting in the x direction; see the above file)

(4) The definition of transport (comp A B) in Thierry's note and in the implementation satisfies (a) and (b) but not (c).  I think a variation of the definition that satisfies (a) and (c) but not (b) is possible.  The technical issue comes down to this: you have a square in the universe, and you want to extract from that a path showing that the square commutes, i.e. that transporting along left-then-top is the same as transporting along bot-then-right.  However, to get both (b) and (c) you need this path to be reflexivity both when the square is horizontally degenerate and when the square is vertically degenerate.  And it isn't clear how to construct such a square.  

-Dan

[Michael Shulman]

Intriguing!

On Sun, May 31, 2015 at 1:40 PM, Dan Licata <d...@cs.cmu.edu> wrote:
> (a) comp A B is definitionally equal to A if B is degenerate
> (b) the Kan operations for the type comp A B respect this definitional
> equality, in particular
> transport (comp A B) v = transport A v
> if B is degenerate in the direction in which A and B are composed

What does it mean for an operation to "respect a definitional
equality"? Or more to the point, what does it mean for an operation
to *not* respect a definitional equality? I thought everything in
type theory respected definitional equality by definition.

> (c) the Kan operations for the type comp A B are themselves regular, in
> particular
> transport (comp A B) v = v
> if A and B are degenerate in the direction you are transporting

Why is this not automatic? If A and B are degenerate in the same
direction, shouldn't there be a regularity equation saying that their
composite is also degenerate, so that (2) applies?

> However, to get both (b) and (c) you need this path to be
> reflexivity both when the square is horizontally degenerate and when the
> square is vertically degenerate. And it isn't clear how to construct such a
> square.

This sounds to me very similar to the problem with doing *simplicial*
sets constructively, that we eventually find ourselves needing to
argue by cases on whether some simplex is degenerate. Maybe it is the
same underlying issue popping up in a different guise?

I also didn't realize that cubical type theory was demanding that the
left and right unit laws p.refl = p and refl.p = p *both* hold
definitionally. That seems dangerous to me, for the same reason. Or
maybe this problem is really the same as the problem I would have
guessed with that.

Mike

[Michael Shulman]

On Sun, May 31, 2015 at 7:17 PM, Dan Licata <d...@cs.cmu.edu> wrote:
>> What does it mean for an operation to "respect a definitional
>> equality"? Or more to the point, what does it mean for an operation
>> to *not* respect a definitional equality? I thought everything in
>> type theory respected definitional equality by definition.
>

> Thierry has been justifying his cubical type theory in terms of a model in cubical sets. So a more careful way to phrase it is "is that definitional equality true in that model?" Of course if you say it's a definitional equality then it's a definitional equality---but does it make sense?

Sorry, but I still don't understand. If the equality (a) is true in
the model as whatever sort of "equality" is modeling definitional
equality, then that equality should be respected by all the model
constructions automatically. What does "make sense" mean?

>>> (c) the Kan operations for the type comp A B are themselves regular, in particular
>>> transport (comp A B) v = v
>>> if A and B are degenerate in the direction you are transporting
>>
>> Why is this not automatic? If A and B are degenerate in the same
>> direction, shouldn't there be a regularity equation saying that their
>> composite is also degenerate, so that (2) applies?
>

> See the picture in the code file I linked to. A and B are squares, where the top of A is glued to the bottom of B. You are transporting an element of the left-hand side of the composite square to the right-hand side of the composite square. (c) is the case where A and B are both horizontally degenerate. (b) above would apply if B were vertically degenerate, but it's not.

I didn't say (b), I said (2). If A and B are both horizontally
degenerate, then it seems as if their vertical composition should also
be horizontally degenerate?

>> I also didn't realize that cubical type theory was demanding that the
>> left and right unit laws p.refl = p and refl.p = p *both* hold
>> definitionally.
>

> I don't think it is; at least I don't see how to get both.

Ah, okay, I misunderstood something you said. Thanks for explaining.

Mike

[Dan Licata]

On May 31, 2015, at 9:53 PM, Michael Shulman <shu...@sandiego.edu> wrote:

> Intriguing!
>
> On Sun, May 31, 2015 at 1:40 PM, Dan Licata <d...@cs.cmu.edu> wrote:
>> (a) comp A B is definitionally equal to A if B is degenerate
>> (b) the Kan operations for the type comp A B respect this definitional
>> equality, in particular
>> transport (comp A B) v = transport A v
>> if B is degenerate in the direction in which A and B are composed
>
> What does it mean for an operation to "respect a definitional
> equality"? Or more to the point, what does it mean for an operation
> to *not* respect a definitional equality? I thought everything in
> type theory respected definitional equality by definition.

Thierry has been justifying his cubical type theory in terms of a model in cubical sets. So a more careful way to phrase it is "is that definitional equality true in that model?" Of course if you say it's a definitional equality then it's a definitional equality---but does it make sense? Since the model is very close to the syntax, so I tend to blur the distinction, and think of the equations that define a transport in the model as being the "definition" of the transport, and the other equations like regularity as needing to be justified. For example, in Pi a:A.B, the definition of transport is the usual transport-backwards-apply-the-function-then-transport-forwards, and then something like regularity is a consequence of that definition, because A and B are regular, so the two transports it reduces to cancel.

>> (c) the Kan operations for the type comp A B are themselves regular, in
>> particular
>> transport (comp A B) v = v
>> if A and B are degenerate in the direction you are transporting
>
> Why is this not automatic? If A and B are degenerate in the same
> direction, shouldn't there be a regularity equation saying that their
> composite is also degenerate, so that (2) applies?

See the picture in the code file I linked to. A and B are squares, where the top of A is glued to the bottom of B. You are transporting an element of the left-hand side of the composite square to the right-hand side of the composite square. (c) is the case where A and B are both horizontally degenerate. (b) above would apply if B were vertically degenerate, but it's not.

>> However, to get both (b) and (c) you need this path to be
>> reflexivity both when the square is horizontally degenerate and when the
>> square is vertically degenerate. And it isn't clear how to construct such a
>> square.
>
> This sounds to me very similar to the problem with doing *simplicial*
> sets constructively, that we eventually find ourselves needing to
> argue by cases on whether some simplex is degenerate. Maybe it is the
> same underlying issue popping up in a different guise?

Maybe; it feels a little different to me. Need to think about this.

> I also didn't realize that cubical type theory was demanding that the
> left and right unit laws p.refl = p and refl.p = p *both* hold
> definitionally. That seems dangerous to me, for the same reason. Or
> maybe this problem is really the same as the problem I would have
> guessed with that.

I don't think it is; at least I don't see how to get both. The composition operation in general is like filling a square and taking a missing face. Say you start with the left face and compose with a top and bottom, to make the right. The regularity condition applies when the top and bottom are degenerate. If the left and top are degenerate but the bottom isn't, it doesn't reduce to the bottom. So if you define composition p.q as left=p,bottom=q,top=degerate, then p.refl = p but not refl.p. If you have inverses in the cube category and define it as top=!p, left=q, bottom=degenerate, then you get the other one. If you define it as left=degeneracy on midpoint, top=!p, bottom=q, then you only get refl.refl, so it's like the definition where you do path induction on both.

-Dan

[Dan Licata]

On Jun 1, 2015, at 1:17 AM, Michael Shulman <shu...@sandiego.edu> wrote:

> On Sun, May 31, 2015 at 7:17 PM, Dan Licata <d...@cs.cmu.edu> wrote:
>>> What does it mean for an operation to "respect a definitional
>>> equality"? Or more to the point, what does it mean for an operation
>>> to *not* respect a definitional equality? I thought everything in
>>> type theory respected definitional equality by definition.
>>
>> Thierry has been justifying his cubical type theory in terms of a model in cubical sets. So a more careful way to phrase it is "is that definitional equality true in that model?" Of course if you say it's a definitional equality then it's a definitional equality---but does it make sense?
>
> Sorry, but I still don't understand. If the equality (a) is true in
> the model as whatever sort of "equality" is modeling definitional
> equality, then that equality should be respected by all the model
> constructions automatically. What does "make sense" mean?
>

You can take "make sense" to just mean be true in the model if you like… (more below)

>>>> (c) the Kan operations for the type comp A B are themselves regular, in particular
>>>> transport (comp A B) v = v
>>>> if A and B are degenerate in the direction you are transporting
>>>
>>> Why is this not automatic? If A and B are degenerate in the same
>>> direction, shouldn't there be a regularity equation saying that their
>>> composite is also degenerate, so that (2) applies?
>>
>> See the picture in the code file I linked to. A and B are squares, where the top of A is glued to the bottom of B. You are transporting an element of the left-hand side of the composite square to the right-hand side of the composite square. (c) is the case where A and B are both horizontally degenerate. (b) above would apply if B were vertically degenerate, but it's not.
>
> I didn't say (b), I said (2). If A and B are both horizontally
> degenerate, then it seems as if their vertical composition should also
> be horizontally degenerate?

Yes, the vertical horizontal composition is horizontally degenerate. Let me try to put it this way: in the syntax you give a reduction rule

transport (comp A B) v |-> some other term

which corresponds to the definition of transport for comp A B in the model. Then you want to know that "some other term" is equal to transport A v when B is vertically degenerate, and equal to v when both A and B are horizontally degenerate, without beta-expanding it and using (2). This is the justification for having (2). It corresponds to the fact that in the model you give a *definition* of [[transport (comp A B) v]] as some construction on [[A]] and [[B]] and [[v]], and you want that definition to define a regular fibration, and it doesn't.

Here's a simpler but analogous situation: you give a definition of substitution with equations like
(e1 e2)[theta] = e1[theta] e2[theta]
then you want to have the equality
e[theta][theta'] = e[theta[theta']]
Of course you can stipulate it as a judgemental equality syntactically, and then even if you had a clause
(foo e)[theta] = something
for which it wasn't the case that
(something for theta)[theta'] = (something for theta[theta'])
it would now be the case that (foo e)[theta][theta'] = (foo e)[theta[theta']] because you declared it to be so. But the equation isn't justified by the definition of substitution, so I would worry that the theory doesn't "make sense" (is inconsistent, doesn't describe any interesting models, won't have a computational interpretation, …). On the other hand, when the composition property is admissible, I can see why the theory makes sense (is consistent, has a computational interpretation) using syntactic methods (analyzing the normal forms).

-Dan

[Thorsten Altenkirch]

I agree in principle.In my ’99 LICS paper I was in the same situation (just for extensionality) - but later when I worked on OTT with Conor he wasn’t happy with this for technical reasons to do with the translation of pattern matching (CC Conor, maybe he can fill in the details). He then suggested a syntactic extension which adds this conversion to the translation (see our PLPV ’98 paper). Maybe something similar could be done for OTT but I think this would require a syntactic presentation of the system. 

Another question: if we have a 2 level system in the sense of HTS, is there any chance that we have J-beta as a strict equality? Or has this the same problem. I am thinking along the lines of Andrej’s Andromeda system where the definitional equality is user defined, but strict equality should be justified semantically.

Thorsten

From: Thierry Coquand <Thierry...@cse.gu.se>
Date: Sunday, 31 May 2015 17:38
To: Dan Licata <d...@cs.cmu.edu>
Cc: "HomotopyT...@googlegroups.com" <homotopyt...@googlegroups.com>
Subject: Re: [HoTT] a cubical type theory

As shown by the work on the simpler cubical set model (without diagonals and connections)

not having definitional equality for the computation rule of J does not seem to be an issue for the development

of consequences of univalence.  

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.

[Michael Shulman]

Thanks for trying to explain to a poor clueless category theorist. I
think I understand now how (c) can fail. This was key for me:

> It corresponds to the fact that in the model you give a *definition* of [[transport (comp A B) v]] as some construction on [[A]] and [[B]] and [[v]], and you want that definition to define a regular fibration, and it doesn't.

Although it seems to me that actually in the model you would be giving
a definition of [[comp A B]] and a separate definition of [[transport
C v]] and then putting those together to get a definition of
[[transport (comp A B) v]]. Is that right, or am I still
misunderstanding?

However, I still don't see how (b) can fail if (a) holds. You said

>> What does "make sense" mean?
>

> You can take "make sense" to just mean be true in the model if you like… (more below)

but it still seems to me that (b) must be true in the model if (a) is:

>> If the equality (a) is true in
>> the model as whatever sort of "equality" is modeling definitional
>> equality, then that equality should be respected by all the model
>> constructions automatically.

Mike

[Dan Licata]

On Jun 3, 2015, at 2:57 PM, Michael Shulman <shu...@sandiego.edu> wrote:

> Thanks for trying to explain to a poor clueless category theorist. I
> think I understand now how (c) can fail. This was key for me:
>
>> It corresponds to the fact that in the model you give a *definition* of [[transport (comp A B) v]] as some construction on [[A]] and [[B]] and [[v]], and you want that definition to define a regular fibration, and it doesn't.
>
> Although it seems to me that actually in the model you would be giving
> a definition of [[comp A B]] and a separate definition of [[transport
> C v]] and then putting those together to get a definition of
> [[transport (comp A B) v]]. Is that right, or am I still
> misunderstanding?

Yes and no. To show that [[comp A B]] is a regular uniform Kan fibration means to give a structure that includes a transport operation for it, and then [[transport A]] is "the transport operation for A". So if you reduce [[transport]] [[comp A B]] one step, you get "the transport operation you defined for comp A B".

> However, I still don't see how (b) can fail if (a) holds. You said
>
>>> What does "make sense" mean?
>>
>> You can take "make sense" to just mean be true in the model if you like… (more below)
>
> but it still seems to me that (b) must be true in the model if (a) is:
>
>>> If the equality (a) is true in
>>> the model as whatever sort of "equality" is modeling definitional
>>> equality, then that equality should be respected by all the model
>>> constructions automatically.

First you define comp A B as a cubical set, and then you define a Kan structure on it. (a) holding but (b) failing is like comp A B being the same cubical set as A when B is degenerate, but not having the same Kan operation.

-Dan

[Michael Shulman]

On Thu, Jun 4, 2015 at 4:36 AM, Dan Licata <d...@cs.cmu.edu> wrote:
> To show that [[comp A B]] is a regular uniform Kan fibration means to give a structure that includes a transport operation for it, and then [[transport A]] is "the transport operation for A". So if you reduce [[transport]] [[comp A B]] one step, you get "the transport operation you defined for comp A B".

Ah, right. Thanks.

> First you define comp A B as a cubical set, and then you define a Kan structure on it. (a) holding but (b) failing is like comp A B being the same cubical set as A when B is degenerate, but not having the same Kan operation.

I don't see how you could say that (a) holds in that case. Wouldn't
that be like saying that two groups are "equal" just because they have
the same underlying set?

[Andrew Polonsky]

In order to provide diversity to some of the sentiments here, I have to say -- it is really impressive that so many things DO work in this approach!

The issue with the computation rule for J being true only propositionally is a pervasive theme in all approaches, and it is remarkable that definitional equality can be pushed as far as it has been in this new cubical model.

Personally, I find the concept of "equivalence of types" to be inherently propositional, and don't see why one should believe in the definitional rule for J on the type level.  Other than a religious faith in the syntax of HoTT defined as "MLTT + UA", that is.

There is a big difference between equivalence between types and equality between objects.  The same equivalence can be obtained in many different ways.  Although one equivalence may be given by a finite amount of syntactic information, it would be a tall order to be able to check whether two given equivalences are the same.  There is no natural "syntactic equality" between equivalences, that would cover all the possible compositions and homotopic manipulations.

For definitional equality, we would need to recognize identity equivalence syntactically, including composition of degenerate equivalences, composition of inverses, etc.  One must indeed have an endless supply of hope if one hopes to ever realize this!

Cheers,

Andrew

[Thierry Coquand]

 Some updates about the problem with regularity: it turned out that regularity
is actually not needed for reducing the filling operation (to fill an open box)
to the composition operation (to find a lid of an open box) given connections.
An updated version of cubical type theory following this remark can be found at

   https://github.com/mortberg/cubicaltt

Compared to the previous implementation, the computation rule for J holds only 
as a propositional equality. Since we keep the diagonal operation however, we still
have a simple way to interpret function extensionality, and "good" computational behavior
for HITs (in particular for the circle where both computation rules for points and paths hold
as judgemental equality).

We also have a new derivation of the axiom of univalence (in the file univalence.ctt).
So both univalence and the fact that the universe is fibrant are derived from only one
operation on types (that we call glueing operation, and which consist in changing some faces
of a cube in the universe along equivalences).

 We also have added an internal way to state the uniform Kan condition, using the notion
of "partial" element in a presheaf model (documented in the References and Notes in the 
cubicaltt homepage). What we noticed was that the notion of "system" that we were using
can be described more clearly as special kind of  partial element (sub singleton). If we
say that a partial element is "connected" if it can be extended to a total element, the uniform
Kan condition becomes then the fact that a partial path connected at 0 is also connected
at 1. This gives a simpler presentation of the typing rules (that can also be found in the References
and Notes).