Formalizing and comparing categorical structures for type dependency
Master Project

Project Description

Different categorical structures have been devised and studied for the purpose of interpreting (that is, giving denotational semantics to) dependently-typed theories. The paper “Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories” aims to give a rigorous comparison between these different structures.

The goal of this project is to formalize (some of) the results of this paper in the UniMath library, a library of mathematics (and, in particular, category theory) based on univalent mathematics written in the computer proof assistant Coq.

Links:

• https://link.springer.com/chapter/10.1007/978-981-97-8943-6_1 (seems to be behind a paywall, get in touch with Benedikt to obtain a copy)

Project Goals

In this project, you will work on the following goals:

• Learn the basics of univalent mathematics
• Learn to use the computer proof assistants Coq and the library UniMath written in Coq
• Understand the paper “Weakest preconditions in fibrations”
• Formalize the definitions, statements, and proofs of this paper in UniMath

Contacts for the Project

• Benedikt Ahrens (TU Delft)
• Kobe Wullaert (TU Delft)