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

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

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

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 ?

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…

eta lets you prove `(fun x => x) = (fun x => (x.1, x.2))`

(a very weak funext) so it's not conservative

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

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?

Should we try and invoke @Rafaël Bocquet ?

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 \times B$ and the metatheoretic product of $A$ and $B$).

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