Showing 1–2 of 2 results for author: Gambino, N

Monoidal bicategories, differential linear logic, and analytic functors

Authors: M. Fiore, N. Gambino, M. Hyland

Abstract: We develop further the theory of monoidal bicategories by introducing and studying bicategorical counterparts of the notions of a linear explonential comonad, as considered in the study of linear logic, and of a codereliction transformation, introduced to study differential linear logic via differential categories. As an application, we extend the differential calculus of Joyal's analytic functors… ▽ More We develop further the theory of monoidal bicategories by introducing and studying bicategorical counterparts of the notions of a linear explonential comonad, as considered in the study of linear logic, and of a codereliction transformation, introduced to study differential linear logic via differential categories. As an application, we extend the differential calculus of Joyal's analytic functors to analytic functors between presheaf categories, just as ordinary calculus extends from a single variable to many variables. △ Less

Submitted 23 May, 2024; v1 submitted 9 May, 2024; originally announced May 2024.

Comments: v2: fixed typos, added references. 46 pages. Comments welcome

MSC Class: 18N10; 18M45; 18F40; 18D60; 18M80

Inductive types in homotopy type theory

Authors: Steve Awodey, Nicola Gambino, Kristina Sojakova

Abstract: Homotopy type theory is an interpretation of Martin-Löf's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional systems of type theory as well as a computational approach to algebraic topology via type theory-based proof assistants such as Coq. The present work investig… ▽ More Homotopy type theory is an interpretation of Martin-Löf's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional systems of type theory as well as a computational approach to algebraic topology via type theory-based proof assistants such as Coq. The present work investigates inductive types in this setting. Modified rules for inductive types, including types of well-founded trees, or W-types, are presented, and the basic homotopical semantics of such types are determined. Proofs of all results have been formally verified by the Coq proof assistant, and the proof scripts for this verification form an essential component of this research. △ Less

Submitted 2 May, 2012; v1 submitted 18 January, 2012; originally announced January 2012.

Comments: 19 pages; v2: added references and acknowledgements, removed appendix with Coq README file, updated URL for Coq files. To appear in the proceedings of LICS 2012

MSC Class: 03B15; 03B70; 03F50