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:5710@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20230309T110000
DTEND;TZID=Europe/Paris:20230309T123000
DTSTAMP:20241124T134246Z
URL:https://www.i2m.univ-amu.fr/evenements/generalized-algebraic-theories-
 and-categories-with-families/
SUMMARY:Peter Dybjer (Chalmers University of Technology\, Göteborg): Gener
 alized algebraic theories and categories with families
DESCRIPTION:Peter Dybjer: We give a new syntax independent definition of th
 e notion of a generalized algebraic theory as an initial object in a categ
 ory of categories with families (cwfs) with extra structure. To this end w
 e define inductively how to build a valid signature $\\Sigma$ for a genera
 lized algebraic theory and the associated category $\\Cwf_\\Sigma$ of cwfs
  with a $\\Sigma$-structure and cwf-morphisms that preserve this structure
  on the nose. Our definition refers to {\\em uniform families} of contexts
 \, types\, and terms\, a purely semantic notion. Furthermore\, we show how
  to syntactically construct initial cwfs with $\\Sigma$-structures. This r
 esult can be viewed as a generalization of Birkhoff's completeness theorem
  for equational logic. It is obtained by extending Castellan\, Clairambaul
 t\, and Dybjer's construction of an initial cwf. We provide examples of ge
 neralized algebraic theories for monoids\, categories\, categories with fa
 milies\, and categories with families with extra structure for some type f
 ormers of dependent type theory. The models of these are internal monoids\
 , internal categories\, and internal categories with families (with extra 
 structure) in a category with families.\n\n&nbsp\;
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 023/03/Peter_Dybjer.png
CATEGORIES:Séminaire,Logique et Interactions
LOCATION:I2M Luminy - Ancienne BU\, Salle Séminaire2 (RdC)\, 163 Avenue de
  Luminy\, 13009 Marseille\, France\, 
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-ADDRESS=163 Avenue de Luminy\, 1300
 9 Marseille\, France\, ;X-APPLE-RADIUS=100;X-TITLE=I2M Luminy - Ancienne B
 U\, Salle Séminaire2 (RdC):geo:0,0
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:STANDARD
DTSTART:20221030T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
END:VTIMEZONE
END:VCALENDAR