BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Using Agda to Explore Path-Oriented Models of Type Theory - Andrew
  Pitts (University of Cambridge)
DTSTART:20170627T123000Z
DTEND:20170627T133000Z
UID:TALK73083@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION:Homotopy Type Theory (HoTT) has re-invigorated research into t
 he&nbsp\;theory and applications of the intensional version of Martin-L&ou
 ml\;f typetheory. On the one hand\, the language of type theory helps to e
 xpress&nbsp\;synthetic constructions and arguments in homotopy theory and&
 nbsp\;higher-dimensional category theory. On the other hand\, the geometri
 c&nbsp\;and algebraic insights of those highly developed branches of&nbsp\
 ;mathematics shed new light on logical and type-theoretic notions. In&nbsp
 \;particular\, HoTT takes a path-oriented view of intensional (i.e.proof-r
 elevant) equality: proofs of equality of two elements of a&nbsp\;type x\,y
  : A\, i.e. elements of a Martin-L&ouml\;f identity type Id_A x y\,&nbsp\;
 behave analogously to paths between two points x\, y in a space A. The&nbs
 p\;complicated internal structure of intensional identity types relatesto 
 the homotopy classes of path spaces. To make this analogy preciseand to ex
 ploit it\, it helps to have a wide range of models ofintensional type theo
 ry that embody this path-oriented view ofequality in some way.In this talk
  I will describe some recent work on path-oriented modelsof type theory ca
 rried out with my student Ian Orton and making use of&nbsp\;the Agda theor
 em-prover. I will try to avoid technicalities in favourof describing why A
 gda in "unsafe" mode is so useful to us while wecreate new mathematics\, r
 ather than verifying existing mathematical&nbsp\;theorems\; and also descr
 ibe some limitations of Agda (to do with&nbsp\;quotient types) in the hope
  that the audience will tell me about a&nbsp\;prover without those limitat
 ions. I also want to make some comments&nbsp\;about mathematical knowledge
  representation as it relates to my&nbsp\;search\, as a homotopical ignora
 mus\, for knowledge that will help in&nbsp\;the construction of models of 
 HoTT.
LOCATION:Seminar Room 2\, Newton Institute
END:VEVENT
END:VCALENDAR