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:4947@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20231109T110000
DTEND;TZID=Europe/Paris:20231109T123000
DTSTAMP:20260107T154213Z
URL:https://www.i2m.univ-amu.fr/evenements/higher-structures-in-homotopy-t
 ype-theory/
SUMMARY:Antoine Allioux (IRIF): Higher Structures in Homotopy Type Theory
DESCRIPTION:Antoine Allioux: \n\nThe definition of algebraic structures on 
 arbitrary types in homotopy type theory (HoTT) has proven elusive so far. 
 This is due to types behaving like spaces instead of plain sets in general
  with equalities between elements of a type behaving like homotopies. Equa
 tional laws of algebraic structures must therefore be stated coherently. H
 owever\, in set-based mathematics\, the presentation of this coherence dat
 a relies on set-level algebraic structures such as operads or presheaves w
 hich are thus not subject to additional coherence conditions. Replicating 
 this approach in HoTT leads to a situation of circular dependency as these
  structures must be defined coherently from the beginning.\n\nWe break thi
 s situation of circular dependency by extending type theory with a univers
 e of cartesian polynomial monads which\, crucially\, satisfy their laws de
 finitionally. This extension permits the presentation of types and their h
 igher structures as opetopic types which are infinite collections of cells
  whose geometry is described by opetopes. Opetopes are geometric shapes or
 iginally introduced by Baez and Dolan in order to give a definition of n-c
 ategories. The constructors under which our universe of cartesian polynomi
 al monads is closed allow us to define\, in particular\, the Baez-Dolan sl
 ice construction on which is based our definition of opetopic type.\n\nOpe
 topic types then enable us to define coherent higher algebraic structures\
 , among which infinity-groupoids and (infinity\, 1)-categories. Crucially\
 , their higher structure coincides with the one induced by their identity 
 types. We then establish some expected results in order to motivate our de
 finitions.\n\n\nDiaporama de l’exposé (PDF)
CATEGORIES:Séminaire,Logique et Interactions
LOCATION:Site Sud\, Luminy\, Ancienne BU\, Salle Séminaire2 (RdC)\, \, 
GEO:0.000000;0.000000
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-ADDRESS=\, ;X-APPLE-RADIUS=100;X-TI
 TLE=Site Sud\, Luminy\, Ancienne BU\, Salle Séminaire2 (RdC):geo:0.000000
 ,0.000000
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:STANDARD
DTSTART:20231029T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
END:VTIMEZONE
END:VCALENDAR