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 2017-03-05 22:28:21 +0100
This site is compiled with nanoc. Built from code written by Cyril Cohen.