Egbert
Reputation
2,425
Next privilege 2,500 Rep.
Create tag synonyms
 Nov 13 awarded Enlightened Nov 13 awarded Nice Answer Jul 28 awarded Custodian Jul 28 reviewed Reject find the Jordan form and $P$ such that $P^{-1}AP = J$. May 17 awarded Yearling Sep 30 awarded Explainer May 17 awarded Yearling Feb 4 comment Suggestions for a learning roadmap for universal algebra? I used Burris and Sankappanavar's "a course in universal algebra" to learn about this topic and I found very clear. Feb 4 answered Two questions on homotopy type theory Jan 21 comment How do I convince my students that the choice of variable of integration is irrelevant? This is a cute way, but don't you think it can be explained using logic rather than pictures? I have the feeling that when a teacher stands in front of the blackboard explaining things this way, he's relying on his authority as a teacher too much to convince his students. Jan 18 answered sSet is a model for Martin-lof type theory Jan 18 comment About constructive mathematics and Homotopy type theory Don't hesitate to ask more questions. That's what the site is for :) Jan 18 comment About constructive mathematics and Homotopy type theory There's a recent blog post by Andrej Bauer which addresses your issues too: math.andrej.com/2014/01/13/… Jan 17 answered Are there “essentially non-constructive” statements? Jan 17 comment About constructive mathematics and Homotopy type theory The cubical sets model, which addresses computational aspects of the univalence axiom, has recently been announced on the homotopytypetheory mailing list. Currently, Coq can't compute with univalence, but that might soon change :) How it is possible to do HoTT in Coq? The same way anything is done in Coq: see github.com/HoTT/HoTT Jan 17 comment How would you quantify the closeness between sets. You can't measure the distance between sets as if it were the distance between lists. Any reasonable notion of distance between sets should be isomorphism invariant -- in particular the distance from {2,8,5} to {9,8,2} should be the same as the distance from {8,5,2} to {9,8,2}. There are more useful metrics for sets involving suprema. Jan 17 answered Introductory books as preparation to read Voevodsky homotopy-theory (HoTT) book Jan 17 answered About constructive mathematics and Homotopy type theory Jan 14 comment Why are second-order 'things' studied so much in mathematics? May I add all of Set Theory to your list of "second order things"? :D First you have truth, then you have propositions and the next step up is sets. See ncatlab.org/nlab/show/homotopy+level. Jan 14 comment If one knows Homotopy Type Theory, what is the easiest way to learn Higher Topos Theory? I used three resources to learn higher topos theory: 1) Lurie's book, 2) Rezk's overview article at math.uiuc.edu/~rezk/homotopy-topos-sketch.pdf and 3) I spent lots of hours reading the nlab.