THORSTEN ALTENKIRCH THORSTEN.ALTENKIRCH@NOTTINGHAM.AC.UK
Professor of Computer Science
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
omega.pdf
(308 Kb)
PDF
You might also like
Should Type Theory Replace Set Theory as the Foundation of Mathematics?
(2023)
Journal Article
Constructing a universe for the setoid model
(2021)
Conference Proceeding
Big Step Normalisation for Type Theory
(2020)
Journal Article
Naive Type Theory
(2019)
Book Chapter
Towards a cubical type theory without an interval
(2018)
Journal Article
Downloadable Citations
About Repository@Nottingham
Administrator e-mail: digital-library-support@nottingham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search