Stream: Coq users

Topic: coq dosn't have eta or Am I missing something?


view this post on Zulip walker (Jan 29 2024 at 17:36):

Goal forall A B (t: (A * B)), t = (t.1, t.2).
Proof.
move => A B t.
Fail by [].

I thought this should have worked, what Am I missing?

Note: I know I can destruct t but I thought I can also do it without destruct.

view this post on Zulip Yann Leray (Jan 29 2024 at 17:38):

The product defined in the standard library doesn't have eta on projections, it is not declared with primitive projections which is the mechanism to add eta-laws on structures

view this post on Zulip Théo Winterhalter (Jan 29 2024 at 17:38):

η\eta for records isn't activated by default. You can do so with

Set Primitive Projections.

Note that this will only affect newly defined records. The prod of the standard library is stuck without η\eta.

view this post on Zulip walker (Jan 29 2024 at 17:42):

I see, It was just a matter of convenience for me, but now I am curious speaking of eta, does it add any logical power having eta from not having eta, or is it just convenience ?

view this post on Zulip Meven Lennon-Bertrand (Jan 29 2024 at 18:21):

Eta promotes a propositional equality into a definitional one. Thus, it is at most as strong as extensional type theory (ETT), which adds the rule that any propositional equality can be turned into a definitional one. However, ETT is not conservative over bare intentional type theory (ITT), because it proves function extensionality and uniqueness of identity proofs. The reason for this is that by adding definitional equalities, ETT makes more terms typable, including more proof terms. A standard result by Martin Hoffmann (refined by Théo and others) is that this is enough: ETT is conservative over ITT + funext + UIP, that is, any theorem provable in the former is also provable in the latter. But in the more general case where not all but merely some equalities are made definitional, the situation is less known. Rafaël Bocquet has some conservativity results, but they are quite complicated…

In the end, what is sure is that eta is at most as strong as ETT, which is itself as strong as ITT + funext + UIP. Since eta is compatible with univalence which contradicts UIP, eta alone is very likely much weaker than ETT (which seems intuitive), but I don't have good arguments for conservativity of eta for records. What I know is that eta for functions is crucial to prove that univalence implies funext (although I don't think there are any proofs that univalence does not imply funext in the absence of eta for functions, because nobody in their sane mind would try and construct a model of univalence where funext does not hold). So it might very well be the case that eta for records has some interesting consequences…

view this post on Zulip Gaëtan Gilbert (Jan 29 2024 at 18:28):

eta lets you prove (fun x => x) = (fun x => (x.1, x.2)) (a very weak funext) so it's not conservative

view this post on Zulip Gaëtan Gilbert (Jan 29 2024 at 18:28):

I don't know if there's anything more interesting you can get out of it though

view this post on Zulip Matthieu Sozeau (Feb 01 2024 at 17:19):

My gut feeling is that with funext you will have equivalence of definitional and propositional eta laws for unit and pairs. IIRC Raphael’s result gives that for unit, no?

view this post on Zulip Meven Lennon-Bertrand (Feb 01 2024 at 18:07):

Should we try and invoke @Rafaël Bocquet ?

view this post on Zulip Rafaël Bocquet (Feb 02 2024 at 20:27):

Matthieu Sozeau said:

My gut feeling is that with funext you will have equivalence of definitional and propositional eta laws for unit and pairs. IIRC Raphael’s result gives that for unit, no?

Yes, definitional eta should be conservative over propositional eta, as long as propositional eta is stated correctly (e.g. with propositional beta and eta for pairs, we should have a half-adjoint equivalence between A×BA \times B and the metatheoretic product of AA and BB).

I don't have any actual results yet for type theories without UIP. Valery Isaev has some result for unit in https://arxiv.org/abs/1804.05045, but the construction is hard to understand and does not scale to other type formers.

I just checked whether I was still missing some idea for actual results, and it seems that I now have everything (the last pieces of the puzzle being strict Rezk completions and the idea of working in cubical sets.)


Last updated: Jun 13 2024 at 21:01 UTC