BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//wp-events-plugin.com//7.2.3.1//EN
TZID:Europe/Paris
X-WR-TIMEZONE:Europe/Paris
BEGIN:VEVENT
UID:8391@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20140418T110000
DTEND;TZID=Europe/Paris:20140418T120000
DTSTAMP:20241120T210358Z
URL:https://www.i2m.univ-amu.fr/evenements/canonicity-of-groupoids-laws-us
 ing-parametricity-theory/
SUMMARY:Marc Lasson (University of Cambridge): Canonicity of groupoids laws
  using parametricity theory
DESCRIPTION:Marc Lasson: The synthetic approach to weak ω-groupoids promot
 ed by the univalent foundation program is the idea that (homotopy) type th
 eory should be the primitive language in which spaces\, points\, paths\, h
 omotopies are derived. Following this approach\, spaces are represented by
  types\, points by inhabitants and paths by equalities between points (als
 o known as identity types) and algebraic properties of these objects shoul
 d not be unforced a priori (for instance by axioms) but should be derived 
 directly from the language. Following this approach requires to be convinc
 ed that definitions of new operations should be canonical\, in the sense t
 hat no important choice should be made by picking an implementation of the
 se operations instead of an other. Identities\, inversion and concatenatio
 n of path\, associativities\, idempotency of inversion\, horizontal and ve
 rtical compositions of 2-paths\, are all examples of groupoid laws.\nParam
 etricity has been introduced by Reynolds to study the polymorphic abstract
 ion of system F. It refers to the concept that well-typed programs cannot 
 inspect the type their arguments\; they must behave uniformly with respect
  to abstract types. Reynolds formalizes this notion by showing that polymo
 rphic programs satisfy the so-called logical relations defined by inductio
 n on the structure of types. Dependent type systems are expressive enough 
 to state their own parametricity theory.\nIn this talk\, we will focus on 
 the consequences of this remark when applied to identity types and we will
  use it to prove that all implementations of a given groupoid law are prov
 ably equal to each other.\n\nhttp://www.cl.cam.ac.uk/~mrl42/
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 020/01/Marc_Lasson.jpg
CATEGORIES:Séminaire,Logique et Interactions
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
DTSTART:20140330T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
END:DAYLIGHT
END:VTIMEZONE
END:VCALENDAR