A.1 should include HoTT features #74

Closed
cangiuli opened this Issue Apr 5, 2013 · 20 comments

Projects

None yet

7 participants

Contributor
cangiuli commented Apr 5, 2013

The presentation of type theory in A.1 (of Peter and Thierry) does not mention univalence, definitional eta, or higher inductive types.

Contributor

A.2.15 mentions funext and univalence, A.2.12 does definitional eta for functions, and A.2.14 does a HIT, so I think this is done.

Member

Except Carlo opened it before the intro lost its number, so now the issue should be considered as referring to A.1.

@DanGrayson DanGrayson reopened this Apr 14, 2013
Member

Peter Aczel wants to deal with the issue by adding a statement that A.1 doesn't include any HoTT features.

Contributor
awodey commented Apr 14, 2013

Why not just add them?

Sent from my iPhone

On Apr 14, 2013, at 5:45 PM, "Daniel R. Grayson" notifications@github.com wrote:

Peter Aczel wants to deal with the issue by adding a statement that A.1 doesn't include any HoTT features.


Reply to this email directly or view it on GitHub.

Owner

But there is no point in repeating these twice. Let us just promote A.2.15 to A.3, i.e., make it its own section. Say in the first sentence of the section that these are given in the style of the second presentation. Actually, I am just going to do this.

Owner

Closed by b48deb7
This looks better. The table of contents now has a line saying "The axioms for HoTT" so people can actually like them.

Contributor

I don't quite like this solution because the presentation in "Axioms for HoTT" is dissimilar from the type theory presented in "The first presentation."

More importantly, "The first presentation" doesn't mention HITs. Since it isn't obvious to me the best way to integrate HITs into the first presentation (since elimination is done via pattern matching) I think Thierry or Peter need to make some remark about this.

@cangiuli cangiuli reopened this Apr 15, 2013
Contributor
awodey commented Apr 15, 2013

Good idea!

Sent from my iPhone

On Apr 14, 2013, at 7:08 PM, Andrej Bauer notifications@github.com wrote:

Closed by b48deb7
This looks better. The table of contents now has a line saying "The axioms for HoTT" so people can actually like them.


Reply to this email directly or view it on GitHub.

Contributor
awodey commented Apr 15, 2013

there can be a remark in the "intro" part that says the two sections of the appendix treat the "basic" theory in two different styles, and then the HoTT axioms are given in the third section, in the style of section 2. No reason to complicated things any further.

Contributor

@awodey: Sure, I'll do that. But I still think HITs should be discussed separately in each section?

Contributor
awodey commented Apr 15, 2013

why?
It's not necessary to do it twice (or three times), and Peter Aczel and Thierry have already said they prefer not to do it in theirs. So why not just do it once, in the third section, and not in the other two?

Contributor

See 911d119

I have added a sentence to clarify that the UA/funext presentation of A.3 works equally well for both A.1 and A.2.

I am satisfied now, but I'd just like to remark that the suitability of pattern-matching for HITs is not so clear, even to experts. If we don't want to broach the issue in A.1, that's fine, but it would be unfair to say (and the appendix currently does not say) that HITs also work equally well in both sections. Therefore, please do not move the circle to A.3.

@cangiuli cangiuli closed this Apr 15, 2013
Contributor

It seems to me that the sort of "pattern matching" described in A.1 is
really just the same sort of syntactic sugar for eliminators that we used
all throughout the book, which works just fine for HITs, modulo
propositionality of the rules for path-constructors. The more complicated
sort of deep pattern-matching that Coq and Agda allow for ordinary
inductive types is hard to make sense of for HITs, but we aren't mentioning
that anywhere in the book at all, are we?

Why would it be wrong to write in the style of A.1 that "if we have C : S1
-> U_m and b:C(base) and l:loop_*(b)=b, then we can introduce a defined
constant f:\prd{x:S1} C(x) with defining equations f(base)=b and
apd_f(loop)=l"? (Aside from the fact that it would destroy the nice
properties described in A.1.9.)

On Mon, Apr 15, 2013 at 12:25 AM, Carlo Angiuli notifications@github.comwrote:

See 911d119911d119

I have added a sentence to clarify that the UA/funext presentation of A.3
works equally well for both A.1 and A.2.

I am satisfied now, but I'd just like to remark that the suitability of
pattern-matching for HITs is not so clear, even to experts. If we don't
want to broach the issue in A.1, that's fine, but it would be unfair to say
(and the appendix currently does not say) that HITs also work equally well
in both sections. Therefore, please do not move the circle to A.3.


Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/74#issuecomment-16366889
.

Contributor

Yes, that was the kind of thing that I was hoping would be added to A.1, except that it would invalidate the claims of A.1.9, and so requires more work than just pasting in that text. But I get the impression that Peter and Thierry don't want the HoTT features in their section because it screws up the syntactic properties. (I disagree with this reasoning but that is why the issue is assigned to Thierry.)

Contributor

Well, if that's the point, then we should move A.2.14 into A.3: if we're claiming that the two presentations are equally good, then all the special HoTT features should treat them equally, either being discussed separately in both A.1 and A.2, or being discussed after both of them in A.3.

Contributor

But (1) A.2 doesn't have any operational semantics, unlike A.1, and (2) it's a bit more of a stretch to say that A.2.14 can be dropped into A.1 without further discussion.

I guess my point is that A.2+A.3 forms a coherent presentation of the HoTT we use in the book, while A.1+A.2.14+A.3 is not so internally consistent.

Contributor

But (1) we don't use any operational semantics in the book, so while this
is a nice feature of A.1 it's irrelevant, and (2) the point I was trying to
make is that I don't see why this should be.

On Mon, Apr 15, 2013 at 1:06 AM, Carlo Angiuli notifications@github.comwrote:

But (1) A.2 doesn't have any operational semantics, unlike A.1, and (2)
it's a bit more of a stretch to say that A.2.14 can be dropped into A.1
without further discussion.

I guess my point is that A.2+A.3 forms a coherent presentation of the HoTT
we use in the book, while A.1+A.2.14+A.3 is not so internally consistent.


Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/74#issuecomment-16367533
.

Contributor

The core feature of A.1 is that their notion of definitional equivalence is inherited from untyped operational semantics. Without that, A.1 is basically a reprisal of Chapter 1 with slightly more formal wording.

Maybe it would be easier to discuss this offline tomorrow. In principle I don't mind entirely factoring out the HoTT features as you suggest.

Owner

Let's not get too emotionally attached to who wrote what (i.e., delete one of the section if it doesn't fit). But I think it's good to have the two presentations.

We should place all the HoTT features into a separate section, as far as I am concerned. This makes sense from the organizational point of view. For example, Martin Escardo asked that we do such a thing, so he can have a look at what is different in the book from the standard setup. He's not going to care whether it is done twice, or in this or that style, he just wants to have one place where he can look at the special HoTT stuff. We can always explain (and should) in the notes how the special HoTT stuff relates to A.1 and A.2.

Contributor

I opened #128; I'll make some changes and then we can continue the discussion there.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment