Term can be constructed interactively, but not given explicitly. about coq HOT 5 CLOSED

this has happened to me, too; I decided to live with it; I suppose it really is a bug?

from coq.

It appears to be specific to HoTT/Coq, at least: Peter tried it with unmodified Coq this afternoon and it worked fine.

It seems to me like a bug if there is a term which cannot be written explicitly, or if there is a way to write it explicitly but Set Printing All does not give us that way.

from coq.

It seems unrelated to polymorphism, to me. Using the latest HoTT/coq, when typechecking:

Definition flip_P_is_retr1 : forall g, flip_P_inv (flip_P g) = g.

The equality is parsed as an @eq instead of @equals.
Using:
Infix "=" := equals : type_scope.

I get the right definition and both flip_P_is_retr1 and flip_P_is_retr2 work (whether or not [Set Universe Polymorphism] is set.

As for flip_P_is_retr3, using the right parentheses, it works for me:

Definition flip_P_is_retr3 : forall g, equals (flip_P_inv (flip_P g)) g
:=
((fun g : forall (a : A) (b : B), P a b =>
@refl (forall (a : A) (b : B), P a b) g)
: forall g : forall (a : A) (b : B), P a b,
@equals
(forall (b : A) (a : B),
@Flip A B (fun (_ : A) (_ : B) => Type) P a b)
(flip_P_inv (flip_P g)) g).

Maybe I'm not reproducing the same behavior here.

from coq.

It works for me now too (with the right parentheses)!

from coq.

No longer relevant, closing.

from coq.