implementation of univalence

[Thierry Coquand]

 We would like to announce a prototype implementation of type theory

+ univalence axiom, with an evaluator for closed terms which computes

their semantics in the cubical set model.

If the term is of type Nat, it will evaluate to a numeral.

 This prototype includes a rudimentary type-checker, with Type:Type (to simplify)

which takes univalence as a non interpreted constant. Univalence however has

an interpretation in the cubical set model, which is used by the evaluator.

 This implements also propositional truncation. (One could include other

examples of higher inductive types; but one should extend first the syntax

of type theory to get natural elimination rules.)

 This includes some examples (in particular, Nicolai Kraus recent myst example).

 There are two ways to get the system

 - either by cloning the github repository with the command 

              git  clone https://github.com/simhu/cubical.git

  -or from hackage at 

        

              http://hackage.haskell.org/package/cubical-0.1.0

  

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

 

 

 

[Steve Awodey]

Dear Thierry,

This sounds very exciting!
Does it mean that you have now established Vladimir's conjecture for the general system (as opposed to just the 1-truncated system)?

Regards,

Steve

--
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/groups/opt_out.

[Thierry Coquand]

Dear Steve,

> Does it mean that you have now established Vladimir's conjecture for the general system (as opposed to just the 1-truncated system)?

Not quite. We have a computational model of univalence. A priori, one may imagine
that there is another computational model (e.g. using simplicial sets)
and that a closed term of type N computes to different numerals in these two models.
Vladimir's conjecture implies in particular that this cannot happen.
Maybe one way to solve it is to represent in TT + univalence our model, defining what
is a cube and then justifies each computation step that we use as
propositional equality in TT + univalence.

Thierry

[Vladimir Voevodsky]

What is the universe structure of the type theory which you interpret and how universes are interpreted?

V.

[Thierry Coquand]

The computation works with a term in Type:Type.
If this term comes from collapsing a term of a type theory with a type
hierarchy, then the computation terminates.
This should also interpret computationally resizing rules
since these rules do not add new computations (the termination in this case
is less clear).
The interpretation of universe is described in section 5.2 of our drat paper
on cubical sets. There it is described semantically in a set theory with one universe
of small sets. The interpretation however is uniform in the size of the universe.
Operationally an element of the universe is described by giving its Kan filling operations.
For the universe itself, the Kan filling operations are like constructors, but we have then to
explain recursively what are the Kan filling operations for these new constructed
elements that we add in the universe.
Thierry

[Martin Escardo]

On 19/12/13 16:58, Thierry Coquand wrote:
>
> We would like to announce a prototype implementation of type theory
> + univalence axiom, with an evaluator for closed terms which computes
> their semantics in the cubical set model.
> If the term is of type Nat, it will evaluate to a numeral.

This is great. Congratulations! It is good to see that univalence does
have a computational interpretation, both in theory and in practice as
in your implementation. As far I was concerned, both a positive and a
negative answer would be surprising, and I am (surprised and) glad to
see this settled positively!

In the last few days, after the implementaton of "cub" was announced,
I experimented with it: (1) I looked at the many given examples and I
ran them (very nice!), and (2) I produced my own examples. The
implementation is very efficient for the examples I tried. I even
tried "rogue" examples, along the lines of bar recursion, which are
not justified by the theory offered by the authors, but work in
practice in the implementation of the cubical model (and fast).

Programming/proving in the language "cub" feels like
programming/proving in Agda, with two main differences: (1) there is
no interactive environment, and so one has to produce complete
proofs/programs from scratch with no help (like when programing in
Haskell or ocaml), and (3) there are no implicit parameters, which
makes the process rather painful and time consuming. Of course this is
no criticism, as this is a prototype implementation.

From a theoretical point of view, I am interested in Steve's and
Vladimir's questions, already addressed by Thierry to some extent.

We know that "Voevodky's conjecture" is not (yet) settled by the
cubical model. As Thierry said, this would imply that in any model of
univalence, the interpretation of a closed term of natural number type
would be the same numeral (which is plausible but unsettled).

It would be nice to know that, at least, this model and Voevodky's
model of Kan simplicial sets give the same interpretation for closed
terms of natural number type. Can this be proved with a
logical-relation argument? This seems plausible, except that the
cubical model interprets the universe a la Hofmann-Streicher, but the
simplicial model interpretation of the universe doesn't seem to be
quite this (unless I am mistaken). But also, Vladimir's original
conjecture implies that it doesn't matter how the universe is
interpreted. In any case, this emphasizes that it would be interesting
to know whether the simplicial and cubical models give the same
interpretations at ground types, as a starting point.

Best,
Martin

[Bas Spitters]

I agree it is very nice, for the reasons that you mention.

In simplicial sets the universe is indeed an adaptation of the Hofmann Streciher construction; see p3 of
http://www.mathematik.tu-darmstadt.de/~streicher/sstt.pdf

So should homotopy theorists now reconsider cubical sets?
http://ncatlab.org/nlab/show/cubical+set

--
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 HomotopyTypeTheory+unsub...@googlegroups.com.

[Thomas Streicher]

Indeed I would say that also the universe of the sSet model can be
given in the form Martin H. and I introduced.
All models introduce much more equalities than there are on the
syntactic model. But in case of the work of Thierry et.al. the model
is defined inside ordinary type theory. It would be interesting to
identify the conversion rules induced by this interpretation.

Thomas

[Валерий Исаев]

The cartesian product of cubical sets is not well-behaved.

Does this fact cause any problems?

E.g., suppose that we have added an interval type I to the system.

Then the product I \times I is contractible (in HoTT), but its interpretation is not.

-- Valery Isaev

четверг, 19 декабря 2013 г., 20:58:48 UTC+4 пользователь coquand написал:

[Steve Awodey]

This has been discussed, and it is indee a very important issue.

I think the idea is that the ones that are Kan -- which are the ones used for the interpretation of types -- should have the right product.

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

[Michael Shulman]

Yes. In particular, an interval type cannot be interpreted by the
"obvious" cubical interval, since that is not Kan -- rather it must be
interpreted by a fibrant replacement thereof.

[Vladimir Voevodsky]

BTW I wonder what it means for the possibility of having exact equality in the system. If we have exact equality then we can create types whose models will be non-fibrant. To still have the cubical model what will we have to change?

V.

[Валерий Исаев]

Was this proved?

It is true that the product of X and Y is well-behaved if X and Y are fibrant in the "canonical" model structure on cubical sets.

But Kan cubical sets are not necessarily fibrant in this sence, and it seems that the product of contractible Kan cubical sets may still be not contractible.

Am I wrong?

-- Valery Isaev

четверг, 26 декабря 2013 г., 23:10:27 UTC+4 пользователь Michael Shulman написал:

> email to HomotopyTypeTheory+unsub...@googlegroups.com.

> For more options, visit https://groups.google.com/groups/opt_out.
>
>
> --
> 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 HomotopyTypeTheory+unsub...@googlegroups.com.

[Thierry Coquand]

Indeed, in HoTT the type for the unit interval is interpreted by the fibrant replacement of the cubical set I (and it has a concrete description that we describe in our draft paper on cubical sets)
Thierry
________________________________________
From: HomotopyT...@googlegroups.com [HomotopyT...@googlegroups.com] on behalf of Steve Awodey [awo...@cmu.edu]
Sent: Thursday, December 26, 2013 8:00 PM
To: Валерий Исаев
Cc: HomotopyT...@googlegroups.com
Subject: Re: Re: [HoTT] implementation of univalence

This has been discussed, and it is indee a very important issue.
I think the idea is that the ones that are Kan -- which are the ones used for the interpretation of types -- should have the right product.

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

[Валерий Исаев]

Oh, I see now.

In appendix 1, you construct a connection for 1-cells.

Is it true that Kan cubical sets can always be equipped with a connection structure?

пятница, 27 декабря 2013 г., 2:23:32 UTC+4 пользователь coquand написал:

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

For more options, visit https://groups.google.com/groups/opt_out.


--
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 HomotopyTypeTheory+unsub...@googlegroups.com.

[Michael Shulman]

What about the gluing approach that I used for the 1-truncated theory
-- could that be combined with the cubical model, to show that the
canonical forms computed by your algorithm are equal to the original
terms? Perhaps the global sections functor from the 1-truncated
theory to groupoids could be composed with the cubical nerve of
groupoids to yield a functor that we could glue along?

[Steve Awodey]

for the 1-truncated theory, it seems like we should be able to compare the simplicial and cubical models directly via functors back and forth, by restricting to the Kan objects on each side in order to get the right shapes (or maybe better, via functors from groupoids into each).

[Michael Shulman]

On Fri, Dec 27, 2013 at 9:42 AM, Steve Awodey <awo...@cmu.edu> wrote:
> for the 1-truncated theory, it seems like we should be able to compare the simplicial and cubical models directly via functors back and forth

Yes, that seems likely, but it wouldn't give a full canonicity result,
would it? Just knowing that the simplicial and cubical models compute
the same values doesn't preclude that some other model might compute a
different value.

My understanding is that for canonicity we need both (1) an algorithm
computing from each term t a canonical form can(t), and (2) a proof in
the type theory that t = can(t). The cubical model gives (1) without
(2), whereas the gluing model gives (2) without (the algorithm part
of) (1). Attempts to extract an algorithm from the gluing model
foundered on its use of univalence for propositions in sets, which is
not constructive -- hence my thought that if we replace sets with the
constructive cubical model, perhaps we could get both.

> On Dec 27, 2013, at 12:30 PM, Michael Shulman <shu...@sandiego.edu> wrote:
>

[Thierry Coquand]

On Dec 26, 2013, at 11:54 PM, Валерий Исаев wrote:

Oh, I see now.

In appendix 1, you construct a connection for 1-cells.

Is it true that Kan cubical sets can always be equipped with a connection structure?

 I don't know (but my guess is that this should be possible…)

 Appendix 1 is not logically necessary for the model of type theory. Its goal

is to describe directly how to define the fundamental groupoid and the path space of a space

represented as a Kan cubical set. This is technically simpler than for simplicial sets

(in particular to define the path space operation for Kan cubical sets is much simpler

than for Kan simplicial sets).

   Thierry

PS: About the interval, maybe the following remarks are relevant. 

Andy Pitts noticed that several concepts of the theory of nominal sets

(e.g. as presented in his book "Nominal sets. Names and symmetry in Computer Science.")

apply for our version of cubical sets. In particular, any cubical set can

equivalently be presented as a nominal set with substitution operations (a=0), (a=1)

for each name a. This alternative presentation is really convenient for the implementation.

The interval I can be presented

 -either as the functor  I(X) = X union {0,1}        covariant functor on the category of names

(our definition of cubical set)

 -or as the nominal set I = Names union {0,1} with canonical swapping and substitution

operations  

 This is a cubical set which does not have Kan filling operations.

 Nominal sets have a separated product (usually called tensor product for cubical sets)

