Globular multicategories with homomorphism types
We introduce various notions of globular multicategory with homomorphism types. We develop a higher dimensional modules construction that constructs globular multicategories with strict homomorphism types. We illustrate how this construction is related to iterated enrichment. We show how various col...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | English |
| Published: |
2022
|
| Subjects: |
| _version_ | 1826311152696557568 |
|---|---|
| author | Dean, CJ |
| author2 | Kremnitzer, Y |
| author_facet | Kremnitzer, Y Dean, CJ |
| author_sort | Dean, CJ |
| collection | OXFORD |
| description | We introduce various notions of globular multicategory with homomorphism types. We develop a higher dimensional modules construction that constructs globular multicategories with strict homomorphism types. We illustrate how this construction is related to iterated enrichment. We show how various collections of “higher category-like”objects give rise to globular multicategories with homomorphism types. We show how these structures suggest a new globular approach to the semantics of (directed) homotopy type theory. |
| first_indexed | 2024-03-07T08:04:08Z |
| format | Thesis |
| id | oxford-uuid:c42f6774-c44c-4dd2-aa13-5e7c1ca96a96 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T08:04:08Z |
| publishDate | 2022 |
| record_format | dspace |
| spelling | oxford-uuid:c42f6774-c44c-4dd2-aa13-5e7c1ca96a962023-10-18T09:13:53ZGlobular multicategories with homomorphism typesThesishttp://purl.org/coar/resource_type/c_db06uuid:c42f6774-c44c-4dd2-aa13-5e7c1ca96a96Dependent Type theoryCategories (Mathematics)EnglishHyrax Deposit2022Dean, CJKremnitzer, YVicary, JDouglas, CAwodey, SWe introduce various notions of globular multicategory with homomorphism types. We develop a higher dimensional modules construction that constructs globular multicategories with strict homomorphism types. We illustrate how this construction is related to iterated enrichment. We show how various collections of “higher category-like”objects give rise to globular multicategories with homomorphism types. We show how these structures suggest a new globular approach to the semantics of (directed) homotopy type theory. |
| spellingShingle | Dependent Type theory Categories (Mathematics) Dean, CJ Globular multicategories with homomorphism types |
| title | Globular multicategories with homomorphism types |
| title_full | Globular multicategories with homomorphism types |
| title_fullStr | Globular multicategories with homomorphism types |
| title_full_unstemmed | Globular multicategories with homomorphism types |
| title_short | Globular multicategories with homomorphism types |
| title_sort | globular multicategories with homomorphism types |
| topic | Dependent Type theory Categories (Mathematics) |
| work_keys_str_mv | AT deancj globularmulticategorieswithhomomorphismtypes |