Elisabeth Bonnevier: Formalizing Cartesian Cubical Sets in UniMath

MsC Project

Tid: Må 2020-03-30 kl 09.30 - 10.30

Föreläsare: Elisabeth Bonnevier

Plats: Zoom, Meeting ID: 788 997 020

Handledare: Anders Mörtberg

Abstract

Homotopy type theory is a new formal system for doing constructive mathematics. As a system for logical deductions, its consistency must be verified by models. We will look at an axiomatization of constructive presheaf models of homotopy type theory and show that cartesian cubical sets satisfy four of these axioms. These results are formalized using the UniMath library for the proof assistant Coq, to which we also give an introduction.

Innehållsansvarig:webmaster@math.kth.se
Tillhör: Institutionen för matematik
Senast ändrad: 2020-03-26