I was reading the article Homotopy type theory and Voevodsky's univalent foundations by Álvaro Pelayo, Michael A. Warren recently. There is a companion file http://mawarren.net/papers/tutorial.v. I compiled it with the latest coq verion 8.8.0 but encountered an error. Can anyone help me? Thanks in advance.
This code was meant to build with a custom-patched version of Coq 8.4 or Coq 8.3 which disabled universe checking; I recall talking with Dan Grayson or Vladimir at some point around then and them mentioning using such a patched version of Coq. (Note also that the file is from Aug 2012, and https://coq.inria.fr/news/ says that Coq 8.4 was released that month.) It's quite unfortunate that the article you cite doesn't seem to mention the version of Coq anywhere.
In any case, you can build this file in Coq versions 8.5 and newer by passing the argument -type-in-type to coqc or coqtop and also adding
Set Asymmetric Patterns.
at the top of the file. If you are using ProofGeneral, you can add
(* -*- coq-prog-args: ("-type-in-type") -*- *)
to the top of the file as well so that you don't have to manually pass -type-in-type to coqtop.