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 |
| id |
nottingham-28381 |
|---|---|
| recordtype |
eprints |
| spelling |
nottingham-283812017-10-18T17:24:19Z http://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 application/pdf en http://eprints.nottingham.ac.uk/28381/1/omega.pdf Altenkirch, Thorsten and 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. http://dl.acm.org/citation.cfm?doid=2631172.2631176 |
| repository_type |
Digital Repository |
| institution_category |
Local University |
| institution |
University of Nottingham Malaysia Campus |
| building |
Nottingham Research Data Repository |
| collection |
Online Access |
| language |
English |
| 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. |
| format |
Conference or Workshop Item |
| author |
Altenkirch, Thorsten Li, Nuo Ondřej, Rypáček |
| spellingShingle |
Altenkirch, Thorsten Li, Nuo Ondřej, Rypáček Some constructions on ω-groupoids |
| author_facet |
Altenkirch, Thorsten Li, Nuo Ondřej, Rypáček |
| author_sort |
Altenkirch, Thorsten |
| title |
Some constructions on ω-groupoids |
| title_short |
Some constructions on ω-groupoids |
| title_full |
Some constructions on ω-groupoids |
| title_fullStr |
Some constructions on ω-groupoids |
| title_full_unstemmed |
Some constructions on ω-groupoids |
| title_sort |
some constructions on ω-groupoids |
| publishDate |
2014 |
| url |
http://eprints.nottingham.ac.uk/28381/ http://eprints.nottingham.ac.uk/28381/ http://eprints.nottingham.ac.uk/28381/1/omega.pdf |
| first_indexed |
2018-09-06T11:49:10Z |
| last_indexed |
2018-09-06T11:49:10Z |
| _version_ |
1610858679870947328 |