> hello. is it required to be familiar with topology in order to read/understand hott?
> the hott book*
<ziman> it probably helps
<ziman> but I know only the basic basics and I could get through it
> could you recommend any introductory book to topology then?
<ziman> I learned it from my prof's course notes, which are in Czech, unfortunately.
> thanks anyway, will try to google something
<jgross_> Topology, by Munkres, is the intro topology text book I learned from. Algebraic Topology, by Hatcher, is the intro homotopy theory book I learned from.  (Munkres assumes some knowledge or comfort with set theory and proofs; Hatcher assumes some intro point-set topology, if I recall correctly.) 
> thanks
<mr-> defanor: I would ignore most of Munkres, except the definitions of a topological space, and continuous maps. From Hatcher, it may be important to understand CW-complexes, because that's how you build HITs. 
<mr-> Also, Homotopy is important. So make sure you understand homotopy groups and how they are functorial.
> mr-: idk what are HITs, but will find out, hopefully. thanks
<mr-> defanor: Higher inductive types. The first example in The Book is the circle, I think. It is constructed as a CW-complex
<mr-> I am not that far into HoTT myself, but most of the "homotopy" in there seems to be the fact that spaces are (infinty) groupoids and continuous maps are functors
<byorgey> as a counterpoint, I know approximately zero topology and made it quite far in the HoTT book with just a good understanding of dependent type theory
<byorgey> there are nice examples of HITs that don't involve topology.  e.g. see Dan Licata's talk on modeling darcs as a HIT.
<mr-> I guess if HoTT is the first time you encounter "transport", that's fine too
<byorgey> yep, it was for me
<mr-> But if you want to see why it is called _Homotopy_ Type Theory, some knowledge in topology might be good :-)
<byorgey> but that's just an issue of history.  One could imagine an alternate universe where HoTT was discovered first and later people came up with tolopogy and named it after the type theory =)
<mr-> Yes, because then there would be a huge pile of previous work on that part of type theory, which could help you figure out homotopy theory.
<sclv> as a counter counter point i’ve learned some elements of topology via the book in conjunction with having some algebraic topologists in our reading group
<sclv> and focusing on the geometric intuition for types is great for someone without that background
<sclv> because it opens up a whole new world of mathematical tools
<sclv> mr- it isn’t spaces that are infiniy groupoids, it is equality that is
<sclv> spaces can have “any old” homotopic structure you want
<sclv> also of course dependent functions are fibrations, which is neat
<Saizan> iiuc, dependent types are fibrations and dependent functions are sections for those
* defanor writes everything down and slowly reads Munkres' "Topology"
<mr-> sclv: I am not sure what you are saying. Spaces are infinity groupoids via the (infinite) fundamental groupoid functor. That functor, together with geometric realization (of simplicial sets) are a Quillan equivalence. In that sense: Spaces are infinity groupoids.
<sclv> Saizan: yeah, that’s probably more accurate
<sclv> ditto mr-
<mr-> Maybe I was missing your point. When talking about spaces, the term "homotopy" has a rather fixed meaning. At least for me ;-)
<sclv> looking in the book the actual slogans are “types are higher groupoids” (resp spaces) and “type families are fibrations”
<sclv> its probably more correct on my part to say “the equality relation provides types with a higher groupoid structure”?