and the square is the separated product I * I , which is not the same as the cartesian product

I x I. The path space Path(X) can be defined as I -* X, where I -* is the right adjoint of the functor

I*. 

 

[Michael Shulman]

After a little more thought, it seems to me that homotopy canonicity (via gluing) and the constructive cubical model already combine to yield a full canonicity proof for the 1-truncated theory.

Suppose t:N is a term using univalence. Homotopy canonicity says there exists an external natural number n and a term p:Id_N(t,suc^n(0)), also using univalence, but doesn't supply an algorithm to compute n. The cubical model gives an algorithm to compute an external natural number m such that [t] = [suc^m(0)] in the cubical model, but doesn't preclude the possibility that [t] is different in some other model. But putting them together, we have [p] : Id_N([t],[suc^n(0)]) in the cubical model, hence [suc^n(0)] = [suc^m(0)] in that model, whence n=m. Thus, we have an algorithm to compute an external natural number n ( = m) such that there exists a term p:Id_N(t,suc^n(0)) -- and so in particular, the value of t computed by the cubical model is the same as that computed by any other model.

Am I missing something?

Mike

[Steve Awodey]

On Jan 4, 2014, at 11:20 AM, Michael Shulman <shu...@sandiego.edu> wrote:

After a little more thought, it seems to me that homotopy canonicity (via gluing) and the constructive cubical model already combine to yield a full canonicity proof for the 1-truncated theory.

Suppose t:N is a term using univalence.

(1)

Homotopy canonicity says there exists an external natural number n and a term p:Id_N(t,suc^n(0)), also using univalence, but doesn't supply an algorithm to compute n.

this is shown by gluing into groupiods, right?

(2)

The cubical model gives an algorithm to compute an external natural number m such that [t] = [suc^m(0)] in the cubical model, but doesn't preclude the possibility that [t] is different in some other model. But putting them together, we have [p] : Id_N([t],[suc^n(0)]) in the cubical model,

why is it the same n, now that we are in cubical sets?

are we now regarding groupoids as special cubical sets, and redoing the gluing proof of (1) with respect to them?

i.e. we gluing into cubical set instead of groupoids for step (1)?

hence [suc^n(0)] = [suc^m(0)] in that model, whence n=m. Thus, we have an algorithm to compute an external natural number n ( = m) such that there exists a term p:Id_N(t,suc^n(0)) -- and so in particular, the value of t computed by the cubical model is the same as that computed by any other model.

Am I missing something?

it seems OK as long as (1) is redone w/resp. to cubical sets rather than groupoids.

So we need to do one of two things:

(i) replace the original gluing along the global sections functor G into Groupoids with a new one along the composite of G with a suitable nerve Groupoids --> cSets, which presumably lands in Kan cSets.

(ii) directly define, in a functorial way, a cubical set structure on (the terms of) each type (and show that the result is Kan).  This has proven hard to do in the simplicial case, but should be relatively easy for cubical sets -- although I admit that I haven't yet found the time to sit down and do it.  Indeed, since we only need the 1-truncated case here, it should be even easier -- not nearly as involved in building globular infinity groupoid of a type.  Then we glue along this "cubical nerve of a type" functor.

These should come to essentially the same thing.

Steve

[Dan Licata]

This seems right to me, nice! Indeed, I think it says that any
(possibly non-constructive) proof of homotopy canonicity can be combined
with any constructive model to give a (possibly non-constructive) proof
of canonicity.

I think it's easier to see what's going on if you state canonicity for
bool instead of nat. In a classical metalanguage, let

CAN = For all closed terms t:2, there is an algorithm nf such that nf(t)
computes a boolean, and if nf(t) is 0 then there is a closed term p :
Id(t,False) and if nf(t) is 1 then there is a closed term p :
Id(t,True).

HCAN = For all closed terms t:2, either there is a closed term p :
Id(t,True) or there is a closed term p : Id(t,False).

