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 |
| Published: |
2014
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/28381/ |