Some constructions on ω-groupoids
Weak ω-groupoids are the higher dimensional generalisation of setoids and are an essential ingredient of the construc- tive semantics of Homotopy Type Theory [10]. Following up on our previous formalisation [3] and Brunerie’s notes [5], we present a new formalisation of the syntax of weak ω- groupoi...
| Main Authors: | , , |
|---|---|
| Format: | Conference or Workshop Item |
| Language: | English |
| Published: |
2014
|
| Online Access: | http://eprints.nottingham.ac.uk/28381/ http://eprints.nottingham.ac.uk/28381/ http://eprints.nottingham.ac.uk/28381/1/omega.pdf |
| Summary: | Weak ω-groupoids are the higher dimensional generalisation of setoids and are an essential ingredient of the construc- tive semantics of Homotopy Type Theory [10]. Following up on our previous formalisation [3] and Brunerie’s notes [5], 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 sus- pension 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. |
|---|