Weak omega-categories from intensional type theory
We show that for any type in Martin-L\"of Intensional Type Theory, the terms of that type and its higher identity types form a weak omega-category in the sense of Leinster. Precisely, we construct a contractible globular operad of definable composition laws, and give an action of this operad on...
| मुख्य लेखक: | |
|---|---|
| स्वरूप: | लेख |
| भाषा: | English |
| प्रकाशित: |
Logical Methods in Computer Science e.V.
2010-09-01
|
| श्रृंखला: | Logical Methods in Computer Science |
| विषय: | |
| ऑनलाइन पहुंच: | https://lmcs.episciences.org/1062/pdf |