An Internal Logic of Virtual Double Categories
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866929684363608064 |
|---|---|
| author | Nasu, Hayato |
| author_facet | Nasu, Hayato |
| contents | We present a type theory called fibrational virtual double type theory (FVDblTT) designed specifically for formal category theory, which is a succinct reformulation of New and Licata's Virtual Equipment Type Theory (VETT). FVDblTT formalizes reasoning on isomorphisms that are commonly employed in category theory. Virtual double categories are one of the most successful frameworks for developing formal category theory, and FVDblTT has them as a theoretical foundation. We validate its worth as an internal language of virtual double categories by providing a syntax-semantics duality between virtual double categories and specifications in FVDblTT as a biadjunction. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_06792 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | An Internal Logic of Virtual Double Categories Nasu, Hayato Category Theory Logic in Computer Science 18C50, 18D70, 18N10(Primary) 68Q65, 18D60 (Secondary) We present a type theory called fibrational virtual double type theory (FVDblTT) designed specifically for formal category theory, which is a succinct reformulation of New and Licata's Virtual Equipment Type Theory (VETT). FVDblTT formalizes reasoning on isomorphisms that are commonly employed in category theory. Virtual double categories are one of the most successful frameworks for developing formal category theory, and FVDblTT has them as a theoretical foundation. We validate its worth as an internal language of virtual double categories by providing a syntax-semantics duality between virtual double categories and specifications in FVDblTT as a biadjunction. |
| title | An Internal Logic of Virtual Double Categories |
| topic | Category Theory Logic in Computer Science 18C50, 18D70, 18N10(Primary) 68Q65, 18D60 (Secondary) |
| url | https://arxiv.org/abs/2410.06792 |