search

mikeshulman / Coq-HoTT

Homotopy type theory
http://homotopytypetheory.org/
Other
12 stars 4 forks source link

Universe bug when making IsGraph a parameter #41

Closed Alizter closed 4 years ago

Alizter commented 4 years ago

Have a look in this branch:

https://github.com/Alizter/HoTT/blob/graph_wildcat/theories/WildCat/Core.v

There is a really weird universe error in the definition of Is1Cat now. I can't work out why this is.

Alizter commented 4 years ago

@mikeshulman Are you able to take a look at this?

mikeshulman commented 4 years ago

Just give the type of all the elements of A.

  cat_idr : forall (a b : A) (f : a $-> b), f $o Id a $== f;

rather than forall a b (f : a $-> b),. I actually don't know why the latter ever worked; how could Coq guess that a and b should belong to A rather than some other random category?

Alizter commented 4 years ago

@mikeshulman Thank you, that was way easier than I thought it would be.