Department of

October 2017 November 2017 December 2017 Su Mo Tu We Th Fr Sa Su Mo Tu We Th Fr Sa Su Mo Tu We Th Fr Sa 1 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 15 16 22 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.