University of Cambridge > Talks.cam > SANDWICH Seminar (Computer Laboratory) > Generalised J rules and simultaneous pattern matching of equalities

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Generalised J rules and simultaneous pattern matching of equalities

Download to your calendar using vCal

If you have a question about this talk, please contact Dr Meven Lennon-Bertrand .

I will present some ongoing work with Jon Sterling, where we are thinking of generalising the J rule to eliminate several equalities at once. These generalised J rules are parametrised by a choice of a shape, that must be picked out from a class of predefined allowed shapes, meant to be contractible. We have a few examples of such classes of shapes, each of them giving rise to a theory. We believe that these theories provide very generic pattern-matching procedures for identity types, allowing to eliminate several identities at the same time, without accidentally proving axiom K or UIP .

This talk is part of the SANDWICH Seminar (Computer Laboratory) series.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

SS03, William Gates Building. Zoom link: https://cl-cam-ac-uk.zoom.us/j/4361570789?pwd=Nkl2T3ZLaTZwRm05bzRTOUUxY3Q4QT09&from=addon Part II Lecture Theatre, First Floor Zoology Hybrid - Maxwell Centre & on Zoom

Other talks

Talk TBC Machine Learning for Spectral Geometry and Vice Versa Quantifying the unquantifiable? Assessing the importance of almsgiving in early modern France and Spain Genomic Medicine CPC CSaP Annual Cleevely Lecture 2026 Title to be confirmed
 

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