# A type theory for cartesian closed bicategories

@article{Fiore2019ATT, title={A type theory for cartesian closed bicategories}, author={Marcelo P. Fiore and Philip Saville}, journal={ArXiv}, year={2019}, volume={abs/1904.06538} }

We construct an internal language for cartesian closed bicategories. Precisely, we introduce a type theory modelling the structure of a cartesian closed bicategory and show that its syntactic model satisfies an appropriate universal property, thereby lifting the Curry-Howard-Lambek correspondence to the bicategorical setting. Our approach is principled and practical. Weak substitution structure is constructed using a bicategorification of the notion of abstract clone from universal algebra, and… Expand

#### Supplemental Presentations

#### 3 Citations

Relative Full Completeness for Bicategorical Cartesian Closed Structure

- Computer Science
- FoSSaCS
- 2020

The glueing construction is extended to accommodate ‘2-dimensional theories’ of types, terms between types, and rewrites between terms and it is shown that free finite-product bicategories are fully complete relative to free cartesian closed bic categories, thereby establishing that the higher-order equational theory of rewriting in the simply-typed lambda calculus is a conservative extension of the algebraic equations. Expand

Cartesian closed bicategories: type theory and coherence

- Mathematics, Computer Science
- ArXiv
- 2020

In this thesis I lift the Curry--Howard--Lambek correspondence between the simply-typed lambda calculus and cartesian closed categories to the bicategorical setting, then use the resulting type… Expand

Coherence and normalisation-by-evaluation for bicategorical cartesian closed structure

- Mathematics, Computer Science
- LICS
- 2020

It is shown that in the free cartesian closed bicategory on a set of objects there is at most one structural 2-cell between any parallel pair of 1-cells, which will reduce the difficulty of constructing structure in arbitrary cartesianclosed bicategories to the level of1-dimensional category theory. Expand

#### References

SHOWING 1-10 OF 61 REFERENCES

A type theory for cartesian closed bicategories (Extended Abstract)

- Computer Science
- 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
- 2019

This work introduces a type theory modelling the structure of a cartesian closed bicategory and shows that its syntactic model satisfies an appropriate universal property, thereby lifting the Curry-Howard-Lambek correspondence to the bicategorical setting. Expand

The cartesian closed bicategory of generalised species of structures

- Mathematics
- 2008

AbstractThe concept of generalised species of structures between small categories and, correspondingly, that of generalised analytic functor between presheaf categories are introduced. An operation… Expand

Towards a proof theory of rewriting: the simply typed 2l-calculus

- Mathematics
- 1996

Abstract This paper describes the simply typed 2λ-calculus, a language with three levels: types, terms and rewrites. The types and terms are those of the simply typed λ-calculus, and the rewrites are… Expand

Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures

- Mathematics
- 2016

We introduce the notion of a relative pseudomonad, which generalizes the notion of a pseudomonad, and define the Kleisli bicategory associated to a relative pseudomonad. We then present an efficient… Expand

2-Dimensional Directed Type Theory

- Computer Science, Mathematics
- MFPS
- 2011

A 2-dimensional directed type theory, or 2DTT, is described, validated by an interpretation into the strict 2-category Cat of categories, functors, and natural transformations, which associates each type with a directed notion of transformation between its elements. Expand

An Algebraic Presentation of Predicate Logic - (Extended Abstract)

- Mathematics, Computer Science
- FoSSaCS
- 2013

A syntax-free representation theorem is provided which places terms in bijection with sieves, a concept from category theory, and it is shown that parameterized algebraic theories characterize a class of enriched monads. Expand

A type theory for synthetic ∞-categories

- Mathematics
- 2018

We propose foundations for a synthetic theory of $(\infty,1)$-categories within homotopy type theory. We axiomatize a directed interval type, then define higher simplices from it and use them to… Expand

Semantic analysis of normalisation by evaluation for typed lambda calculus

- Computer Science
- PPDP '02
- 2002

This paper analyses the lambda definability result of Jung and Tiuryn via Kripke logical relations and shows how it can be adapted to unify definability and normalisation, yielding an extensional normalisation result. Expand

A theory of recursive domains with applications to concurrency

- Mathematics, Computer Science
- Proceedings. Thirteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.98CB36226)
- 1998

A 2-categorical theory for recursively defined domains is developed that generalises the traditional approach based on order- theoretic structures to category-theoretic ones and uses the framework to study (open-map) bisimulation. Expand

The Virtues of Eta-Expansion

- Computer Science
- J. Funct. Program.
- 1995

Interpreting η-conversion as an expansion rule in the simply-typed λ-calculus maintains the confluence of reduction in a richer type structure. This use of expansions is supported by categorical… Expand