A type theory for Cartesian closed bicategories

DOI10.5555/3470152.3470190MaRDI QIDQ6654504zbMATH OpenFDO

Authors Marcelo P. Fiore, Philip Saville

Publication date 19 December 2024

Full work available at URL https://doi.org/10.5555/3470152.3470190

zbMATH Keywords

Cartesian closed bicategoriesCurry-Howard-Lambek correspondencehigher category theorytyped lambda calculus

Mathematics Subject Classification ID

Type theory (03B38) Combinatory logic and lambda calculus (03B40) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) 2-categories, bicategories, double categories (18N10)

Recommendations

• Coherence for bicategorical cartesian closed structure
• Coherence and normalisation-by-evaluation for bicategorical Cartesian closed structure
• Relative full completeness for bicategorical Cartesian closed structure
• A Cartesian bicategory of polynomial functors in homotopy type theory
• scientific article; zbMATH DE number 1497809

Cited in

(5)

• Relative full completeness for bicategorical Cartesian closed structure
• From thin concurrent games to generalized species of structures (extended version)
• Effectful semantics in 2-dimensional categories: premonoidal and Freyd bicategories
• Effectful semantics in bicategories: strong, commutative, and concurrent pseudomonads
• A 2-categorical approach to the semantics of dependent type theory with computation axioms

This page was built for publication: A type theory for Cartesian closed bicategories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6654504)