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.
coq code of the article Homotopy type theory and Voevodsky's univalent foundations
123 Views Asked by ShanNing At
1
There are 1 best solutions below
Related Questions in COQ
- CoqIDE loadpath error for ssreflect
- How to assign a natural number to variable in Coq?
- Handling let in hypothesis
- Sum of exponents with same base
- How to run Athena | Coq | Isabelle codes remotely?
- Is equality decidable on any coinductive type?
- Coq "convoy pattern"
- In coq, how to do "induction n eqn: Hn" in a way that doesn't mess up the inductive hypothesis?
- Pattern matching multiple constructors in a single clause in Coq
- How to use Coq GenericMinMax to prove facts about the reals
- what does the colon greater than sign mean in coq
- Subtyping in Coq
- How to write coq definitions with "subtypes"
- Stronger completeness axiom for real numbers in Coq
- When is the first input to `list_rec` not a constant function?
Related Questions in HOMOTOPY-TYPE-THEORY
- How to define higher inductive types in Z3
- Importing HoTT library in Coq
- Equality between paths
- Is the univalence axiom injective?
- Interval extensionality?
- How to prove that the defining equations of the recursor for N hold propositionally using the induction principle for N in Agda?
- Unfolding terms created with `assert` in Coq
- Is this formulation of Modulo a Set?
- Why does universe level restriction behave differently between inductive family and parameterized inductive type without axiom K in agda
- In scala, what can be done to prevent compiler from cyclic summoning of implicit premises? And how to avoid them
- In cubical type theory, why are there function types that accept intervals as arguments when there are already a path type?
- Constructing a path with constraints in an isSet type
- Constructing squares with constraints in an isSet type
- How do I handle the higher inductive cases when defining functions on HITs?
- coq code of the article Homotopy type theory and Voevodsky's univalent foundations
Trending Questions
- UIImageView Frame Doesn't Reflect Constraints
- Is it possible to use adb commands to click on a view by finding its ID?
- How to create a new web character symbol recognizable by html/javascript?
- Why isn't my CSS3 animation smooth in Google Chrome (but very smooth on other browsers)?
- Heap Gives Page Fault
- Connect ffmpeg to Visual Studio 2008
- Both Object- and ValueAnimator jumps when Duration is set above API LvL 24
- How to avoid default initialization of objects in std::vector?
- second argument of the command line arguments in a format other than char** argv or char* argv[]
- How to improve efficiency of algorithm which generates next lexicographic permutation?
- Navigating to the another actvity app getting crash in android
- How to read the particular message format in android and store in sqlite database?
- Resetting inventory status after order is cancelled
- Efficiently compute powers of X in SSE/AVX
- Insert into an external database using ajax and php : POST 500 (Internal Server Error)
Popular Questions
- How do I undo the most recent local commits in Git?
- How can I remove a specific item from an array in JavaScript?
- How do I delete a Git branch locally and remotely?
- Find all files containing a specific text (string) on Linux?
- How do I revert a Git repository to a previous commit?
- How do I create an HTML button that acts like a link?
- How do I check out a remote Git branch?
- How do I force "git pull" to overwrite local files?
- How do I list all files of a directory?
- How to check whether a string contains a substring in JavaScript?
- How do I redirect to another webpage?
- How can I iterate over rows in a Pandas DataFrame?
- How do I convert a String to an int in Java?
- Does Python have a string 'contains' substring method?
- How do I check if a string contains a specific word?
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-typetocoqcorcoqtopand also addingat the top of the file. If you are using ProofGeneral, you can add
to the top of the file as well so that you don't have to manually pass
-type-in-typetocoqtop.