From vaugely skimming through it, it looks like they define a more explicit version of judgmental equality, from which they found an extensional type theory, and proceed to calculate the fundamental group of different spaces in that theory. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.