CM = There is an algorithm nf : closed terms of type 2 -> booleans such
that nf(True) = 1 and nf(False) = 0 and for all p : Id(t,t'), nf(t) =
nf(t').

Then CM (constructive model) + HCAN (homotopy canonicity) implies CAN:
Assume t:2. By CM, we get nf(t) is a boolean. Suppose nf(t) is 0, then
we need to show that there is a closed term p : Id(t,False). By HCAN,
either Id(t,True) or Id(t,False). In the second case, we're done. In
the first, we run the proof of Id(t,True) through the constructive
model (this is like the "[p] : Id_N([t],[suc^n(0)]) in the cubical model, hence [suc^n(0)] =
[suc^m(0)]" step below), getting nf(t) = nf(True) = 1. Thus we have 0
= nf(t) = 1, a contradiction.

However, it seems a little round-about to use one model (groupoids) to
get homotopy canonicity and another to get computation; I'd think we
could get both at once, by gluing syntax with the constructive model.
Also, I don't see any reason why we shouldn't be able to get a full
constructive proof of HCAN, which would actually compute the path as
well as the answer---this would be useful for tactics. Thoughts?

-Dan

[Kevin Watkins]

I was wondering myself whether the cubical evaluator could in theory be extended to carry around terms (in the surface theory with postulated univalence).  Along with evaluating t to v it would produce a term Id(s_0, s_1) (where s_0 and s_1 are preimages of t and v in the translation from the surface theory to the cubical model).

[Michael Shulman]

Yes, gluing with the cubical model instead was my first thought. But Thierry has pointed out that the ordinary groupoid model can also be done constructively, to give an algorithm for the 1-truncated theory.

However, I'm not sure that the gluing proof of homotopy canonicity *is* constructive. If I recall correctly, I had to use LEM in the metatheory to test whether a witness to reducibility of suc(n) was the successor of a witness to reducibility of n or not. It seems that this would not be an issue with bool, though, which confuses me.

I'm not really happy with using "homotopy canonicity" to refer to the non-algorithmic version, as it's not clear what that has to do with homotopy. I first started using "homotopy canonicity" to mean that the given term was only propositionally equal to a numeral rather than judgmentally, but now the usage seems to have drifted. What about saying "judgmental/propositional" and "algorithmic/nonalgorithmic" for the four possibilities?

Mike

[Vladimir Voevodsky]

On Jan 5, 2014, at 12:40 PM, Michael Shulman wrote:

Yes, gluing with the cubical model instead was my first thought. But Thierry has pointed out that the ordinary groupoid model can also be done constructively, to give an algorithm for the 1-truncated theory.

However, I'm not sure that the gluing proof of homotopy canonicity *is* constructive. If I recall correctly, I had to use LEM in the metatheory to test whether a witness to reducibility of suc(n) was the successor of a witness to reducibility of n or not. It seems that this would not be an issue with bool, though, which confuses me.

I'm not really happy with using "homotopy canonicity" to refer to the non-algorithmic version, as it's not clear what that has to do with homotopy. I first started using "homotopy canonicity" to mean that the given term was only propositionally equal to a numeral rather than judgmentally, but now the usage seems to have drifted. What about saying "judgmental/propositional" and "algorithmic/nonalgorithmic" for the four possibilities?

I agree. Homotopy canonicity should mean what Mike says - canonicity up to paths-equality. One can further talk about decidable and general homotopy canonicity.

V.

[Steve Awodey]

so, do we have a proof or not?

[Peter LeFanu Lumsdaine]

On Mon, Jan 6, 2014 at 3:31 AM, Steve Awodey <awo...@cmu.edu> wrote:

so, do we have a proof or not?

As I understand the situation: we definitely have 

(1) a non-constructive proof of propositional canonicity, for the 1-truncated theory;

(2) a good algorithm for computing the canonical value, for terms of Bool, Nat, and other standard types.  (We know constructively that this algorithm computes the value in the groupoid model, and we know non-constructively by part 1 that the value in other models must always agree with this.)

I specify a *good* algorithm, because once we know propositional canonicity at all, we automatically have a terrible algorithm for it: given t:Nat, just enumerate and check all terms of the theory until we find one of type Id(t,[n]) for some numeral [n]; propositional canonicity then implies that this will terminate.  (I’m assuming that typechecking always remains at least semi-decidable.) So in particular, combining this observation with the above, we also get

(3) a bad algorithm for finding a proof that the canonical value is canonical;

and Thierry and Mike’s last couple of emails suggest that we perhaps also have, via Mike’s gluing proof applied to the constructively-presented groupoid model 

(4) (?) a good algorithm for finding a proof that the canonical value is canonical

but this is a little subtle, since it depends on constructivity of the propositional-canonicity-via-gluing argument, which is not entirely clear yet.

(And we also have, for the full un-truncated theory, an algorithm computing the value of terms in the cubical model; so *if* we had a proof of propositional canonicity for the un-truncated theory, we would know that these values were canonical, and this would again give us a good algorithm for computing the canonical values.)

–p.

[Vladimir Voevodsky]

Can we please get the terminology straight? 

1-tructaion is an extra axiom (every secondary path is homotopic to the identity). If one can prove canonicity in a theory with yet another axiom then canonicity in the theory without this axiom would follow. So the phrase "proof of propositional canonicity, for the 1-truncated theory;" makes no sense.

We should formulate what has been done by specifying precisely the universe structure of the theory for which various versions of homotopy canonicity has been proved. E.g. 

"a sequence of universe U_n with U_0 impredicative, U_n a subset of U_{n+1}, and U_n an object of U_{n+1}" (this is more or less the current setup of Coq)

it is important to be very precise in it.

BTW Note that univalence axiom is incompatible with 1-truncation axiom if there are at least three universes which are members of each other e.g. U0:U1:U2 and Bool:U0 . 

V.

[Michael Shulman]

On Jan 6, 2014 8:21 AM, "Vladimir Voevodsky" <vlad...@ias.edu> wrote:
> If one can prove canonicity in a theory with yet another axiom then canonicity in the theory without this axiom would follow.

This isn't clear to me.  A way to compute a canonical form in a theory with an added axiom can of course be applied to a term not containing that axiom, but the corresponding proof that Id(t,can(t)) might still contain the added axiom.

The nonconstructive proof of propositional canonicity applies to the theory with 1-truncation axiom and two univalent universes U0:U1, with bool and nat in U1.  This is what one has in the groupoid model, so presumably the algorithm arising from constructivizing that model also applies there.

Mike

[Vladimir Voevodsky]

On Jan 6, 2014, at 11:37 AM, Michael Shulman <shu...@sandiego.edu> wrote:

On Jan 6, 2014 8:21 AM, "Vladimir Voevodsky" <vlad...@ias.edu> wrote:
> If one can prove canonicity in a theory with yet another axiom then canonicity in the theory without this axiom would follow.

This isn't clear to me.  A way to compute a canonical form in a theory with an added axiom can of course be applied to a term not containing that axiom, but the corresponding proof that Id(t,can(t)) might still contain the added axiom.

Yes, that's right. I was not precise enough.  

The nonconstructive proof of propositional canonicity applies to the theory with 1-truncation axiom and two univalent universes U0:U1, with bool and nat in U1.  This is what one has in the groupoid model, so presumably the algorithm arising from constructivizing that model also applies there.

Can it further accommodate a resizing axiom in the form of a function RR1: hProp(U1)->U0 such that j(RR1(P))=P and RR1(j(P))=P (where j:U0->U1)?

V.

BTW Do you also have j:U0->U1 in your universe structure? It does not follow from U0:U1.

[Michael Shulman]

On Mon, Jan 6, 2014 at 9:04 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> BTW Do you also have j:U0->U1 in your universe structure? It does not follow
> from U0:U1.

Yes, sorry I did not say that.

> Can it further accommodate a resizing axiom in the form of a function RR1:
> hProp(U1)->U0 such that j(RR1(P))=P and RR1(j(P))=P (where j:U0->U1)?

It seems likely (at least if "=" means propositional equality), but I
have not checked it.

Mike

[Peter LeFanu Lumsdaine]

On Mon, Jan 6, 2014 at 4:20 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:

Can we please get the terminology straight? 

Yes, I was being a bit unclear about which theories I meant.

When I wrote “the 1-truncated theory”, I had in mind: the theory with two univalent universes U_0 -> U_1,  and with the axiom scheme that all types are 1-truncated.  The important point was that (iirc) this is the theory that Mike’s gluing proof with the groupoid model applies to.

When I wrote “the full un-truncated theory”, I had in mind: the theory with a N-indexed hierarchy of univalent universes, and no truncation axioms.

In particular, neither of these is literally a sub-theory of the other.  The second has more universes, while the first has the truncation axiom.

–p.

[Altenkirch Thorsten]

From: Peter LeFanu Lumsdaine <p.l.lu...@gmail.com>
Date: Tue, 7 Jan 2014 00:03:17 +0000
To: Vladimir Voevodsky <vlad...@ias.edu>
Cc: Steve Awodey <awo...@cmu.edu>, Michael Shulman <shu...@sandiego.edu>, Dan Licata <d...@cs.cmu.edu>, Thierry Coquand <Thierry...@cse.gu.se>, "HomotopyT...@googlegroups.com" <homotopyt...@googlegroups.com>
Subject: Re: [HoTT] implementation of univalence

On Mon, Jan 6, 2014 at 4:20 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:

Can we please get the terminology straight? 

Yes, I was being a bit unclear about which theories I meant.

When I wrote “the 1-truncated theory”, I had in mind: the theory with two univalent universes U_0 -> U_1,  and with the axiom scheme that all types are 1-truncated.  The important point was that (iirc) this is the theory that Mike’s gluing proof with the groupoid model applies to.

An easy way to achieve this would be to add K for equality of equality proofs, I.e.

K1 : (A : Type)(a, b : A)(p : a = b)(P : p = p -> Type)(m : P (refl p))(q : p = p) P(q)

with K1 A a b p P m (refl p) == m

T. 

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.

[Vladimir Voevodsky]

On Jan 6, 2014, at 7:03 PM, Peter LeFanu Lumsdaine wrote:

On Mon, Jan 6, 2014 at 4:20 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:

Can we please get the terminology straight? 

Yes, I was being a bit unclear about which theories I meant.

When I wrote “the 1-truncated theory”, I had in mind: the theory with two univalent universes U_0 -> U_1,  and with the axiom scheme that all types are 1-truncated.  

Do you mean U_0:U_1 and U_0->U_1 ? I think one should also specify whether Bool (with elimination to all families of types) is in U_0 or U_1. 

V.

[Martin Escardo]

On 19/12/13 18:26, Thierry Coquand wrote:
> Dear Steve,
>
>> Does it mean that you have now established Vladimir's conjecture for the general system (as opposed to just the 1-truncated system)?
>
>

> Not quite. [...]

Particular case of the question:

Is it at least easy to see that if you run a pure MLTT program
(i.e. that doesn't mention univalence or HIT's) of ground type (with
arbitrarily high universes) using the cubical model, we get the same
numeral as that computed syntactically by normalization?

M.

[Martin Escardo]

On 07/01/14 21:29, Martin Escardo wrote:
> Particular case of the question:
>
> Is it at least easy to see that if you run a pure MLTT program
> (i.e. that doesn't mention univalence or HIT's) of ground type (with
> arbitrarily high universes) using the cubical model, we get the same
> numeral as that computed syntactically by normalization?

(This is what programming language semanticists would call
"computational adequacy" of the model. Is the model computationally
adequate? Of course it should be.)

[Martin Escardo]

> yes, it is, and no, afaik, it's not been proved yet. usually
> logical relations are required.
>
> bob

And while we are at it: Is the Kan simplicial model of HoTT
computationally adequate wrt to the MLTT fragment of HoTT (where we
have Id and a countable tower of universes in our version of MLTT).

Can you exhibit a closed term of type N in MLTT (with identitiy types
and a sequence of universes) that normalizes to 17, but whose
denotation in Kan simplicial sets is 13?

Of course, you shouldn't be able to do that. Despite its
non-constructivity, the meaning assigned by the Kan simplicial model
should be the same as that assigned by the operational semantics of
MLTT. (For MLTT terms.)

The same should apply to the Kan cubical model.

Martin

[Peter LeFanu Lumsdaine]

On Tue, Jan 7, 2014 at 11:53 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

And while we are at it: Is the Kan simplicial model of HoTT
computationally adequate wrt to the MLTT fragment of HoTT (where we
have Id and a countable tower of universes in our version of MLTT).

Can you exhibit a closed term of type N in MLTT (with identitiy types
and a sequence of universes) that normalizes to 17, but whose
denotation in Kan simplicial sets is 13?

I don’t follow the issue here. Isn’t this immediate from soundness, i.e. the theorem that the model is a model?  Surely the reduction of the operational semantics is a sub-relation of the definitional equality of MLTT, which is modelled in simplicial sets by strict equality, and so if one term reduces to another then their denotations in SSets must be equal?

I feel like I must be misunderstanding something in the question here — the operational semantics under consideration, perhaps?

–p.

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 HomotopyTypeTheory+unsub...@googlegroups.com.

[Martin Escardo]

On 08/01/14 00:30, Peter LeFanu Lumsdaine wrote:
> On Tue, Jan 7, 2014 at 11:53 PM, Martin Escardo <m.es...@cs.bham.ac.uk
> <mailto:m.es...@cs.bham.ac.uk>> wrote:
>
> And while we are at it: Is the Kan simplicial model of HoTT
> computationally adequate wrt to the MLTT fragment of HoTT (where we
> have Id and a countable tower of universes in our version of MLTT).
>
> Can you exhibit a closed term of type N in MLTT (with identitiy types
> and a sequence of universes) that normalizes to 17, but whose
> denotation in Kan simplicial sets is 13?
>

> I don�t follow the issue here. Isn�t this immediate from soundness, i.e.

> the theorem that the model is a model? Surely the reduction of the
> operational semantics is a sub-relation of the definitional equality of
> MLTT, which is modelled in simplicial sets by strict equality, and so if
> one term reduces to another then their denotations in SSets must be equal?
>

> I feel like I must be misunderstanding something in the question here �

> the operational semantics under consideration, perhaps?

The issue is that, quoting Thierry in a private conversation,

the model does not validate the computation rule of J
definitionally.

Martin

[Vladimir Voevodsky]

On Jan 7, 2014, at 7:59 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

>
> On 08/01/14 00:30, Peter LeFanu Lumsdaine wrote:
>> On Tue, Jan 7, 2014 at 11:53 PM, Martin Escardo <m.es...@cs.bham.ac.uk
>> <mailto:m.es...@cs.bham.ac.uk>> wrote:
>>
>> And while we are at it: Is the Kan simplicial model of HoTT
>> computationally adequate wrt to the MLTT fragment of HoTT (where we
>> have Id and a countable tower of universes in our version of MLTT).
>>
>> Can you exhibit a closed term of type N in MLTT (with identitiy types
>> and a sequence of universes) that normalizes to 17, but whose
>> denotation in Kan simplicial sets is 13?
>>

>> I don’t follow the issue here. Isn’t this immediate from soundness, i.e.

>> the theorem that the model is a model? Surely the reduction of the
>> operational semantics is a sub-relation of the definitional equality of
>> MLTT, which is modelled in simplicial sets by strict equality, and so if
>> one term reduces to another then their denotations in SSets must be equal?
>>

>> I feel like I must be misunderstanding something in the question here —

>> the operational semantics under consideration, perhaps?
>
> The issue is that, quoting Thierry in a private conversation,
>
> the model does not validate the computation rule of J
> definitionally.

That's besides the point:

1. if t:nat and t normalizes to n (a numeral) then ( the model of t = the model of n) since reductions become equalities and ( the model of n = n ) since the model takes O to 0 and S to n => 1 + n .

2. if t:nat and there is e : Id t t' then (the model of t ) = ( the model of t') because the model of e is a homotopy between the model of t and the model of t' and two points of natural numbers set which are homotopic are equal.

3. We conclude that if t : nat and there is e : Id t n for a numeral n then the evaluation of t is n .

What we do not immediately know is the converse - if t : nat evaluates to n (a numeral) is there e : Id t n .

V.

[Michael Shulman]

On Tue, Jan 7, 2014 at 4:59 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> the model does not validate the computation rule of J definitionally.

That may be an issue with the cubical model, but not the simplicial one.

[Altenkirch Thorsten]

On 08/01/2014 00:59, "Martin Escardo" <m.es...@cs.bham.ac.uk> wrote:

>
>On 08/01/14 00:30, Peter LeFanu Lumsdaine wrote:
>> On Tue, Jan 7, 2014 at 11:53 PM, Martin Escardo <m.es...@cs.bham.ac.uk
>> <mailto:m.es...@cs.bham.ac.uk>> wrote:
>>
>> And while we are at it: Is the Kan simplicial model of HoTT
>> computationally adequate wrt to the MLTT fragment of HoTT (where we
>> have Id and a countable tower of universes in our version of MLTT).
>>
>> Can you exhibit a closed term of type N in MLTT (with identitiy
>>types
>> and a sequence of universes) that normalizes to 17, but whose
>> denotation in Kan simplicial sets is 13?
>>

>> I don¹t follow the issue here. Isn¹t this immediate from soundness, i.e.

>> the theorem that the model is a model? Surely the reduction of the
>> operational semantics is a sub-relation of the definitional equality of
>> MLTT, which is modelled in simplicial sets by strict equality, and so if
>> one term reduces to another then their denotations in SSets must be
>>equal?
>>

>> I feel like I must be misunderstanding something in the question here ‹

>> the operational semantics under consideration, perhaps?
>
>The issue is that, quoting Thierry in a private conversation,
>
> the model does not validate the computation rule of J
> definitionally.

This was also true for my old paper on eliminating extensionality
(http://www.cs.nott.ac.uk/~txa/publ/lics99.pdf) but this was fixed later
(http://www.cs.nott.ac.uk/~txa/publ/obseqnow.pdf) using Conor's insights
how to strengthen conversion (a technique which has many other
applications as well).

Cheers,
Thorsten

>
>Martin
>
>--

>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/groups/opt_out.

[Thomas Streicher]

> Can you exhibit a closed term of type N in MLTT (with identitiy types
> and a sequence of universes) that normalizes to 17, but whose
> denotation in Kan simplicial sets is 13?

The functor \Delta : Set -> sSet preserves the lcc structure and all
colimits and it is full and faithful. Moreover, its image lives in the
Kan part of sSet. This should also apply to the cubical set model.

Thomas

[Andreas Abel]

On 08.01.2014 02:32, Vladimir Voevodsky wrote:
> That's besides the point:
>
> 1. if t:nat and t normalizes to n (a numeral) then ( the model of t = the model of n) since reductions become equalities and ( the model of n = n ) since the model takes O to 0 and S to n => 1 + n .
>
> 2. if t:nat and there is e : Id t t' then (the model of t ) = ( the model of t') because the model of e is a homotopy between the model of t and the model of t' and two points of natural numbers set which are homotopic are equal.
>
> 3. We conclude that if t : nat and there is e : Id t n for a numeral n then the evaluation of t is n .
>
> What we do not immediately know is the converse - if t : nat evaluates to n (a numeral) is there e : Id t n .

I had expected that if t evaluates to n then simply

refl : Id t n

At least in our implementations of type theory, terms with the same
normal form are definitionally equal and hence indistinguishable, so t
is indistinguishable from n. Isn't

refl : Id t t

true anymore?

Cheers,
Andreas

--
Andreas Abel <>< Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andrea...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/

[Vladimir Voevodsky]

On Jan 8, 2014, at 11:33 AM, Andreas Abel <andrea...@ifi.lmu.de> wrote:

> On 08.01.2014 02:32, Vladimir Voevodsky wrote:
>> That's besides the point:
>>
>> 1. if t:nat and t normalizes to n (a numeral) then ( the model of t = the model of n) since reductions become equalities and ( the model of n = n ) since the model takes O to 0 and S to n => 1 + n .
>>
>> 2. if t:nat and there is e : Id t t' then (the model of t ) = ( the model of t') because the model of e is a homotopy between the model of t and the model of t' and two points of natural numbers set which are homotopic are equal.
>>
>> 3. We conclude that if t : nat and there is e : Id t n for a numeral n then the evaluation of t is n .
>>
>> What we do not immediately know is the converse - if t : nat evaluates to n (a numeral) is there e : Id t n .
>
> I had expected that if t evaluates to n then simply
>
> refl : Id t n
>
> At least in our implementations of type theory, terms with the same normal form are definitionally equal and hence indistinguishable, so t is indistinguishable from n. Isn't
>
> refl : Id t t
>
> true anymore?

Sorry, I used ambiguous terminology. Thierry calls his mode ``an evaluator" so what I meant by ``evaluates to" is ``equals to in the model".

V.

[Andreas Abel]

Ah I see, thanks for clarifying! --Andreas

[Thierry Coquand]

We now have an experimental branch called conv in the github repository
which uses the cubical evaluator for testing conversions during type-checking.

As a consequence, we have new conversion rules for the constant

mapOnPaths : (A B:U) (f:A->B) (x y :A) -> Id A x y -> Id B (f x) (f y)

that are justified by this explanation of the Identity type.

These new definitional equalities are that this operation commutes in
a definitional way with identity and composition of functions, e.g. we have

mapOnPaths (\x -> x) p = p (1)

equality which does not hold definitionally in MLTT.

This simplifies some proofs, e.g. the proof of gradth.

Thus, whereas the computation rule for J as a conversion is missing
(it holds only as a propositional equality), we also have new definitional
equalities not present in MLTT.

The interpretation of the constant mapOnPath in the model is

mapOnPaths f (<a>u) = <a>(f u)

where a is a symbol intuitively ranging over the unit interval and <a>u is the affine
abstraction used in nominal sets. If f is \ x -> x we get the equality (1).

If u does not depend on a, then the constant path <a>u is the interpretation of
refl u.

This use of nominal sets is really convenient for the implementation. (One could
avoid it by using deBruijn index, and then one can see that cubical identities
are nothing but the usual laws for deBruijn indices).

For connecting the cubical model and MLTT + univalence, notice that the argument

>> the model does not validate the computation rule of J
>> definitionally.
>
> That's besides the point:
>
> 1. if t:nat and t normalizes to n (a numeral) then ( the model of t = the model of n) since reductions become equalities and ( the model of n = n ) since the model takes O to 0 and S to n => 1 + n .
>
> 2. if t:nat and there is e : Id t t' then (the model of t ) = ( the model of t') because the model of e is a homotopy between the model of t and the model of t' and two points of natural numbers set which are homotopic are equal.
>
> 3. We conclude that if t : nat and there is e : Id t n for a numeral n then the evaluation of t is n .

which shows that if t is a closed term of type Nat which reduces to S^k(0) in MLTT then
the semantics of t is also k in the cubical set model, is
purely "syntactical". The only thing to check is that all computation rules of MLTT
are justified as propositional equalities in the cubical set model. All such rules are
actually also computation
rules for the cubical evaluator except for the computation rule for J which is justified
as a propositional equality.
This argument does not need for instance to build a model of MLTT in cubical sets.

This suggests that it should also be possible to have a similar argument in the other direction.
It would be enough for this to have a notion of cube in MLTT
and to interpret all operators and justify all reduction rules of the cubical evaluator
as propositional equalities in MLTT + univalence. If this can be done then we would have
a proof that if t reduces to k with the cubical evaluator, then t is propositionally equal
to S^k(0) in MLTT + univalence.

Thierry

[Vladimir Voevodsky]

Hmmm... so in this branch the type checker is allowed to use your new ``cubical reductions" but is not allowed to use iota-reduction for Id-types?


V.

[Thierry Coquand]

On Jan 11, 2014, at 4:29 PM, Vladimir Voevodsky wrote:

> Hmmm... so in this branch the type checker is allowed to use your new ``cubical reductions" but is not allowed to use iota-reduction for Id-types?
>
>
> V.

Exactly. Besides having new conversion rules for mapOnPaths, we also have
(now in the master branch of the github repository)

-introduced a new type of "dependent equality" or dependent path

IdP A B P a b

for P : Id U A B and a:A, b:B. Using this new type construction, one can define
the notion of "dependent path"

IdD A F a0 a1 p b0 b1 for A:U, F:A-> U, a0 a1:A, p : Id A a0 a1, b0 : F a0, b1:F a1

IdD A F a0 a1 p b0 b1 = IdP (F a0) (F a1) (mapOnPaths F a0 a1 p) b0 b1

mentioned in Remarks 6.2.1, 6.2.3 in the book. This satisfies the definitional equality

IdP A A (refl U A) a0 a1 = Id A a0 a1

-an extension of mapOnPaths for dependent types

mapOnPaths A F f a0 a1 p : IdD A F a0 a1 p (f a0) (f a1) if f : (x:A) -> F x

and a simpler way to express equality on a sigma type, with good behavior w.r.t. mapOnPaths

-introduced the circle S1 so that, using the notation of Lemma 6.2.5 in the book, both
equations

f base = a
mapOnPaths f loop = p

are definitional. It is then possible to define the helix and -compute- the winding number of
an element of Id S1 base base

Anders, Cyril, Simon, Thierry

[Peter LeFanu Lumsdaine]

(Apologies for re-awakening sleeping dogs — but I hope this will help those who, like me, were left rather confused and uncertain by this thread.)

I just had a discussion with Per Martin-Löf that left me with (I think!) a much better understanding of what’s going on in the cubical model — and in particular, a satisfactory answer to Martin’s question above, “is it possible to have a term t:Nat which normalises to the numeral [17] but which is interpreted in the cubical model as 13?”

As previously explained by Thierry, the issue is that the Id-comp rule is modeled only as a path, not as strict equality.  I had (mis)understood this as meaning that the paper shows:

“The cubical model is a weak model of (ordinary Martin-Löf) type theory.”

and so I was confused, because I wasn’t sure precisely what a weak model meant, or what consequences one could draw from it.  Instead, though, what the paper quite un-problematically shows is that:

“The cubical model is a (genuine, strict) model of a slightly weaker type theory.”

where the type theory being modeled (call it WTT for now) is obtained from the usual type theory (call it TT) by removing the Id-comp rule, and replacing it with just a propositional equality.

So we certainly know: if *in WTT*, we have a term t:Nat which normalises (or, more generally, is propositionally equal) to [17], then the interpretation of t in the cubical model will be 17.

On the other hand, if we just know that in ordinary TT our term t normalises to [17], then we don’t know what will happen to t in the model unless we can somehow lift the normalisation to a proof of equality in WTT.  However (as the cubical paper mentions) Nils Anders Danielsson has done a fair bit of exploration in Agda, coding up the fundamentals of HoTT without assuming (iirc) the reduction rules for *any* inductive types, showing that in practice, proofs in TT can be lifted to proofs in WTT.  This gives heuristic evidence for something like

Conjecture: TT is conservative over WTT.

If this holds, then we’d have a positive answer to Martins question — given a term t:Nat in WTT that normalises in TT to [17], conservativity says that we can lift the TT term |- refl(t) : Id(t,[17]) to a proof in WTT |- p : Id(t,[17]), and so conclude that in the cubical model, t is interpreted as 17.  This would also then give a precise sense in which the cubical model is a weak model of the full type theory TT.

I’ve been vague in all this about exactly what TT/WTT should be.  For the conservativity to be plausible, they certainly need functional extensionality, since without it a lambda-abstracted version of the Id-comp rule gives an easy counterexample.  Given that, it seems like they could reasonably also include anything that’s modeled (possible weakly) by the cubical model; and, Nils’ explorations suggest, WTT could weaken all iota-reductions to propositional equalities.

Apologies to NAD and the cubical experts if I’m still misunderstanding or misrepresenting anything of their work — hopefully I’m not and this all makes sense…

–p.

--

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.

[Thierry Coquand]

Dear Peter,
Many thanks for this message. The explicit introduction of the theory

WTT = TT removing the Id-comp rule and replacing it with just a propositional equality

makes the discussion much clearer.

I should emphasize that this is the -only- weakening of TT; in particular the computation
rules for Sigma, Nat, Bool, W-types, disjoint sums… all still hold in a definitional way
(and as reduction rules).
This is the theory that Nils Anders has been using, so in

> Nils Anders Danielsson has done a fair bit of exploration in Agda, coding up the fundamentals of HoTT without assuming (iirc) the reduction rules for *any* inductive types, showing that in practice, proofs in TT can be lifted to proofs in WTT.

one should read "without assuming the reduction rule for the Id type (but assuming all the other reduction rules
for list, disjoint sums, Nat, Bool…)"

