Seminars Sorted by Series

Homotopy Type Theory in Coq

Type Systems and Proof Assistant

Toward a Computational Interpretation of Univalence

Type Systems

On the Setoid Model of Type Theory

Type Systems

Kan Simplicial Set Model of Type Theory

Type Systems (continued)

Kan Simplicial Set Model of Type Theory (continued)

Toward Higher Inductive Types

The Simplicial Model of UA

Type Systems

Type Systems

The Simplicial Model of Univalence

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