Commit 79edc31a authored by Jakob von Raumer's avatar Jakob von Raumer

update readme

parent eea119cd
......@@ -30,6 +30,11 @@ Locally confluent relations and the main theorem (Theorem 42) of the paper.
The further main results of our paper: Theorem 43 and Theorem 12.
## src/freegrp.lean
Contains the proof that the reduction relation on the free group on a given type is
locally confluent.
# Path Spaces of Higher Inductive Types
This repository furthermore contains the formalizations for the paper "Path Spaces of Higher Inductive Types in Homotopy Type Theory" by Nicolai Kraus and Jakob von Raumer. This file describes some of the contents and connects them to the respective definitions and propositions of the paper.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment