সংরক্ষণ করুন:
| প্রধান লেখক: | , , |
|---|---|
| বিন্যাস: | Preprint |
| প্রকাশিত: |
2021
|
| বিষয়গুলি: | |
| অনলাইন ব্যবহার করুন: | https://arxiv.org/abs/2106.04475 |
| ট্যাগগুলো: |
ট্যাগ যুক্ত করুন
কোনো ট্যাগ নেই, প্রথমজন হিসাবে ট্যাগ করুন!
|
সূচিপত্রের সারণি:
- We study the dependent type theory CaTT, introduced by Finster and Mimram, which presents the theory of weak $ω$-categories, following the idea that type theories can be considered as presentations of generalized algebraic theories. Our main contribution is a formal proof that the models of this type theory correspond precisely to weak $ω$-categories, as defined by Maltsiniotis, by generalizing a definition proposed by Grothendieck for weak $ω$-groupoids: Those are defined as suitable presheaves over a cat-coherator, which is a category encoding structure expected to be found in an $ω$-category. This comparison is established by proving the initiality conjecture for the type theory CaTT, in a way which suggests the possible generalization to a nerve theorem for a certain class of dependent type theories