Univalence from a Computer Science Point-of-View - Dan Licata
Institute for Advanced Study via YouTube
Overview
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