Jason Gross

I have an example at https://gist.github.com/JasonGross/8852236 (very bottom) where the unification engine churns for 3-4 seconds before deciding that terms are unifiable. I'm not sure if anything can be done...

coqc loops(?) when coqtop doesn't

6

At https://github.com/JasonGross/HoTT/tree/be130e7b72e8b5bf804e3612b095de0ba01d864c, `time ./hoqtop < theories/categories/Limits/Functors.v` finishes in under 1 second, while `hoqc theories/categories/Limits/Functors.v` spins for a quite a while.

Syntax for explicit universe levels

2

If we provide a syntax for explicit universe levels, @mattam82 has said that he will provide it. I propose something like the following: ``` coq Definition foo {universes i

Universe inconsistencies depend oddly on the stdlib (polyproj)

6

Here is some code that works on HoTT/coq trunk, fails on `pose (@isequiv_apD10 H (Lift A)).` with polyproj, and fails on `exact t'` with polyproj when we replace the standard...

``` coq (* File reduced by coq-bug-finder from original input, then from 669 lines to 79 lines, then from 89 lines to 44 lines *) Set Primitive Projections. Reserved Notation...

``` coq Set Primitive Projections. Set Implicit Arguments. Set Universe Polymorphism. Set Asymmetric Patterns. Inductive sum A B := inl : A -> sum A B | inr : B...

``` coq Set Implicit Arguments. Set Primitive Projections. Polymorphic Inductive eqp A (x : A) : A -> Type := eqp_refl : eqp x x. Monomorphic Inductive eqm A (x...

Error: Conversion test raised an anomaly (polyproj)

1

``` coq Set Implicit Arguments. Require Import Logic. Global Set Universe Polymorphism. Global Set Asymmetric Patterns. Local Set Primitive Projections. Local Open Scope type_scope. Record prod (A B : Type)...

``` coq (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") *) (* File reduced by coq-bug-finder from original input, then from 4988 lines to 856 lines, then from 648 lines to...

Behold another issue with `Set`. In this case, the problem is that the theorem that `Contr (Unit : Set)` doesn't also prove `Contr (Unit : Type)` for other universes, even...