4

Toward a cubical type theory univalent by definition
Supervised by Hugo Herbelin.
Cubical Type Theory provides a computational meaning to Voevodsky’s univalence axiom. It uses an abstract …
Hugo Moeneclaey
PDF Cite
Monoids up to coherent homotopy in two-level type theory
Supervised by Peter LeFanu Lumsdaine.
We present a formalization of monoids up to coherent homotopy in Agda. In order to achieve this …
Hugo Moeneclaey
PDF Cite
Expansion proofs for arithmetic
Supervised by Setfan Hetzl.
We present two extensions of expansion proofs to arithmetic. We define expansion proofs with induction, and …
Hugo Moeneclaey
PDF Cite
A schema for higher inductive types of level one and its interpretation
Supervised by Peter Dybjer.
We present a general schema for (non-dependent) higher inductive types built using only point and path …
Hugo Moeneclaey
PDF Cite