Propositional or definitional in exercises 5.2, 5.3? #639

Closed
JasonGross opened this Issue Feb 26, 2014 · 18 comments

Projects

None yet

5 participants

@JasonGross
Contributor

It's not clear to me whether "satisfy a recurrence" in exercises 5.2 and 5.3 means that the computation rules have to hold prepositionally, or definitionally. If the latter, I can see how to do 5.2 iff the uniqueness principle for nat is only propositional and not judgmental.

@kristinas
Contributor

I think I was the one who put in the exercise. What I had in mind was showing n + 1 = 1 + n. Both of these functions satisfy the same recurrence (1,s) definitionally. But now I realized I am not sure whether the fact that these are not definitionally equal is mentioned in the book - although it probably should be since this is a major problem for things like simplicial sets, according to my understanding.

@mikeshulman
Contributor

I hope that nothing in the book gave you the impression that the uniqueness principle for nat was judgmental.

@JasonGross
Contributor

@mikeshulman no, nothing in the book. I also think I got the name wrong. Is there a name for the rule

match n with
 | 0 => 0
 | S p => S p
end = n

? (equivalently, n = nat_rect (fun _ => nat) 0 (fun _ => S) n)
I was doing the exercises in Coq, and I've been pushing for these rules to be judgmental for all types in Coq (I've called them eta rules before, but then people seem to think that I'm saying that every nat is judgmentally either zero or a successor, which isn't what I'm saying. And I want this rule for equality, too (it's provable propositionally, but I want it judgmentally). But there doesn't seem to be any other name for them, so maybe I should call the half-eta rules?). I didn't want to use an example that stops working at some point.

Should the book mention "definitionally" for this exercise? The example I came up with used maps to Bool, and said that fun _ => true and nat_rect (fun _ => Bool) true (fun _ x => x) (i.e., f 0 = true and f (S p) = f p) are propositionally equal but not judgmentally equal. This seems a bit more robust, because, e.g., CoqMT makes n + 1 and 1 + n judgmentally equal.

Are there any examples where we can derive a contradiction with univalence from a judgmental equality of functions which are known to satisfy the same recurrence judgmentally? (either out of nat or out of something more complicated?)

@mikeshulman
Contributor

I don't know a standard name for this rule; it's certainly only a special case of the general eta rule / uniqueness principle. Maybe "weak eta"? Ask a type theorist (i.e. not me).

Univalence certainly doesn't contradict this judgmental rule for nat, since it holds in the simplicial set model (in which nat is a "strict 0-type"). However, there are also desired homotopical models in which it doesn't hold judgmentally even for nat, so I would argue strongly against adding it to any proof assistant. Whether it's consistent with univalence to suppose it for identity types is an interesting question; I don't think that that one holds even in the simplicial model.

@JasonGross
Contributor

You mean "whether it's consistent with univalence to suppose it judgmentally for identity types"? Are there any models in which symmetry is judgmentally involutive (i.e., eq_sym (eq_sym p) = p judgmentally)?

@JasonGross
Contributor

I think my position is roughly "how much is judgmental should be left up to the user". I like things judgmental equalities because it makes proving things easier and sometimes faster.

@mikeshulman
Contributor

Supposing a contradiction makes proving things especially easy and fast. (-: Making equalities judgmental isn't something you can just do willy-nilly; you have to think about whether it matches the intended models.

I don't know any homotopical models in which symmetric is "naturally" judgmentally involutive, but it's possible one could make it be so by making some careful arbitrary choices. I haven't tried.

@mikeshulman
Contributor

Anyway, as for the book, we should certainly clarify this point.

@kristinas
Contributor

To come back to my earlier question: Is there a place in the book where we discuss that n + 1 is not judgmentally equal to 1 + n?

@mikeshulman
Contributor

I don't see one.

I'm wary of putting too much emphasis on this, as I think it looks kind of weirdo to a newcomer to type theory. So e.g. I'd like to try to avoid mentioning it in chapter 1 or 2.

@awodey
Contributor
awodey commented Feb 26, 2014

it’s actually a good motivation for identity types, because it shows how they can be used to prove things by induction that can’t be proved just definitionally.

On Feb 26, 2014, at 4:32 PM, Mike Shulman notifications@github.com wrote:

I don't see one.

I'm wary of putting too much emphasis on this, as I think it looks kind of weirdo to a newcomer to type theory. So e.g. I'd like to try to avoid mentioning it in chapter 1 or 2.


Reply to this email directly or view it on GitHub.

@martinescardo
Contributor

On 26/02/14 21:32, Mike Shulman wrote:

I don't see one.

I'm wary of putting too much emphasis on this, as I think it looks kind
of weirdo to a newcomer to type theory. So e.g. I'd like to try to avoid
mentioning it in chapter 1 or 2.

This is weird, and is one of the first things people get stuck with when
they try Coq or Agda. Precisely because of this it should be explained
rather than hidden, I think. One has to prove that 1+n=n+1, and use
transport with this often. And this is not an isolated phenomenon. But I
am not saying it should (not) be in Chapters 1 or 2. I am saying that to
be able to use type theory we should be aware of this, and how to deal
with it.

Martin

@mikeshulman
Contributor

Okay, those are good points. Maybe what I'm afraid of can be avoided by using this opportunity to emphasize that we shouldn't expect this to be judgmental; propositional equality is the real "equality of mathematics", with judgmental equality being a more or less metatheoretic thing that makes our lives easier?

@JasonGross
Contributor

I think judgmental equality is not just to make our lives easier (though, for me, that's certainly our primary purpose); that's part of why I like Voevodsky's proposal to have types for both propositional and judgmental equality.

@martinescardo
Contributor

On 26/02/14 21:58, Mike Shulman wrote:

Okay, those are good points. Maybe what I'm afraid of can be avoided by
using this opportunity to emphasize that we shouldn't /expect/ this to
be judgmental;

I agree. But actually most people expect (wrongly you may say) n+1 to be
the same as 1+n in the sense of being interchangeable, because this is
what they are used to.

propositional equality is the real "equality of
mathematics", with judgmental equality being a more or less
metatheoretic thing that makes our lives easier?

(This is not the place to discuss this, I guess. I agree with you,
modulo the question of whether it is possible to have a dependent type
theory without judgemental equality. If not, then it is more than mere
convenience.)

Martin

@kristinas
Contributor

Maybe the place to discuss n + 1 vs 1 + n would be when we introduce propositional uniqueness rules?

@awodey
Contributor
awodey commented Feb 26, 2014

I agree with this.
the “mathematical equality” is the propositional one — which equations are taken to be judgmental is more a matter of engineering and conventions (see the choices that are made for HITs).

On Feb 26, 2014, at 4:58 PM, Mike Shulman notifications@github.com wrote:

Okay, those are good points. Maybe what I'm afraid of can be avoided by using this opportunity to emphasize that we shouldn't expect this to be judgmental; propositional equality is the real "equality of mathematics", with judgmental equality being a more or less metatheoretic thing that makes our lives easier?


Reply to this email directly or view it on GitHub.

@mikeshulman
Contributor

Note that I did not use the word "just". (-:

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