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: | Dean, CJ |
---|---|
Other Authors: | Kremnitzer, Y |
Format: | Thesis |
Language: | English |
Published: |
2022
|
Subjects: |
Similar Items
-
Globular: an online proof assistant for higher-dimensional rewriting
by: Krzysztof Bar, et al.
Published: (2018-01-01) -
Algebraic coherent confluence and higher globular Kleene algebras
by: Cameron Calk, et al.
Published: (2022-11-01) -
2-adjoint equivalences in homotopy type theory
by: Daniel Carranza, et al.
Published: (2021-01-01) -
Lax orthogonal factorisations in monad-quantale-enriched categories
by: Maria Manuel Clementino, et al.
Published: (2017-09-01) -
Weak omega-categories from intensional type theory
by: Peter LeFanu Lumsdaine
Published: (2010-09-01)