Code attachment for [this issue](https://github.com/HoTT/coq/issues/19) on [HoTT/coq](https://github.com/HoTT/coq)

Term that cannot be given explicitly

Inductive equals {A : Type} (a : A) : A -> Type :=
  refl : equals a a.

Arguments refl {A a} , [A] a.

Notation "x = y" := (equals x y).

Definition flip {A B : Type} {P : A -> B -> Type}
  : (forall a b, P a b) -> (forall b a, P a b)
  := fun f b a => f a b.

Variables (A B : Type) (P : A -> B -> Type).

Let flip_P := @flip _ _ P.
Let flip_P_inv := @flip _ _ (flip P).

Set Printing All.
Set Printing Universes.

(* Succeeds: *)
Definition flip_P_is_retr1 : forall g, flip_P_inv (flip_P g) = g.
Proof.
  intro g.  unfold flip_P, flip_P_inv, flip.  exact (refl g).
Defined.

(* Fails: *)
Definition flip_P_is_retr2 : forall g, flip_P_inv (flip_P g) = g.
Proof.
  intro g.  exact (refl g).
Defined.

(* Fails (even though the definiens is exactly the output of [Print flip_P_is_retr1.]): *)
Definition flip_P_is_retr3 : forall g, 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).

(* If we avoid using [flip P] (i.e. using flip at a higher universe level), then things work fine: *) 
Let flip_P_inv' := @flip _ _ (fun b a => P a b).

Definition flip_P_is_retr4 : forall g, flip_P_inv' (flip_P g) = g.
Proof.
  intro g.  exact (refl g).
Defined.