Reflexive graph quotients are pushouts

I'd like to tell about a theorem that has been useful for me on several occasions, that was also the first topicĀ in a series of presentations I'm currently giving at the CMU HoTT seminar. It characterizes the reflexive graph quotients as a certain pushout, so it allows us to find new, possibly more intuitive descriptions … Continue reading Reflexive graph quotients are pushouts


The loop space of the 2-sphere

Back in January 2016 I gave an introductory talk at the University of Ljubljana about Homotopy Type Theory. The goal of this talk was to display some basic techniques in the field, such as constructing higher inductive types, and using the encode-decode method to figure out what its identity type is. Recall that the topological … Continue reading The loop space of the 2-sphere