BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:One-Dimensional Higher Inductive Types - Peter Dybjer\, Chalmers U
 niversity of Technology
DTSTART:20170120T140000Z
DTEND:20170120T150000Z
UID:TALK69708@talks.cam.ac.uk
CONTACT:Dominic Mulligan
DESCRIPTION:Higher inductive types are a key feature of Homotopy Type Theo
 ry. Higher inductive types generalise ordinary inductive types\, by not on
 ly having constructors for elements (points)\, but also constructors for e
 qualities between elements (paths)\, constructors for equalities between e
 qualities\, etc. In spite of their importance for the theory\, the syntax 
 and semantics of higher inductive types are not yet fully understood. To t
 his end we look at the special case of "one-dimensional" higher inductive 
 types (1-hits)\, that is\, higher inductive types with only point and path
  constructors. A general form for an introduction rule for a 1-hit is prop
 osed\, as well as an inversion principle for deriving the elimination and 
 equality rules from the introduction rules. We also show that the setoid m
 odel supports this schema. Finally\, we outline the extension of this sche
 ma to 2-hits and their interpretation as groupoids.
LOCATION:FW26
END:VEVENT
END:VCALENDAR