Seminars Sorted by Series

Type Systems

The Simplicial Model of Univalence

Type Systems

Invariance Under Isomorphism and Definability

The Type System TS

Constructing HITs in a Realizability Model

Simplicial Types

State of the New Proof Assistant

Homotopy and Univalence

Orthogonal factorization in HoTT

Weak Infinity Groupoids in HoTT

The Calculus of Opetopes

A Quillen Model Structure in Type Theory

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

The Hopf Fibration via Higher Inductive Types

On Finite Types That Are Not h-Sets

pi_2(s^2) in HoTT

Locally Cartesian Closed Infinity Categories

Semantics of Higher Inductive Types

Formal Abstract Homotopy Theory

Cohomology in Homotopy Type Theory

Setoids, e-Categories, and Exact Completions

Eilenberg-Mac Lane Spaces in HoTT

Homotopy Colimits and a Descent Theorem

Gluing in Homotopy Type Theory

A Proof Assistant Prototype Based on Algebraic Effects and Handlers

Substructural Type Theory

The James Construction and pi_4(S^3)

Natural Models of Type Theory

On the Category of hSets

HoTT is a Polyvalent Foundation of Mathemtics

Directed Type Theory

Homotopy Type Theory

Simplicial Set