Name
Abstract | ||
|---|---|---|
Weak ω-groupoids are the higher dimensional generalisation of setoids and are an essential ingredient of the constructive semantics of Homotopy Type Theory [13]. Following up on our previous formalisation [3] and Brunerie's notes [6], we present a new formalisation of the syntax of weak ω-groupoids in Agda using heterogeneous equality. We show how to recover basic constructions on ω-groupoids using suspension and replacement. In particular we show that any type forms a groupoid and we outline how to derive higher dimensional composition. We present a possible semantics using globular sets and discuss the issues which arise when using globular types instead. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1145/2631172.2631176 | LFMTP |
Keywords | Field | DocType |
higher dimensional structures,mathematical logic,agda,category theory,homotopy type theory,type theory,theory,formalisation | Generalization,Constructive,Pure mathematics,Type theory,Homotopy type theory,Agda,Category theory,Syntax,Semantics,Mathematics | Conference |
Citations | PageRank | References |
0 | 0.34 | 3 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Thorsten Altenkirch | 1 | 668 | 56.85 |
| Nuo Li | 2 | 4 | 2.14 |
| Ondrej Rypacek | 3 | 8 | 1.92 |