not all equality was proven using reflexivity. My understanding of the matter is that is has to do with the placement of the forall (x : A) quantifier. It is permissible to move one of the x's to the top level (based path induction), but not both. (This is somewhat obscured by the reuse of variable names.) There is also a geometric intuition, which is that when both or one endpoints of the path are free (inner-quantification), then I can contract the path into nothingness. But I have a difficult time mapping this onto any sort of rigorous argument.
http://blog.ezyang.com/2013/06/homotopy-type-theory-chapter-one/
#homotopy folks any clue on it?