Popular repositories Loading

1. Three-HITs Three-HITs Public

   All higher inductive types can be obtained from three simple HITs.

   Coq 17 2

2. groupoids groupoids Public

   Groupoids vs 1-Types

   Coq 10 1

3. HITs-Examples HITs-Examples Public

   Examples of Higher Inductive Types

   Coq 7

4. RezkCompletion RezkCompletion Public

   The Rezk completion as a higher inductive types

   Coq 7

5. nmvdw.github.io nmvdw.github.io Public

   HTML 2 1

6. Finite-Bags Finite-Bags Public

   Coq 1