Timeline for Analysis of proof that for a category which is also a poset, every diagram commutes
Current License: CC BY-SA 4.0
2 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 29 at 23:17 | comment | added | Andrej Bauer |
Did you try to run the code in Coq to determine whether Coq accepts it? To answer some of the questions: the type of le_refl mentions le, so Coq can tell it is a constraint on le. The forall quantifier declares a bound variable, so there are no undeclared variables here.
|
|
| Mar 29 at 19:36 | history | asked | Julius Hamilton | CC BY-SA 4.0 |