Daniel R. Grayson
Daniel R. Grayson
Marc Levine suggests formalizing this paper: Spivakovsky, Mark "A solution to Hironaka's polyhedra game". Arithmetic and geometry, Vol. II, 419–432, Progr. Math., 36, Birkhäuser Boston, Boston, MA, 1983. The whole...
My definition of well ordered set is this: ``` Definition hasSmallest {X : UU} (R : hrel X) : hProp := ∀ S : hsubtype X, (∃ x, S x)...
... as in the discussion at #861
Someone should port omega (see http://coq.inria.fr/refman/Reference-Manual023.html) to unimath. It would clean up hnat.v and my code considerably.
setquot3
Here is another elegant way to construct set quotients: http://www.cs.bham.ac.uk/~mhe/agda-new/UF-Quotient.html , devised by Martin Escardo. We should implement it, perhaps after waiting for us to stop using type-in-type, so we...
Do we want to encourage or discourage the use of auto and autorewrite with or without hint databases (in the style guide at https://github.com/UniMath/UniMath/blob/master/UniMath/README.md )? On the one hand, it...
VV: " Basics do not require type-in-type and maybe we can make it clear even with the existing Coq." I'll see if I can set this up in the Makefile.
A comment from Thorsten Altenkirch: In Moerdijk and Gambino’s “Wellfounded trees in categories” it is shown that very topos has W-types. I think that UniMath gives you a topos (on...
Vladimir thought it was important for those not acquainted with UniMath to be able to learn it well by stepping through the proofs (in ProofGeneral or Coqide), working their way...
\equiv
Let's do for \equiv what we did for = --- use \equivto for the type of equivalences and \equiv for its propositional truncation.