YoVDO

Univalence from a Computer Science Point-of-View - Dan Licata

Offered By: Institute for Advanced Study via YouTube

Tags

Type Theory Courses Theoretical Computer Science Courses Homotopy Theory Courses

Course Description

Overview

Explore univalence from a computer science perspective in this 56-minute conference talk by Dan Licata from Wesleyan University, presented at the Vladimir Voevodsky Memorial Conference hosted by the Institute for Advanced Study. Delve into topics such as Martin-Löf type theory, coproduct injection, computation, canonicity theorem, and the Univalence Axiom. Examine constructive cubical models, main ideas in recommender systems, and the application of Z in type theory. Investigate the equivalence of different concepts, group structures, and geometric constructs like circles, universal covers, and tori. Gain insights into synthetic homotopy theory, Brunerie's number, and various computer science applications before concluding with a Q&A session.

Syllabus

Intro
Martin-Löf type theory
coproduct injection is parity
Computation
Canonicity theorem
Univalence Axiom
Progress
Constructive Cubical Models
Main Ideas
Recommender System
Z in type theory (1)
addition (1)
Equivalence of (1) and (3)
Using univalence
Group structure
Without univalence
Circle
Universal Cover
Torus
Synth homotopy theory
Brunerie's number
CS Applications
Questions


Taught by

Institute for Advanced Study

Related Courses

Lie Algebras and Homotopy Theory - Jacob Lurie
Institute for Advanced Study via YouTube
Artin Reciprocity via Spheres
Fields Institute via YouTube
Basic Homotopy Theory by Samik Basu
International Centre for Theoretical Sciences via YouTube
Star Clusters in Clique Complexes and the Vietoris-Rips Complex of Planar Sets
Applied Algebraic Topology Network via YouTube
Invariants for Tame Parametrised Chain Complexes
Applied Algebraic Topology Network via YouTube