Generalised J rules and simultaneous pattern matching of equalities

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

• Thibaut Benjamin (University of Cambridge)
• Monday 10 February 2025, 13:00-14:00
• FS07, Computer Laboratory.

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:

• FS07, Computer Laboratory
• tcw57’s list

Note that ex-directory lists are not shown.