2,190 reputation
317
bio website homotopytypetheory.org
location
age 28
visits member for 2 years, 7 months
seen Nov 4 at 20:06

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.
Oct
29
awarded  Nice Answer
May
17
awarded  Yearling
May
15
awarded  Caucus
Aug
6
awarded  Nice Question
Jun
15
awarded  Enthusiast