M-Types in Homotopy Type Theory

Terminal semantics for codata types in intensional Martin-Löf type theory

Univalent categories and the Rezk completion

Initiality for Typed Syntax and Semantics


This page was last updated at 2018-06-21 06:49:25 -0700
This site is compiled with nanoc. Built from code written by Cyril Cohen.