Univalent

video lecture

"Setoids, e-Categories, and Exact Completions"

March 07, 2013

Richard Garner

video lecture

Eilenberg-Mac Lane Spaces in HoTT

March 13, 2013

video lecture

Formal Abstract Homotopy Theory

February 28, 2013

Jeremy Avigad

video lecture

Semantics of Higher Inductive Types

February 27, 2013

Michael Shulman

video lecture

$pi_2(s^2)$ in HoTT

February 20, 2013

Guillaume Brunerie

video lecture

Locally Cartesian Closed Infinity Categories

February 21, 2013

Joachim Kock

video lecture

Cohomology in Homotopy Type Theory

March 06, 2013

Eric Finster

video lecture

On Finite Types That Are Not h-Sets

February 14, 2013

Sergey Melikhov

video lecture

The Hopf Fibration via Higher Inductive Types

February 13, 2013

Peter Lumsdaine

video lecture

Isomorphic Structures of any Kind are `Equal' in HoTT: But What is a Kind of Structure?

February 07, 2013

Peter Aczel