[Theory] Fwd: Talk of potential interest

[stuart]

Dear Colleagues,

FYI:

> Begin forwarded message:
> 
> From: Denis Hirschfeldt <drh at uchicago.edu>
> Subject: Talk of potential interest
> Date: April 24, 2023 at 10:12:43 AM CDT
> To: "Stuart A. Kurtz" <stuart at cs.uchicago.edu>
> Cc: Akhil Mathew <amathew3 at uchicago.edu>
> 
> Dear Stuart,
> 
> I'm forwarding below the announcement of a couple of talks by Emily Riehl tomorrow that might be of interest to you and others in CS/TTIC. I'd appreciate it if you could forward it to whatever mailing lists you think are appropriate.
> 
> Thanks,
> 
>     Denis
> 
> ________________________________________
> From: full_math-request at lists.uchicago.edu <full_math-request at lists.uchicago.edu> on behalf of Akhil Mathew <amathew at math.uchicago.edu>
> Sent: Sunday, April 23, 2023 9:50 AM
> To: all at math.uchicago.edu
> Subject: Emily Riehl speaks in AT seminar (4/25)
> 
> Emily Riehl (Johns Hopkins University) will speak in the algebraic
> topology seminar on Tuesday (4/25). The seminar will meet in E308 from
> 4-5pm, preceded by a
> pretalk from 2:40-3:40pm.
> 
> Talk Title: Infinity-category theory for undergraduates
> 
> Abstract:
> At its current state of the art, infinity-category theory is
> challenging to explain even to specialists in closely related
> mathematical areas. Nevertheless, historical experience suggests that
> in, say, a century's
> time, we will routinely teach this material to undergraduates. This talk
> describes one dream about how this might come about --- under the
> assumption that 22nd century undergraduates have absorbed the
> background intuitions of homotopy type theory/univalent foundations. If time
> permits, we'll share a new computer formalized proof of the
> infinity-categorical Yoneda lemma in this formal system that reveals
> how close it is to the classical proof of the 1-categorical Yoneda
> lemma.
> 
> Pretalk Title: Homotopy type theory and univalent foundations
> 
> Abstract: This talk will introduce an alternative foundation system
> for mathematics in which "equality" becomes "identity," which is no
> longer a mere predicate but can carry structure. The primitive notion
> is called a "type," which can be interpreted as something like a set,
> or as something like a mathematical proposition, or as a something
> like a groupoid or moduli space, which has higher structure. What
> Voevodsky named the "univalent foundations of mathematics" arose from
> a recently discovered homotopy theoretic interpretation of dependent
> type theory, originally designed as a formal system for constructive
> mathematics. We will introduce this formal system, explore Voevodsky's
> univalence axiom and its consequences, and discuss advantages for
> computer formalization.

Peace,

Stu

---------------

Stuart A. Kurtz
George and Elizabeth Yovovich Professor, Department of Computer Science and the College
Master, Physical Sciences Collegiate Division
The University of Chicago



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mailman.cs.uchicago.edu/pipermail/theory/attachments/20230424/7a812cf1/attachment.html>