BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Generalised J rules and simultaneous pattern matching of equalitie
 s - Thibaut Benjamin (University of Cambridge)
DTSTART:20250210T130000Z
DTEND:20250210T140000Z
UID:TALK228169@talks.cam.ac.uk
CONTACT:Dr Meven Lennon-Bertrand
DESCRIPTION: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\, ea
 ch 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 prov
 ing axiom K or UIP.
LOCATION:FS07\, Computer Laboratory
END:VEVENT
END:VCALENDAR