Q:

Proof in Coq that equality is reflexivity

The HOTT book writes on page 51:
... we can prove by path induction on p: x = y  that  
 $(x, y, p) =_{ \sum_{(x,y:A)} (x=y)} (x, x, refl x)$ .

Can someone show me how to prove this in Coq?

A:

Actually, it is possible to prove this result in Coq:
Notation "y ; z" := (existT _ y z) (at level 80, right associativity).

Definition hott51 T x y e :
  (x; y; e) = (x; x; eq_refl) :> {x : T & {y : T & x = y} } :=
  match e with
  | eq_refl => eq_refl
  end.

Here, I've used a semicolon tuple notation to express dependent pairs; in Coq, {x : T & T x} is the sigma type \sum_{x : T} T x. There is also a slightly easier-to-read variant, where we do not mention y:
Definition hott51' T x e : (x; e) = (x; eq_refl) :> {y : T & x = y} :=
  match e with
  | eq_refl => eq_refl
  end.

If you're not used to writing proof terms by hand, this code might look a bit mysterious, but it is doing exactly what the HoTT book says: proceeding by path induction. There's one crucial bit of information that is missing here, which are the type annotations needed to do path induction. Coq is able to infer those, but we can ask it to tell us what they are explicitly by printing the term. For hott51', we get the following (after some rewriting):
hott51' = 
fun (T : Type) (x : T) (e : x = x) =>
match e as e' in _ = y' return (y'; e') = (x; eq_refl) with
| eq_refl => eq_refl
end
     : forall (T : Type) (x : T) (e : x = x),
       (x; e) = (x; eq_refl)

The important detail there is that in the return type of the match, both x and e are generalized to y' and e'. The only reason this is possible is because we wrapped x in a pair. Consider what would happen if we tried proving UIP:
Fail Definition uip T (x : T) (e : x = x) : e = eq_refl :=
  match e as e' in _ = y' return e' = eq_refl with
  | eq_refl => eq_refl
  end.

Here, Coq complains, saying:
The command has indeed failed with message:
In environment
T : Type
x : T
e : x = x
y' : T
e' : x = y'
The term "eq_refl" has type "x = x" while it is expected to have type
 "x = y'" (cannot unify "x" and "y'").

What this error message is saying is that, in the return type of the  match, the e' has type x = y', where y' is generalized. This means that the equality e' = eq_refl is ill-typed, because the right-hand side must have type x = x or y' = y'.

