University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > A computational method for left adjointness

A computational method for left adjointness

Add to your list(s) Download to your calendar using vCal

  • UserSimon Forest, University of Aix-Marseille
  • ClockFriday 26 November 2021, 14:00-15:00
  • HouseFW26.

If you have a question about this talk, please contact Jamie Vicary.

Recently, several computational tools have been proposed for higher categories, like CaTT, Globular, cateq, etc. Paradoxically, fewer tools exist for more common 1-categories. A reason for this might be that the computational problems on 1-categories, expressed using generators and relations, do not appear as interesting as the ones on higher dimensional categories. In this talk, an alternative computational framework for 1-categories is proposed, which enables working with large categories like the categories of sets, groups, etc. As an application, a computational method for proving that (some) functors between such categories are left adjoint is introduced. In good cases, this method is fully automated as will be shown on several examples.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2021 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity