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:8432@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20140318T110000
DTEND;TZID=Europe/Paris:20140318T120000
DTSTAMP:20241120T210412Z
URL:https://www.i2m.univ-amu.fr/evenements/category-theory-in-the-univalen
 t-foundations/
SUMMARY:Benedikt Ahrens (CIMI\, University Paul Sabatier\, Toulouse): Categ
 ory theory in the Univalent Foundations
DESCRIPTION:Benedikt Ahrens: The Univalent Foundations is an extension of I
 ntensional Martin-Löf Type Theory (MLTT) recently proposed by V. Voevodsk
 y. Its novelty is the Univalence Axiom which implements the idea that indi
 stinguishable types should be equal by identifying equality of types with 
 isomorphism of types. When formalizing category theory in traditional\, se
 t-theoretic foundations\, a significant discrepancy between the foundation
 al notion of "sameness" - equality - and its categorical notion arises: mo
 st category-theoretic concepts are invariant under weaker notions of samen
 ess than equality\, namely isomorphism in a category or equivalence of cat
 egories. We show that this discrepancy can be avoided when formalizing cat
 egory theory in Univalent Foundations. In this talk I first give an introd
 uction to Voevodsky's Univalent Foundations. Afterwards I define categorie
 s and univalent categories within Univalent Foundations\, and develop basi
 c category theory. The two main results of our work are the following:\n-#
  Two univalent categories are equivalent (in the category-theoretic sense)
  if and only if they are equal (in the type-theoretic sense).\n-# Any cate
 gory can be turned into a univalent category via a universal construction\
 , which we call the Rezk completion.\n\n
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 020/01/Benedikt_Ahrens.jpg
CATEGORIES:Séminaire,Logique et Interactions
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:STANDARD
DTSTART:20131027T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
END:VTIMEZONE
END:VCALENDAR