An Internal Logic of Virtual Double Categories

Hayato Nasu

An Internal Logic of Virtual Double Categories

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2410.06792 v2 pith:3FCTTQMN submitted 2024-10-09 math.CT cs.LO

Hayato Nasu This is my paper · ORCID

classification math.CTcs.LO

keywords theoryvirtualdoublecategoriesfvdblttcategorytypeformal

verification ladder T0 review T1 audit T2 compute T3 formal

0 comments

read the original abstract

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.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

Logical Aspects of Virtual Double Categories
math.CT 2025-01 conditional novelty 6.0 of 10

Elementary existential fibrations correspond exactly to cartesian equipments obtained via the new /BU il construction, and regular fibrations correspond to those with Beck-Chevalley pullbacks.

Pith tools