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/ |
| _version_ | 1848793554986467328 |
|---|---|
| author | Altenkirch, Thorsten Li, Nuo Ondřej, Rypáček |
| author_facet | Altenkirch, Thorsten Li, Nuo Ondřej, Rypáček |
| author_sort | Altenkirch, Thorsten |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | 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. |
| first_indexed | 2025-11-14T19:02:09Z |
| format | Conference or Workshop Item |
| id | nottingham-28381 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T19:02:09Z |
| publishDate | 2014 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-283812020-05-04T20:16:04Z https://eprints.nottingham.ac.uk/28381/ Some constructions on ω-groupoids Altenkirch, Thorsten Li, Nuo Ondřej, Rypáček 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. 2014 Conference or Workshop Item PeerReviewed Altenkirch, Thorsten, Li, Nuo and Ondřej, Rypáček (2014) Some constructions on ω-groupoids. In: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP '14), 17 Jul 2014, Vienna, Austria. Logic Programming Groupoids http://dl.acm.org/citation.cfm?doid=2631172.2631176 |
| spellingShingle | Logic Programming Groupoids Altenkirch, Thorsten Li, Nuo Ondřej, Rypáček Some constructions on ω-groupoids |
| title | Some constructions on ω-groupoids |
| title_full | Some constructions on ω-groupoids |
| title_fullStr | Some constructions on ω-groupoids |
| title_full_unstemmed | Some constructions on ω-groupoids |
| title_short | Some constructions on ω-groupoids |
| title_sort | some constructions on ω-groupoids |
| topic | Logic Programming Groupoids |
| url | https://eprints.nottingham.ac.uk/28381/ https://eprints.nottingham.ac.uk/28381/ |