-include "types.ma".
+include "hott/types.ma".
(* * * Basic definitions of homotopy type theory, particularly the groupoid structure of identity types. *)
| forall _, _ => fail 1 x "is not atomic"
| _ => idtac
end.
-*)
\ No newline at end of file
+*)