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 answers
Related Questions in COQ
- Coq : mutually recursive definitions with [mrec] in InteractionTrees Library
- Is there a function that returns a list of values with specific type in OCaml?
- How to prove (X !-> 3) =[ <{ X := X + 2 }> ]=> (X !-> 5)?
- Showing polynomial equality in coq/ssreflect
- Syntax of the case tactic in coq
- Why assuming singleton elimination and definitional proof irrelevance leads to UIP, in Coq?
- Understanding nat_ind2 in Logical Foundations
- What `dependent induction` tactic does in Coq and how to use it
- Split multiple conjuncts in the goal
- Coq can't define an inductive proposition
- Coq Decreasing Argument mapping
- The `specialize` tatic in Coq does not work well with typeclasses?
- Multiple Assignements in a Coq Map to the same value
- Decider for lists In Fixpoint
- VSCoq Error: Connection to server got closed. Server will not be restarted
Related Questions in HOMOTOPY-TYPE-THEORY
- Why assuming singleton elimination and definitional proof irrelevance leads to UIP, in Coq?
- In cubical type theory, why are there function types that accept intervals as arguments when there are already a path type?
- Why does cubical agda choose the particular two component homogeneous path composition operator it does?
- Agda: Failed to solve the following constraints: P x <= _X_53 (blocked on _X_53)
- Unfolding terms created with `assert` in Coq
- Importing HoTT library in Coq
- How do you use the Ring solver in Cubical Agda?
- In scala, what can be done to prevent compiler from cyclic summoning of implicit premises? And how to avoid them
- Why does universe level restriction behave differently between inductive family and parameterized inductive type without axiom K in agda
- Coq for HoTT: proving || P-> X || -> (P-> ||X||)
- How does one write (and debug) a two arguement dependent application, apd2, and use this to prove functoriality of such ap in agda?
- How to prove element addition is injective for a cubical finite multi set?
- How does one use identity elimination (in agda) to prove Eckmann Hilton for higher dimensional paths in HoTT?
- How to explicitly use an induction principle in coq?
- Is this formulation of Modulo a Set?
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?
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)
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.