A computational method for left adjointness

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

• Simon Forest, University of Aix-Marseille
• Friday 26 November 2021, 14:00-15:00
• FW26.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.