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 |