View Proposal

---

Proposer

James McKinna

Title

Simplicial Objects in Dependent Type Theory

Goal

Formal prof development in the Agda interactive theorem prover

Description

There has been much recent interest from the mathematics community in so-called *cubical type theory*, a development of intuitionistic type theory in which homotopy-theoretic structure and results may be developed synthetically. Classical structures in homotopy theory include the so called simplicial category, %Delta$ and simnplicial structures, considered as presheaves on $Delta$ with values in suitable categories of interest. Mac lane's "Categories for the Working Mathematician" contains the essential material with which to begin the project. The aim of this project is to develop the general theory of such structures in the Agda theorem prover, an implementation of intuitionistic type theory, and specifically to do so on top of the existing standard library Data.Fin of the dependent family `Fin n` (for `n : Nat`) of finite types. This project is suitable for mathematics students, and mathematically inclined computer science students interested in developing a chapter of classical mathematics in a formalised setting.

Resources

Standard computing facilities

Background

Famiiarity with Agda theorem prover a bonus

Url

Difficulty Level

Challenging

Ethical Approval

None

Number Of Students

1

Supervisor

James McKinna

Keywords

Degrees