Department of

October 2017 November 2017December 2017Su Mo Tu We Th Fr Sa Su Mo Tu We Th Fr Sa Su Mo Tu We Th FrSa1 2 3 4 5 6 7 1 2 3 4 1 2 8 9 10 11 12 13 14 5 6 7 8 9 10 11 3 4 5 6 7 8 9 15 16 17 18 19 20 21 12 13 14 15 16 17 18 10 11 12 13 14 151622 23 24 25 26 27 28 19 20 21 22 23 24 25 17 18 19 20 21 22 23 29 30 31 26 27 28 29 30 24 25 26 27 28 29 30 31

Tuesday, November 28, 2017

**Abstract:** Homotopy type theory is an emerging field of mathematics, based on Martin-Löf's constructive theory of types. We think of types as spaces, and type families as fibrations. With the addition of the univalence axiom and higher inductive types doing homotopy theory in type theory (and in a proof assistant!) then becomes feasible. (Reflexive) coequalizers can be used to define a many homotopy colimits in type theory. The case of reflexive coequalizers is interesting because classically the topos of reflexive graphs is cohesive over the topos of sets. I will present analogous results in homotopy type theory.