The fact that the equality

J C d (refl a) = d

is not a computation rule is connected to the fact that, in this computational interpretation of Id, refl is not a constructor
and that Id A a b is not an inductively defined type anymore.

Thierry


PS1: On the other hand, the model justifies -new- definitional equalities like

mapOnPaths (\x -> g (f x)) p = mapOnPaths g (mapOnPaths f p)

mapOnPaths (\x -> x) p = p

that are not valid in TT.

PS 2: I should also correct a previous message. Checking some invariant in our program,
we discovered that the elimination rule for S1 in the cubical model
has to be modified, and with this modification, in the computation rules (notation for Lemma 6.2.5 in the book)

f base = a
mapOnPaths f loop = p

only the first equation is validated definitionally, while the second holds only as a propositional equality.

[Michael Shulman]

On Tue, Jan 21, 2014 at 10:06 AM, Thierry Coquand
<Thierry...@cse.gu.se> wrote:
> f base = a
> ap f loop = p

>
> only the first equation is validated definitionally, while the second holds only as a propositional equality.

Very interesting! I wonder whether it is a coincidence that so many
different factors seem to point to this sort of thing being the
"right" choice for the computation rules of a HIT, or if there is some
deeper reason for it.

[Guillaume Brunerie]

Thierry, could you be more specific? Is it in the cubical model that the second rule only holds propositionally or is just in the syntax that it's somehow problematic to assume it?
Because I completely disagree with Mike, both computation rules should definitely be definitional (but I can understand that hacking it into the syntax of MLTT could be problematic).

