Some constructions on ω-groupoids

Altenkirch, Thorsten; Li, Nuo; Ond?ej, Ryp�?ek

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. © 2014 ACM.

Citation

Altenkirch, T., Li, N., & Ondřej, R. (2014, July). Some constructions on ω-groupoids. Presented at LFMTP '14: Theory and Practice, Vienna, Austria

• Presentation Conference Type: Edited Proceedings
• Conference Name: LFMTP '14: Theory and Practice
• Start Date: Jul 17, 2014
• End Date: Jul 17, 2014
• Acceptance Date: Jan 1, 2014
• Publication Date: Jul 17, 2014
• Deposit Date: Mar 15, 2015
• Publicly Available Date: Mar 15, 2015
• Publisher: Association for Computing Machinery (ACM)
• Peer Reviewed: Peer Reviewed
• Article Number: 4
• Book Title: LFMTP '14: Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice
• ISBN: 9781450328173
• DOI: https://doi.org/10.1145/2631172.2631176
• Keywords: Logic Programming, Groupoids
• Public URL: https://nottingham-repository.worktribe.com/output/997876
• Publisher URL: http://dl.acm.org/citation.cfm?doid=2631172.2631176