Monthly Archives: June 2015
Not every weakly constant function is conditionally constant
As discussed at length on the mailing list some time ago, there are several different things that one might mean by saying that a function is “constant”. Here is my preferred terminology: is constant if we have such that for … Continue reading
Posted in Univalence
13 Comments
Double Groupoids and Crossed Modules in HoTT
The past eight months I spent at CMU for my master thesis project. I ended up formalizing some algebraic structures used in Ronald Brown’s book “Non-Abelian Algebraic Topology”: Double groupoids with thin structure and crossed modules over groupoids. As the … Continue reading
Posted in Code, Homotopy Theory
31 Comments
Homotopy Type Theory 