Guillaume

[Thierry Coquand]

 In the cubical set model as we have now, we can only validate the second rule propositionally.

 It would indeed be nice to have a model where it holds in a definitional way.

 Thierry

[Michael Shulman]

Please notice that I did not say that I think this *is* the right choice. (-:

[Dan Licata]

Hi Thierry and everyone,

This is surprising to me, because there must be some extra definitional
equality that is valid. Suppose I take

Cover : S1 -> Type
Cover = S1-rec Z (ua successor)

then

transport_Cover (loop,0)

is a closed term of type Nat, which must reduce to a numeral. So is it
the case that this transport reduces, but

ap Cover loop

does not? If we rewrite the transport as

coe (ap Cover loop) 0

where coe is the function A = B -> (A -> B)
then is the idea that coe causes reductions but the path itself is not reduced?

Thanks!
-Dan

[Thierry Coquand]

Hello,

ap Cover loop is of type Id U Z Z

so it will be a path in the universe, which is obtained by Kan composition.
In the prototype it evaluates to something like

<2> Com U (Box 0 3 or (N, N) [((2,0),equivEq 3 (or (N, N)) (or (N, N)) (sucZ)),((2,1),or (N, N))])

where equivEq … is the path between Z = N + N and Z = N + N obtained by univalence
and Com U … the Kan composition operation in the universe.

In the universe, Kan composition behaves like a constructor.

It is only when we apply the function "coe : A=B -> A -> B" to it that the computation starts
and if we apply it to zero it reduces to one.

Thierry

[Peter LeFanu Lumsdaine]

On Tue, Jan 21, 2014 at 10:12 PM, Dan Licata <d...@cs.cmu.edu> wrote:

Hi Thierry and everyone,

This is surprising to me, because there must be some extra definitional
equality that is valid.  

This issue can also come up without any involvement of univalence (and hence with fewer openings for other clever reductions to help things along).  Define

[ P : S1 -> Nat ]

[ P = S1-rec 0 (refl 0) ]

and then consider

[ transport List (ap S1 loop) nil ]

which appears stuck, although it “should” reduce to [nil].

Other than a a computation rule for [ ap (S1-rec …) loop ], what kind of rule could allow this term to reduce?  I find it hard to imagine what could apply — unless somehow the type-directed computation of J/transport for loop could realise that Nat is an hset, and hence that it can ignore its path argument?

–p.

 

[Dan Licata]

Hi Thierry,

Thanks; that makes sense! So at type Z->Z, do you get a definitional
equality between

transport Cover loop
and
(\x.x+1)

?

Are the identity types "lazy" at all types? I.e. are there types where
Kan composition does not behave like a constructor?

[Thierry Coquand]

> Are the identity types "lazy" at all types? I.e. are there types where
> Kan composition does not behave like a constructor?

Kan composition behaves like a constructor for U and Pi types and not
as a constructor at types Id and data types.
Thierry

[Dan Licata]

Hi Peter,

Is the idea with your example that List : Nat -> Type (i.e. it's the
type of lists of length n)? And should it be "ap P loop"?
Otherwise I can't type-check it.

Based on Thierry's response, I'd guess that

transport List (ap P loop)

would reduce,
as would

coe (ap List (ap P loop))

but that ap P loop by itself does not reduce?


Thierry, is it still the case that the following hold definitionally?

ap(f o g) p = ap f (ap g p)
ap(\x -> x) p = p
ap f refl = refl

?

-Dan

[Thierry Coquand]

>
> Thierry, is it still the case that the following hold definitionally?
>
> ap(f o g) p = ap f (ap g p)
> ap(\x -> x) p = p
> ap f refl = refl
>
> ?

Yes, all these equalities hold definitionally.
Thierry

[Dan Licata]

Hi Thierry,

It's surprising to me that it's not like a constructor at data types.
Does that mean that if you have

p : Id Nat m n

then

p . refl
refl . p
p . (q . r) for appropriate q and r

will reduce? What do they reduce to?

How is the composition treated for higher inductives? Is that included
in "data types"?

Thanks!
-Dan

On Jan21, Thierry Coquand wrote:
>

[Thierry Coquand]

Data types are treated as (recursively defined) labelled sum, where the labels
are the constructors. So the only possible (closed) cubes for

p : Id Nat m n

are only possible if m = n = S^k(0) and then p has to be the constant cube S^k(0).
So for Nat, Bool, … the (closed) cubes are all constant and the Kan completion operation
is quite simple.

For higher inductives, we have only so far looked at propositional truncation
and S1 and the interval. There Kan composition operations are treated as constructors
and I think this is the correct interpretation (for S1, it is the elimination rule which should
be improved).
Thierry

[Steve Awodey]

Dear Guillaume,

On Jan 21, 2014, at 3:21 PM, Guillaume Brunerie <guillaume...@gmail.com> wrote:

Thierry, could you be more specific? Is it in the cubical model that the second rule only holds propositionally or is just in the syntax that it's somehow problematic to assume it?
Because I completely disagree with Mike, both computation rules should definitely be definitional

you seem quite certain — I am not yet convinced either way.

may I ask what your reasons are for this?

best,

Steve

[Jason Gross]

On Tue, Jan 21, 2014 at 3:21 PM, Guillaume Brunerie <guillaume...@gmail.com> wrote:

both computation rules should definitely be definitional (but I can understand that hacking it into the syntax of MLTT could be problematic).

What would be the problem with having it as part of the syntax of MLTT?  The computation rule should be

∀ A (f_base : A) (f_loop : f_base = f_base)

 ap (Circle_rect A f_base f_loop) loop

 ≡ ap (λ (x : Circle) ⇒ match x return A with

                          | base ⇒ f_base

                          | loop ⇒ f_loop

                        end)

      loop

 ≡ match loop in (_ = y) return

    ((λ (x : Circle) ⇒ match x return A with

                         | base ⇒ f_base

                         | loop ⇒ f_loop

                       end) base

      = (λ (x : Circle) ⇒ match x return A with

                            | base ⇒ f_base

                            | loop ⇒ f_loop

                          end) y)

   with

     | refl ⇒ refl

   end

 ≡ match loop in (_ = y) return

    (f_base

      = match y return A with

          | base ⇒ f_base

          | loop ⇒ f_loop

        end)

   with

     | refl ⇒ refl

   end

 ≡ match f_loop in (_ = fy) return (f_base = fy) with

    | refl ⇒ refl

   end

no?

More generally, I think the rule should be that given a higher inductive type [T] and a path constructor [p : a = b], any match of the form

  match p in (_ = y) return (P (match y with a => c | b => d | p => f end)) with

    | refl ⇒ g

  end

should be convertible with

  match f in (_ = y) return (P y) with

    | refl ⇒ g

  end

(Note that [P] must not mention [y] anywhere else; we must have only a single [y] that shows up, and it must be of the form [match y with ... end].)

To ensure judgmental confluence (in the case where [P] is (λ _ ⇒ foo), i.e., a constant function), you'd then also need the rule

match x return A with

  | constructor => a

end 

≡ a

(assuming [a] doesn't mention any arguments of the constructor, and all the branches of the match unify, and the return type is constant).  I don't think you need any other rules, but I'm not completely sure.

-Jason

[Thierry Coquand]

I was wondering if the refinement of the program for elimination rule over S1 we had to do was
actually needed on examples, and Guillaume provided the following one
(that I want to record here as a useful test for future implementation).

One defines a function

f : (x:S1) -> Id S1 x x

by S1-elimination with the specification

f base = loop
ap f loop = proof that loop : Id S1 base base is equal to loop : Id S1 base base
over loop (this is basically because loop^{-1} . loop . loop = loop)

From this one defines

g : S1 -> (S1 -> S1)

g x base = x
ap (g x) loop = f x

and

h : S1 -> S1
h x = g x x

We have ap h loop : Id S1 base base and its winding number should be 2
(as it is computed by the evaluator).

Thierry

[Guillaume Brunerie]

On 2014/1/22 Steve Awodey <awo...@cmu.edu> wrote:
> Dear Guillaume,
>
> On Jan 21, 2014, at 3:21 PM, Guillaume Brunerie
> <guillaume...@gmail.com> wrote:
>
> Thierry, could you be more specific? Is it in the cubical model that the
> second rule only holds propositionally or is just in the syntax that it's
> somehow problematic to assume it?
> Because I completely disagree with Mike, both computation rules should
> definitely be definitional
>
> you seem quite certain — I am not yet convinced either way.
> may I ask what your reasons are for this?

It seems just wrong to have one computation rule definitionally and
the other one only propositionally. I don’t see the identity type as a
construction that you define once and can then apply to any type (as
is done in MLTT), each type former should come with its own higher
dimensional structure, introduction, elimination and reduction rules,
and a higher inductive type is not something strange anymore, it’s
just an inductive type where some of the constructors happen to
construct higher dimensional structure. The elimination rule shouldn’t
treat them differently.

Also, I became convinced that this kind of definitional reduction is
essential if we want HoTT to be usable by normal mathematicians some
day.
I’ve given up on formalizing new stuff until we get the type theory
right, because right now using HoTT is way too tedious for no good
reason.
The good news is that I’m also convinced that we will get the type
theory right someday, so there is hope :-)

Guillaume

[Guillaume Brunerie]

On 2014/1/22 Jason Gross <jason...@gmail.com> wrote:
> On Tue, Jan 21, 2014 at 3:21 PM, Guillaume Brunerie
> <guillaume...@gmail.com> wrote:
>
>> both computation rules should definitely be definitional (but I can
>> understand that hacking it into the syntax of MLTT could be problematic).
>
> What would be the problem with having it as part of the syntax of MLTT?

Well, adding higher inductive types or univalence to MLTT already
sounds like a hack to me. The definition of the identity type as an
inductive family says that the identity type is generated by
reflexivity, but then we add randomly new equality proofs, that’s
nonsense.
Doesn’t it look wrong to you to write something like "match loop with
| refl => refl"? You’re asking the type theory to look at loop and
return refl when loop is refl. But loop isn’t refl and will never be!
Maybe that your reduction rule makes sense but I’m pretty sure that
you would need more than that. More generally, my guiding principle
for a well behaved type theory is that because of the higher
dimensional / higher groupoidal stuff you can’t have anything ad hoc.
If you add something ad hoc somewhere, then you will need another hack
to handle the 2-dimensional version of it, then another hack of hack
for the 3-dimensional version, and so on, and it will quickly blow up
and become completely unmanageable.
Also, for me the main advantage of HoTT is that it allows you to do
homotopy theory and more generally mathematics without the ad hoc-ness
of other foundations, so if the best type theory we can come up with
is MLTT + univalence + HIT + maybe some random additional reduction
rules, then I don’t think HoTT is any better than any other
foundation.
But as I said I’m sure there is a good type theory behind HoTT, so I’m
not worried :-)

