3
Using Agda to Explore PathOriented Models of Type Theory
http://sms.cam.ac.uk/media/2520888
Pitts, A
Tuesday 27th June 2017  13:30 to 14:30
40
Using Agda to Explore PathOriented Models of Type Theory
http://sms.cam.ac.uk/media/2520888
http://rss.sms.cam.ac.uk/itunesimage/2526702.jpg
no

Using Agda to Explore PathOriented Models of Type Theory
ucs_sms_2520307_2520888
http://sms.cam.ac.uk/media/2520888
Using Agda to Explore PathOriented Models of Type Theory
Pitts, A
Tuesday 27th June 2017  13:30 to 14:30
Thu, 20 Jul 2017 09:47:14 +0100
Isaac Newton Institute
Pitts, A
258e6cdcc9bad4d115c96747884a541b
3a5b2d6314261358f739a7d7a24aa389
9c5c08c409e2e4696e8fda8c1b972d69
ed90c9f8f8c4402f49ec716beb0d47b5
Pitts, A
Tuesday 27th June 2017  13:30 to 14:30
Pitts, A
Tuesday 27th June 2017  13:30 to 14:30
Cambridge University
3389
http://sms.cam.ac.uk/media/2520888
Using Agda to Explore PathOriented Models of Type Theory
Pitts, A
Tuesday 27th June 2017  13:30 to 14:30
Homotopy Type Theory (HoTT) has reinvigorated research into the theory and applications of the intensional version of MartinLöf typetheory. On the one hand, the language of type theory helps to express synthetic constructions and arguments in homotopy theory and higherdimensional category theory. On the other hand, the geometric and algebraic insights of those highly developed branches of mathematics shed new light on logical and typetheoretic notions. In particular, HoTT takes a pathoriented view of intensional (i.e.proofrelevant) equality: proofs of equality of two elements of a type x,y : A, i.e. elements of a MartinLöf identity type Id_A x y, behave analogously to paths between two points x, y in a space A. The complicated internal structure of intensional identity types relatesto the homotopy classes of path spaces. To make this analogy preciseand to exploit it, it helps to have a wide range of models ofintensional type theory that embody this pathoriented view ofequality in some way.
In this talk I will describe some recent work on pathoriented modelsof type theory carried out with my student Ian Orton and making use of the Agda theoremprover. I will try to avoid technicalities in favourof describing why Agda in "unsafe" mode is so useful to us while wecreate new mathematics, rather than verifying existing mathematical theorems; and also describe some limitations of Agda (to do with quotient types) in the hope that the audience will tell me about a prover without those limitations. I also want to make some comments about mathematical knowledge representation as it relates to my search, as a homotopical ignoramus, for knowledge that will help in the construction of models of HoTT.
20170720T09:47:15+01:00
3389
2520888
true
16x9
false
no