Skip to main content

Research Repository

Advanced Search

Some constructions on ?-groupoids

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

Authors

Nuo Li

Ryp�?ek Ond?ej



Abstract

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.

Citation

Altenkirch, T., Li, N., & Ond?ej, R. (2014). Some constructions on ?-groupoids. . https://doi.org/10.1145/2631172.2631176

Conference Name International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP '14)
Conference Location Vienna, Austria
Start Date Jul 14, 2014
End Date Jul 14, 2014
Acceptance Date Jan 1, 2014
Publication Date Jul 17, 2014
Deposit Date Mar 15, 2015
Publicly Available Date Mar 28, 2024
Publisher Association for Computing Machinery (ACM)
Peer Reviewed Peer Reviewed
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
Additional Information Published in: LFMTP 2014: proceedings of the Ninth International Workshop on Logical Frameworks and Meta-Languages: Theory & Practice: July 17, 2014, Vienna, Austria. New York : Association for Computing Machinery, 2014, ISBN: 978-1-4503-2817-3. Article no. 4, doi: 10.1145/2631172.2631176

Files





You might also like



Downloadable Citations