University of Birmingham > Talks@bham > Lab Lunch > Using Yoneda rather than J to present the identity type.

## Using Yoneda rather than J to present the identity type.Add to your list(s) Download to your calendar using vCal - Martin Escardo, CS Theory Group Birmingham
- Wednesday 22 November 2017, 01:00-02:00
- CS 217.
If you have a question about this talk, please contact Dr Steve Vickers. I will explain that the induction principle J for Martin-Lof’s identity types amounts to the Yoneda Lemma, when types are seen as infty-groupoids (and hence categories). This holds internally in MLTT : from J we derive the Yoneda Lemma, and conversely from the Yoneda Lemma we derive J. Moreover, the computation rule for Yoneda gives the computation rule for J, and vice versa. This talk is part of the Lab Lunch series. ## This talk is included in these lists:- CS 217
- Computer Science Departmental Series
- Computer Science Distinguished Seminars
- Lab Lunch
- Theoretical computer science seminar
- computer sience
Note that ex-directory lists are not shown. |
## Other listsPostgraduate Algebra Seminar Mathematics Colloquium Human Computer Interaction seminars## Other talksTBC |