Guillaume

[Michael Shulman]

On Wed, Jan 22, 2014 at 2:29 AM, Guillaume Brunerie
<guillaume...@gmail.com> wrote:
> Doesn’t it look wrong to you to write something like "match loop with
> | refl => refl"? You’re asking the type theory to look at loop and
> return refl when loop is refl. But loop isn’t refl and will never be!

This makes perfect sense if you remember that in general, (higher)
inductive types are only *generated* by their constructors.

http://golem.ph.utexas.edu/category/2013/02/presentations_and_representati.html

The syntax "match" for the recursion principle may give the mistaken
impression that that means the *only* inhabitants of an inductive type
are the constructors, but it's just a syntax.

Mike

[Martin Escardo]

In this sense, it is completely acceptable, as happens in the cubical
model, that the "computation rule" for J is replaced by a path. Then no
"matching with refl" is taking place.

The type of J is still the good old induction principle for Id. It is
just that in this model one computes in a different way, which is not by
term reduction.

Can we get a type theory adapted to the cubical model (a "cubical type
theory") where computation in the cubical model can be emulated
syntactically in the type theory?

Martin

[Thomas Streicher]

I have no reason to doubt that the way you, Thierry, have organized
the cubical set model the J-rule its evaluation rule doesn't hold
judgementally.

But I would expect otherwise for the following reason. As clarified by
Cisinski, Shulman et.al. presentable lcc \infty-categories do
correspond to right proper Cisinski model structures. For the latter I
think one can always build a model of type theory just as I did it for
simplicial sets. That means I have a construction of a universe there
("`a la Hofmann and Streicher" if I my say so). And there I also can
interpret idenity types by factoring the diagonal into an anodyne
cofibration followed by a fibration.

My question now is whether

a) cubical sets are not a right proper Cisinski model structure OR
b) the Kan condition of Thierry is different from the one of the
Cisinski model structure.

Presumably, the answeris b) ?

Thomas

[Thierry Coquand]

I am not sure if this is an answer to your question but if you are in a
classical metatheory one can do reasoning by case whether a cube
is degenerate or not and define then an "interpretation" of J with
evaluation rule holding judgmentally.
So I would expect that in a classical metatheory, we don't see the difference
between our notion of Kan cubical sets and the one of Cisinski.
(And in a classical metatheory, our work can be seen as a nonstandard
presentation of this model, where use of classical reasoning is minimized.)
Thierry

[Thomas Streicher]

Thanks, that's very clear!

Thomas

[Michael Shulman]

Put differently, writing "match loop with | refl => A end" is no
weirder than -- in fact, it is exactly as weird as -- writing "match
(loop^2) with | base => A | loop => B end". In both cases you can
define a function by matching against the generators, but the higher
nature of types means there is more in the resulting type than just
the generators. So I don't see a principled or philosophical reason
why the computation rules for matching against base or loop are more
(or less) deserving of being judgmental than the computation rule for
matching against refl.

I *am* very sympathetic to the argument that judgmental computation
for loop makes many formalizations much more feasible. I just find it
interesting that that particular rule seems to be so tricky to achieve
in models. I believe we have it in the simplicial model, but only for
a special version of "ap" that is propositionally, but not
judgmentally, equal to the usual one defined from J; thus if we use
the ordinary "ap" then the computation rule for loop is only
propositional.

[Michael Shulman]

On Wed, Jan 22, 2014 at 8:06 AM, Thomas Streicher
<stre...@mathematik.tu-darmstadt.de> wrote:
> As clarified by Cisinski, Shulman et.al. presentable lcc
> \infty-categories do correspond to right proper Cisinski model
> structures. For the latter I think one can always build a model of
> type theory just as I did it for simplicial sets.

I don't think the same construction of a universe always works. The
"Hofmann-Streicher universe" always exists in any presheaf category,
but it may not be a fibrant object in the model structure.

One can obtain a model of type theory from any right proper Cisinski
model structures by using the "local universes" construction of
Lumsdaine and Warren, but this type theory doesn't necessarily contain
a (strict) universe.

Mike

[Marc Bezem]

Dear All,

At the risk of stating the obvious, a crucial point in the cubical set model is:

IF we would use classical logic for an "interpretation" of J with the evaluation rule holding judgmentally,

THEN we can no longer compute with interpretations of terms (containing J).

Marc

[Martin Escardo]

Regarding Peter's analysis below, I now realize that my question is
not well posed.

The reason is that a closed term of ground type in TT doesn't
necessarily type-check in WTT (due to the lack of the computation rule
for J).

But every WTT term is a TT term. Then the question should be
formulated more accurately as: is there a closed WTT term of type N
which normalizes to 17 when considered as a TT term, but whose
interpretation is 13 in the cubical model?

The answer is no.

I repeat my understanding of Vladimir's argument (08/Jan/14,1:32GMT),
reformulated in light of Peter's observations:

* Let t:N be a closed WTT, and hence TT, term.

* Let [[t]] stand for the cubical interpretation of t.

* If t normalizes to n in TT, then there is a path from [[t]] to
[[n]] in the model.

