A type theory for Cartesian closed bicategories

DOI10.5555/3470152.3470190MaRDI QIDQ6654504zbMATH OpenFDO

Authors Marcelo P. Fiore, Philip Saville

Publication date 19 December 2024

zbMATH Keywords

higher category theorytyped lambda calculusCurry-Howard-Lambek correspondenceCartesian closed bicategories

Mathematics Subject Classification ID

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

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

(1)

• Relative full completeness for bicategorical Cartesian closed structure

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)