Fix broken equality; add equality for sigma; simply Q

Equality for functions should be

    (x y : A) (p : x=y) f x = g y

and not

    (x : A) f x = g x

Simplified the Rational representation by making the denominator a
non-zero natural; thus the sign is entirely kept inside the numerator.
Added a trivial tactic

This recursively instantiates refl and tt as necessary.
Add sigma equality for trivial tactic
Require refl to convert homotopy into identity proof