The reason is that for any reduction t->t' in TT, either [[t]] is
[[t']] (when the reduction doesn't mention the computation rule for
J) or else there is a path from [[t]] to [[t']] (when the reduction
is by the computation rule for J). So, in any case, there is a path
from [[t]] to [[t']].

* But, by the nature of [[N]] in cubical sets (it is an hset), if
there is a path from [[t]] to [[n]], then [[t]] is [[n]].

* Hence if t normalizes to n in TT, then the cubical interpretation
of [[t]] is n (or [[n]] to be pedantic).

* Because TT is strongly normalizing, the converse also holds: if the
cubical interpretation of t is n, then t normalizes to n.

This shows that a closed WTT term of type N normalizes to n according
to the Martin-Loef computation rules of TT if and only if its
interpretation in cubical sets is n.

So "computational adequacy" does hold for WTT terms under the cubical
semantics. For TT terms, the question doesn't make sense, because
there is no cubical interpretation for them (at least a priori).

(The theory actually considered by Thierry et al is incomparable with
TT: it lacks the judgemental rule for J, but has judgemental
equalities not available in TT, and hence is stronger than WTT.)

Martin


On 21/01/14 17:05, Peter LeFanu Lumsdaine wrote:
> (Apologies for re-awakening sleeping dogs — but I hope this will help
> those who, like me, were left rather confused and uncertain by this thread.)
>
> I just had a discussion with Per Martin-Löf that left me with (I think!)
> a much better understanding of what’s going on in the cubical model —
> and in particular, a satisfactory answer to Martin’s question above, “is
> it possible to have a term t:Nat which normalises to the numeral [17]
> but which is interpreted in the cubical model as 13?”
>
> As previously explained by Thierry, the issue is that the Id-comp rule
> is modeled only as a path, not as strict equality. I had
> (mis)understood this as meaning that the paper shows:
>
> “The cubical model is a weak model of (ordinary Martin-Löf) type theory.”
>
> and so I was confused, because I wasn’t sure precisely what a weak model
> meant, or what consequences one could draw from it. Instead, though,
> what the paper quite un-problematically shows is that:
> , let's call it "cub"
as the files have the suffix ".cub" in their implementation,
> “The cubical model is a (genuine, strict) model of a slightly weaker
> type theory.”
>
> where the type theory being modeled (call it WTT for now) is obtained
> from the usual type theory (call it TT) by removing the Id-comp rule,
> and replacing it with just a propositional equality.
>
> So we certainly know: if *in WTT*, we have a term t:Nat which normalises
> (or, more generally, is propositionally equal) to [17], then the
> interpretation of t in the cubical model will be 17.
>
> On the other hand, if we just know that in ordinary TT our term t
> normalises to [17], then we don’t know what will happen to t in the
> model unless we can somehow lift the normalisation to a proof of
> equality in WTT. However (as the cubical paper mentions) Nils Anders
> Danielsson has done a fair bit of exploration in Agda, coding up the
> fundamentals of HoTT without assuming (iirc) the reduction rules for
> *any* inductive types, showing that in practice, proofs in TT can be
> lifted to proofs in WTT. This gives heuristic evidence for something like
>
> Conjecture: TT is conservative over WTT.
>
> If this holds, then we’d have a positive answer to Martins question —
> given a term t:Nat in WTT that normalises in TT to [17], conservativity
> says that we can lift the TT term |- refl(t) : Id(t,[17]) to a proof in
> WTT |- p : Id(t,[17]), and so conclude that in the cubical model, t is
> interpreted as 17. This would also then give a precise sense in which
> the cubical model is a weak model of the full type theory TT.
>
> I’ve been vague in all this about exactly what TT/WTT should be. For
> the conservativity to be plausible, they certainly need functional
> extensionality, since without it a lambda-abstracted version of the
> Id-comp rule gives an easy counterexample. Given that, it seems like
> they could reasonably also include anything that’s modeled (possible
> weakly) by the cubical model; and, Nils’ explorations suggest, WTT could
> weaken all iota-reductions to propositional equalities.
>
> Apologies to NAD and the cubical experts if I’m still misunderstanding
> or misrepresenting anything of their work — hopefully I’m not and this
> all makes sense…
>
> –p.
>
>
> , let's call it "cub"
as the files have the suffix ".cub" in their implementation,
>
> On Thu, Jan 16, 2014 at 6:36 PM, Thierry Coquand
> <Thierry...@cse.gu.se <mailto:Thierry...@cse.gu.se>> wrote:
>
>
> On Jan 11, 2014, at 4:29 PM, Vladimir Voevodsky wrote:
>
> > Hmmm... so in this branch the type checker is allowed to use your
> new ``cubical reductions" but is not allowed to use iota-reduction
> for Id-types?
> >
> >
> > V.
>
> Exactly. Besides having new conversion rules for mapOnPaths, we also
> have
> (now in the master branch of the github repository)
>
> -introduced a new type of "dependent equality" or dependent path
>
> IdP A B P a b
>
> for P : Id U A B and a:A, b:B. Using this new type construction,
> one can define
> the notion of "dependent path"
>
> IdD A F a0 a1 p b0 b1 for A:U, F:A-> U, a0 a1:A, p : Id A a0
> a1, b0 : F a0, b1:F a1, let's call it "cub"
as the files have the suffix ".cub" in their implementation,
>
> IdD A F a0 a1 p b0 b1 = IdP (F a0) (F a1) (mapOnPaths F a0 a1 p) b0 b1
>
> mentioned in Remarks 6.2.1, 6.2.3 in the book. This satisfies the
> definitional equality
>
> IdP A A (refl U A) a0 a1 = Id A a0 a1
>
> -an extension of mapOnPaths for dependent types
>
> mapOnPaths A F f a0 a1 p : IdD A F a0 a1 p (f a0) (f a1)
> if f : (x:A) -> F x
>
> and a simpler way to express equality on a sigma type, with good
> behavior w.r.t. mapOnPaths
>
> -introduced the circle S1 so that, using the notation of Lemma
> 6.2.5 in the book, both
> equations
>
> f base = a
> mapOnPaths f loop = p
>
> are definitional. It is then possible to define the helix and
> -compute- the winding number of
> an element of Id S1 base base
>
> Anders, Cyril, Simon, 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

> <mailto:HomotopyTypeTheory%2Bunsu...@googlegroups.com>.

[Dan Licata]

Hi Martin,

I agree with your summary up until

On Jan23, Martin Escardo wrote:
> * Because TT is strongly normalizing, the converse also holds: if the
> cubical interpretation of t is n, then t normalizes to n.

I don't see why strong normalization implies that. Could you elaborate?
E.g. WTT extended with the univalence axiom is strongly normalizing, has
a cubical interpretation, but does not have the property that if the

cubical interpretation of t is n, then t normalizes to n.

Also, I think it's important to note that by WTT here you mean WTT
without univalence, right? The rest of the argument applies to WTT with
univalence,

> This shows that a closed WTT term of type N normalizes to n according
> to the Martin-Loef computation rules of TT if and only if its
> interpretation in cubical sets is n.

By WTT here you mean WTT without univalence, right? The only if
(soundness) direction applies to WTT with univalence.

Thanks!
-Dan

[Martin Escardo]

On 23/01/14 03:41, Dan Licata wrote:
>
> I agree with your summary up until
>
> On Jan23, Martin Escardo wrote:
>> * Because TT is strongly normalizing, the converse also holds: if the
>> cubical interpretation of t is n, then t normalizes to n.
>
> I don't see why strong normalization implies that.

Because TT has the canonicity property: Every closed, normal TT term
of ground type is a numeral.

> Could you elaborate?

Suppose that [[t]]=[[n]] and that t normalizes to m in TT, where n and
m are numerals. We want to know that m=n.

By the argument you accepted, [[t]]=[[m]]. By transitivity,
[[m]]=[[n]]. By the nature of [[N]], we have that m=n, as required.

Martin

PS. Yes, my original question was, for a closed term of ground type
that doesn't use univalence, whether the cubical interpretation gives
the number corresponding to the numeral produced by normalization of
the term. Of course, with univalence, the normal form is not
canonical. But, as I said in my previous message, and spotted by
Peter, it is not enough to remove univalence to have a well posed
question. We also need to consider WTT rather than TT.)

[Vladimir Voevodsky]

Thank you Peter. This is helpful! V.

On Jan 21, 2014, at 12:05 PM, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com> wrote:

(Apologies for re-awakening sleeping dogs — but I hope this will help those who, like me, were left rather confused and uncertain by this thread.)

I just had a discussion with Per Martin-Löf that left me with (I think!) a much better understanding of what’s going on in the cubical model — and in particular, a satisfactory answer to Martin’s question above, “is it possible to have a term t:Nat which normalises to the numeral [17] but which is interpreted in the cubical model as 13?”

As previously explained by Thierry, the issue is that the Id-comp rule is modeled only as a path, not as strict equality.  I had (mis)understood this as meaning that the paper shows:

“The cubical model is a weak model of (ordinary Martin-Löf) type theory.”

and so I was confused, because I wasn’t sure precisely what a weak model meant, or what consequences one could draw from it.  Instead, though, what the paper quite un-problematically shows is that:

“The cubical model is a (genuine, strict) model of a slightly weaker type theory.”

where the type theory being modeled (call it WTT for now) is obtained from the usual type theory (call it TT) by removing the Id-comp rule, and replacing it with just a propositional equality.

So we certainly know: if *in WTT*, we have a term t:Nat which normalises (or, more generally, is propositionally equal) to [17], then the interpretation of t in the cubical model will be 17.

On the other hand, if we just know that in ordinary TT our term t normalises to [17], then we don’t know what will happen to t in the model unless we can somehow lift the normalisation to a proof of equality in WTT.  However (as the cubical paper mentions) Nils Anders Danielsson has done a fair bit of exploration in Agda, coding up the fundamentals of HoTT without assuming (iirc) the reduction rules for *any* inductive types, showing that in practice, proofs in TT can be lifted to proofs in WTT.  This gives heuristic evidence for something like

Conjecture: TT is conservative over WTT.

If this holds, then we’d have a positive answer to Martins question — given a term t:Nat in WTT that normalises in TT to [17], conservativity says that we can lift the TT term |- refl(t) : Id(t,[17]) to a proof in WTT |- p : Id(t,[17]), and so conclude that in the cubical model, t is interpreted as 17.  This would also then give a precise sense in which the cubical model is a weak model of the full type theory TT.

I’ve been vague in all this about exactly what TT/WTT should be.  For the conservativity to be plausible, they certainly need functional extensionality, since without it a lambda-abstracted version of the Id-comp rule gives an easy counterexample.  Given that, it seems like they could reasonably also include anything that’s modeled (possible weakly) by the cubical model; and, Nils’ explorations suggest, WTT could weaken all iota-reductions to propositional equalities.

Apologies to NAD and the cubical experts if I’m still misunderstanding or misrepresenting anything of their work — hopefully I’m not and this all makes sense…

–p.

On Thu, Jan 16, 2014 at 6:36 PM, Thierry Coquand <Thierry...@cse.gu.se> wrote:

On Jan 11, 2014, at 4:29 PM, Vladimir Voevodsky wrote:

> Hmmm... so in this branch the type checker is allowed to use your new ``cubical reductions" but is not allowed to use iota-reduction for Id-types?
>
>
> V.

Exactly. Besides having new conversion rules for mapOnPaths, we also have
(now in the master branch of the github repository)

-introduced a new type of "dependent equality" or dependent path

IdP A B  P   a   b

for P : Id U A B   and a:A, b:B.  Using this new type construction, one can define
the notion of "dependent path"

 IdD A F a0 a1 p b0 b1    for A:U, F:A-> U, a0 a1:A, p : Id A a0 a1, b0 : F a0, b1:F a1

 IdD A F a0 a1 p b0 b1 = IdP (F a0) (F a1) (mapOnPaths F a0 a1 p) b0 b1

mentioned in Remarks 6.2.1, 6.2.3 in the book. This satisfies the definitional equality

  IdP A A (refl U A) a0 a1 = Id A a0 a1

-an extension of mapOnPaths for dependent types

 mapOnPaths A F f  a0 a1 p :   IdD A F a0 a1 p (f a0) (f a1)      if   f : (x:A) -> F x

and a simpler way to express equality on a sigma type, with good behavior w.r.t. mapOnPaths

-introduced  the circle S1 so that, using the notation of Lemma 6.2.5 in the book, both
equations

  f base                         = a
  mapOnPaths f loop = p

are definitional. It is then possible to define the helix and  -compute- the winding number of
an element of Id S1 base base

Anders, Cyril, Simon, 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/groups/opt_out.

[Martin Escardo]

On 23/01/14 00:10, Martin Escardo wrote:
> * If t normalizes to n in TT, then there is a path from [[t]] to
> [[n]] in the model.
>
> The reason is that for any reduction t->t' in TT, either [[t]] is
> [[t']] (when the reduction doesn't mention the computation rule for
> J) or else there is a path from [[t]] to [[t']] (when the reduction
> is by the computation rule for J). So, in any case, there is a path
> from [[t]] to [[t']].

It is important here that is t is a closed term of ground type in WTT,
which reduces to t' according to the rules of TT (not just WTT), then
t' is also a WTT term.

Martin

[Thierry Coquand]

Now that we have a name for the theory

WTT = TT - Identity type (but with Nat, List, Bool, W,…)
+ a type Path A a0 a1 satisfying the laws of Id with computation rule
expressed as a propositional equality

one can state

the cubical set model is a model of WTT + the Axiom of Univalence

We know also that

if t is a closed term of type Nat of WTT (so, it does use the Axiom of Univalence)
and t --> S^n(0) then t evaluates to n for the cubical evaluation


I believe that it should also be possible to show (variation of Vladimir's conjecture
but for WTT)

if t is a closed term of type Nat of WTT + the Axiom of Univalence, then t evaluates
to a numeral n in the cubical model and there is a proof in WTT + the Axiom of Univalence
of Path Nat t S^n(0)

the idea being that one could represent in WTT + the Axiom of Univalence the
notion of cube and interpret each step of the cubical evaluation as a propositional
equality in WTT + the Axiom of Univalence.

Thierry


PS: in this computational analysis of Path, where refl is not a constructor, (and furthermore
in the model it is not decidable if an element is of the form refl) one cannot expect the evaluation rule
for J to be a computation rule. However, it may still hold as a definitional equality. For the cubical
set model as it is now, it does not hold for the universe, where the Kan operation for
the universe is essentially composition of relation
and we don't have that the composition of a relation R with the identity relation is definitionally
equal with R.
An example of definitional equality that holds in the cubical model but are not computation rules are
the equality for ap/mapOnPaths

ap (\ x -> x) p = p ap f (refl u) = refl (f u)

[Peter LeFanu Lumsdaine]

Is this clear?  Suppose the reduction is a deep Id-comp, in some sub-term s of t.  From the point of view of WTT, we have replaced an arbitrary (not necessarily abstractable) sub-term of t with a not-definitionally-equal term s'.  Why should the resulting t' still typecheck? 

–p.

[Thierry Coquand]

 Yes this is not clear.

 Maybe the result should be stated as

 If t is a closed term of type Nat in WTT + the Axiom of Univalence and we

have a closed term  in Path Nat t S^n(0)   then t evaluates to n 

for the cubical evaluation

 Thierry

[Martin Escardo]

On 23/01/14 10:17, Peter LeFanu Lumsdaine wrote:
>
> On Thu, Jan 23, 2014 at 10:35 AM, Martin Escardo
> <m.es...@cs.bham.ac.uk <mailto:m.es...@cs.bham.ac.uk>> wrote:
>
>
> On 23/01/14 00:10, Martin Escardo wrote:
>
> * If t normalizes to n in TT, then there is a path from [[t]] to
> [[n]] in the model.
>
> The reason is that for any reduction t->t' in TT, either
> [[t]] is
> [[t']] (when the reduction doesn't mention the computation
> rule for
> J) or else there is a path from [[t]] to [[t']] (when the
> reduction
> is by the computation rule for J). So, in any case, there
> is a path
> from [[t]] to [[t']].
>
>
> It is important here that is t is a closed term of ground type in WTT,
> which reduces to t' according to the rules of TT (not just WTT), then
> t' is also a WTT term.

Yes, the argument breaks here. (Perhaps this can be rescued considering
big-step normalization `a la Altenkirch-Chapman, but I haven't given
enough thought to this.)

>
> Is this clear? Suppose the reduction is a deep Id-comp, in some
> sub-term s of t. From the point of view of WTT, we have replaced an
> arbitrary (not necessarily abstractable) sub-term of t with a
> not-definitionally-equal term s'. Why should the resulting t' still
> typecheck?

Martin

[Martin Escardo]

>> * If t normalizes to n in TT, then there is a path from
>> [[t]] to [[n]] in the model.
>>
>> The reason is that for any reduction t->t' in TT, either
>> [[t]] is [[t']] (when the reduction doesn't mention the
>> computation rule for J) or else there is a path from [[t]]
>> to [[t']] (when the reduction is by the computation rule
>> for J). So, in any case, there is a path
>> from [[t]] to [[t']].
>>

>> It is important here that if t is a closed term of ground type

>> in WTT, which reduces to t' according to the rules of TT (not
>> just WTT), then t' is also a WTT term.
>

> the argument breaks here.

So, for the record, the 17-13 problem remains unsolved.

For all we know so far, it is in principle possible that there is a
WTT closed term of ground type which, when considered as a TT term,
normalizes to the numeral 17, under Martin-Loef's reductions
(including the computation rule for J), but whose cubical
interpretation is 13.

Of course, this shouldn't be the case, but we don't know.

The conjecture ("computational adequacy" of the cubical model of WTT
with respect to the operational semantics of TT) is that a WTT closed
term t:N normalizes under TT-reductions to a numeral n if and only if
the cubical interpretation of t is (the cubical interpretation of) n.

A positive solution to this conjecture is equivalent to a negative
solution to the 17-13 problem.

I think this (namely computational adequacy) is a minimal criterion
for the correctness of the cubical model of WTT.

Martin

[Michael Shulman]

We spent a while last year trying to fit HITs into the native syntax
of Coq, without much success. Part of the problem is that Coq's match
syntax supports deep nested matches, and it's hard to make sense of
those for an HIT.

If you're just talking about MLTT in Coq syntax, then one can of
course add whatever judgmental equalities are desired, and the result
makes perfect sense as mathematics. But I don't think it's at all
trivial to carefully specify an algorithm which computes with such
equalities and show that it terminates. However, I'd love to be
proven wrong.

[Vladimir Voevodsky]

On Jan 21, 2014, at 2:18 PM, Michael Shulman <shu...@sandiego.edu> wrote:

> On Tue, Jan 21, 2014 at 10:06 AM, Thierry Coquand
> <Thierry...@cse.gu.se> wrote:
>> f base = a
>> ap f loop = p
>>
>> only the first equation is validated definitionally, while the second holds only as a propositional equality.
>
> Very interesting! I wonder whether it is a coincidence that so many
> different factors seem to point to this sort of thing being the
> "right" choice for the computation rules of a HIT, or if there is some
> deeper reason for it.

What is an example of another reason for this choice?

V.

[Vladimir Voevodsky]

I have the idea of introducing something which I called tfc-terms (from trivial fibration-cofibration). One of the possible formats is as follows:

Gamma |- f : Prod x : T,  T'

Gamma |-  t : T

Gamma |- p : T' [ t / x ]

Gamma |- e : Id ( f t ) p 

-----------------------------------

Gamma |- tfc ( f , t, p, e ) : Prod x : T , T'

with the computation rule

Gamma | tfc(f, t, p, e) t reduces to p .

In other words given a (dependent) function and a point in the fiber of the family propositionally equal to the value of the function we get a new function which is definitionally equal to this point in this fiber.

This would be very convenient for the theory of set-questions constructed in Foundations and possible elsewhere.

A more or less equivalent thing would be to provide means to find a contraction for every contractible type which is definitionally trivial at the center of the contraction. 

Homotopy-theoretically it corresponds to declaring sections of fibrations to be cofibrations.

It seems that addition of such constructors should make it possible to "fix" the issues for J and S^1.

Thierry?

V.

On Jan 21, 2014, at 3:27 PM, Thierry Coquand <Thierry...@cse.gu.se> wrote:

 In the cubical set model as we have now, we can only validate the second rule propositionally.

 It would indeed be nice to have a model where it holds in a definitional way.

 Thierry

 

On Jan 21, 2014, at 9:21 PM, Guillaume Brunerie wrote:

Thierry, could you be more specific? Is it in the cubical model that the second rule only holds propositionally or is just in the syntax that it's somehow problematic to assume it?
Because I completely disagree with Mike, both computation rules should definitely be definitional (but I can understand that hacking it into the syntax of MLTT could be problematic).

Guillaume

[Michael Shulman]

On Thu, Jan 23, 2014 at 10:13 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
>> Very interesting! I wonder whether it is a coincidence that so many
>> different factors seem to point to this sort of thing being the
>> "right" choice for the computation rules of a HIT, or if there is some
>> deeper reason for it.
>
> What is an example of another reason for this choice?

Here are a few:

* It's what we get in the cubical model.

* It's what we get in the simplicial model (and other models in
simplicial presheaves) if we insist that "ap" means the version
defined via J.

* It's possible to "implement" in existing proof assistants using
private inductive types.

* It's what we get if we reduce higher paths to 1-paths using hubs and spokes.

[Vladimir Voevodsky]

On Jan 23, 2014, at 4:54 AM, Thierry Coquand <Thierry...@cse.gu.se> wrote:

one cannot expect the evaluation rule
for J to be a computation rule. However, it may still hold as a definitional equality. 

Interesting. It might make sense to distinguish the two, but I am not sure why would you not want to consider this definitional equality for J to be a computation rule?

V.

[Thierry Coquand]

one cannot expect the evaluation rule

for J to be a computation rule. However, it may still hold as a definitional equality. 

Interesting. It might make sense to distinguish the two, but I am not sure why would you not want to consider this definitional equality for J to be a computation rule?

 What I should have written is that it would not be a computation rule in the sense of

unfolding definitions. 

 In the present evaluator all computation steps correspond to unfolding definitions of the various operations.

All these definitions are done in a constructive metatheory (they are all uniform; no definition

by cases on undecidable statements). 

 For the example

 coerce : (A B : U) -> Id U A B -> A -> B

(which is simpler than J, but the issue is the same) we have that

 coerce p a

is defined in the following way

  p represents a path p(x)   between A and B

  coerce p a   is defined to be the Kan composition operation corresponding 

to this path for the generic Kan fibration X (X:U) over U and for a:A

 The Kan filling and composition operations are defined by induction on the type

structure.

 In the model, it is not possible to decide if this path p(x) is constant or not, so we

cannot define   coerce p a     by case whether p is a constant path or not.

 

 In  the case however where  p(x) happens to be the constant path, do we 

have that this Kan composition coerce p a is equal to a?? (If this would be the case

we should be able to add the equality   coerce p a = a  for p constant)

 More generally if we fill an open box which 

is constant in its "principal" direction do we obtain a filling which is constant

in this direction?

 Unfortunately, this does not hold the way the Kan filling are defined for the universe, essentially

because they are defined by composing relations, and the composition of a relation R

with the identity relation is not the same as R.

 One may argue that one could change the definition of composition of relation in order to force

this equality. It is not clear  if this can be done in a consistent way. (One has

then to check preservation w.r.t. dependent product which forces new equalities…)

 Thierry

 

 

[Jason Gross]

I see.  So the problem is that for nested matches where the inner match is on a HIT, you need some syntax for the "ap <outter constructor> <inner path>" case, and it's not quite clear what the syntax for that should be; and also when the outer match is on a HIT, you need to desugar the inner match when specifying the return type of the outer match on a path.  Still, it doesn't seem to be a fatal flaw, and I'd be fine with just disallowing nested matches on HITs, or using "fixmatch" like Bruno Barras does in his branch and disallowing deep nesting when using fixmatch.  Were there other problems?

I don't know how the proof of beta-iota reduction termination goes for Coq (can anyone point me at a reference?), so I don't have a deep understanding of how to extend it for HITs.  (I think that delta-zeta reduction is unproblematic because it can be applied all at once and not again).  However, I suspect that any rules which strictly reduce the number of "match"es in the goal (and don't introduce any genuinely new terms?) will work similarly to the iota proof.  Especially in the case of 

 match x return A with

   | constructor => a

 end

 ≡ a

this is just iota reduction in cases when x is not already a constructor (and it's clear that it doesn't break well-typedness), and I don't see how the proof of iota-reduction termination could use the fact that x is genuinely a constructor.  It's less clear in the case of my other rule, but it still seems iota-like to me.  I'll try to see if I can find the termination proof for Coq, and see if I can extend it to this case.

-Jason  

[Vladimir Voevodsky]

On Jan 24, 2014, at 8:59 AM, Thierry Coquand <Thierry...@cse.gu.se> wrote:

 Unfortunately, this does not hold the way the Kan filling are defined for the universe, essentially

because they are defined by composing relations, and the composition of a relation R

with the identity relation is not the same as R.

What is the definition of composition of relations?

V.

PS Is (coerce idpath) an idempotent?

[Michael Shulman]

I always thought fixmatch was the way to go. I'm not up to date on what Bruno has been doing, though.

I'd be interested to see if standard termination proofs can be adapted to HITs. I don't know whether anyone has worked on this specifically -- attention seems to be more focused on univalence with HITs perhaps included, which is reasonable since for all the homotopy applications of HITs you need univalence too.

[Jason Gross]

Bruno hasn't tocuhed https://github.com/barras/coq/tree/hit for ~5 months (since around the Barcelona HoTT conference), so I don't know what he's been doing since then.  But in that branch, he already has fixmatch and some computation rules, so you can do something like " Inductive Interval := | zero : Interval | one : Interval with paths := | seg : zero = one." and prove functional extensionality from that.

I'll look in to the termination proofs used for Coq, and see if I can work more rules into them for HITs, when I get a chance.

-Jason