Categories with Families: Unityped, Simply Typed, and Dependently Typed

TL;DR

This paper explores the categorical logic of various lambda calculus forms through categories with families, establishing equivalences and biequivalences with fundamental categorical structures and discussing initial object constructions.

Contribution

It introduces subcategories of cwfs, such as scwfs and ucwfs, and proves several categorical equivalence and biequivalence theorems relating them to key categorical concepts.

Findings

Established equivalences between cwfs and categorical logic structures

Defined subcategories with simplified type dependencies

Discussed constructions of initial cwfs with extra structure

Abstract

We show how the categorical logic of untyped, simply typed and dependently typed lambda calculus can be structured around the notion of category with family (cwf). To this end we introduce subcategories of simply typed cwfs (scwfs), where types do not depend on variables, and unityped cwfs (ucwfs), where there is only one type. We prove several equivalence and biequivalence theorems between cwf-based notions and basic notions of categorical logic, such as cartesian operads, Lawvere theories, categories with finite products and limits, cartesian closed categories, and locally cartesian closed categories. Some of these theorems depend on the restrictions of contextuality (in the sense of Cartmell) or democracy (used by Clairambault and Dybjer for their biequivalence theorems). Some theorems are equivalences between notions with strict preservation of chosen structure. Others are biequivalences between notions where properties are only preserved up to isomorphism. In addition to this we discuss various constructions of initial ucwfs, scwfs, and cwfs with extra structure.

Figures

Equations

$$\Gamma$$

$$\Gamma \mathtt{context}$$

$$\Gamma ={\Gamma }^{\prime }$$

$$\Delta \to \gamma :\Gamma$$

$$\Delta \to \gamma ={\gamma }^{\prime }:\Gamma$$

$$T(\gamma ):(\mathrm{Tm}(\Gamma ,A){)}_{A\in \mathrm{Ty}(\Gamma )}\to (\mathrm{Tm}(\Delta ,B){)}_{B\in \mathrm{Ty}(\Delta )}$$

$${\mathrm{p}}_{\Gamma ,A}:\Gamma \cdot A\to \Gamma {\mathrm{q}}_{\Gamma ,A}\in \mathrm{Tm}(\Gamma \cdot A,A[{\mathrm{p}}_{\Gamma ,A}])$$

$${\mathrm{p}}_{\Gamma ,A}\circ ⟨\gamma ,a⟩=\gamma {\mathrm{q}}_{\Gamma ,A}[⟨\gamma ,a⟩]=a.$$

$$l:{\mathcal{C}}_0\to \mathbb{N},$$

$${\gamma }_{\Gamma }:\Gamma \cong 1.\overline{\Gamma }$$

$$\sigma :T_{\mathcal{C}}\Rightarrow T_{\mathcal{D}}\circ F$$

$${\sigma }_{\Gamma }:{\mathrm{Ty}}_{\mathcal{C}}(\Gamma )\to {\mathrm{Ty}}_{\mathcal{D}}(F\Gamma )$$

$${\sigma }_{\Gamma }^A:{\mathrm{Tm}}_{\mathcal{C}}(\Gamma ,A)\to {\mathrm{Tm}}_{\mathcal{D}}(F\Gamma ,{\sigma }_{\Gamma }(A))$$

$$F(A[\gamma ])=(FA)[F\gamma ]F(a[\gamma ])=(Fa)[F\gamma ].$$

$$\mathrm{Tm}(\gamma )=\_[\gamma ]:\mathrm{Tm}(m)\to \mathrm{Tm}(n).$$

$${\mathrm{p}}_n:s(n)\to n{\mathrm{q}}_n\in \mathrm{Tm}(s(n))$$

$${\mathrm{p}}_n\circ ⟨\gamma ,a⟩=\gamma {\mathrm{q}}_n[⟨\gamma ,a⟩]=a.$$

$$\mathcal{C}(-,n)\times \mathrm{Tm}(-):{\mathcal{C}}^{\mathrm{op}}\to \mathrm{Set}$$

$$\gamma =⟨⟨\dots ⟨⟨⟩,a_1⟩,\dots ⟩,a_n⟩:\underline{m}\to \underline{n}$$

$${\pi }_i^m={\mathrm{q}}_{i-1}[{\mathrm{p}}_i]\cdots [{\mathrm{p}}_{m-1}]\in \mathrm{Tm}(m)$$

$${\pi }_i^m[⟨a_1,\dots ,a_m⟩]=a_i$$

$$\mathcal{C}(\underline{m},\underline{n})\cong \mathrm{Tm}(\underline{m}{)}^n$$

$$L:\mathcal{N}\to \mathcal{C},$$

$${\lambda }_n$$

$${\mathrm{ap}}_n$$

$$\begin{array}[]{rclcl}\lambda_{n}(b)[\gamma]&=&\lambda_{m}(b[\langle\gamma\circ\mathrm{p}_{m},\mathrm{q}_{m}\rangle])\\ \mathrm{ap}_{n}(c,a)[\gamma]&=&\mathrm{ap}_{m}(c[\gamma],a[\gamma])\\ \mathrm{ap}_{n}(\lambda_{n}(b),a)&=&b[\langle\mathrm{id}_{n},a\rangle]&&(\beta)\\ \lambda_{n}(\mathrm{ap}_{s(n)}(c[\mathrm{p}_{n}],\mathrm{q}_{n}))&=&c&&(\eta)\end{array}$$

$$\mathrm{Tm}(\mathrm{s}(-))\stackrel{\lambda }{\cong }\mathrm{Tm}(-)$$

$${\lambda }_0$$

$${\mathrm{ap}}_0$$

$${\lambda }_n(b)(\gamma )$$

$${\mathrm{ap}}_n(c,a)(\gamma )$$

$${\mathrm{var}}_n(i)$$

Full text

1 Introduction

An important part of categorical logic is to establish correspondences between languages (from logic) and categorical models. For example, in their book Introduction to higher order categorical logic LS86 Lambek and Scott prove equivalences between typed lambda calculi and cartesian closed categories, between untyped lambda calculi and C-monoids, and between intuitionistic type theories and toposes. Lambek and Scott’s intuitionistic type theories are intuitionistic versions of Church’s simple theory of types, which should not be confused with Martin-Löf’s intuitionistic type theories. Interestingly, in the preface of their book (LS86, p viii) Lambek and Scott express a desire to include a result concerning the latter too:

We also claim that intuitionistic type theories and toposes are closely related, in as much as there is a pair of adjoint functors between their respective categories. This is worked out out in Part II. The relationship between Martin-Löf type theories and locally cartesian closed categories was established too recently (by Robert Seely) to be treated here.

Seely’s seminal paper SeelyRAG:locccc claims to prove that a category of Martin-Löf type theories is equivalent to a category of locally cartesian closed categories (lcccs). However, his result relies on an interpretation of substitution as pullback, and the latter are only defined up to isomorphism. It is not clear how to choose pullbacks in such a way that the strict laws for substitution are satisfied. This coherence problem is identified and solved by Curien curien:fi and Hofmann hofmann:csl who provide alternative methods for interpreting Martin-Löf type theory in lcccs (see also CurienGH14). By using Hofmann’s interpretation Clairambault and Dybjer ClairambaultD11; ClairambaultD14 show that there is an actual biequivalence of 2-categories.

In this paper we ask ourselves what it would take to add the missing chapter on Martin-Löf type theory and its correspondence with lcccs to the book by Lambek and Scott.

First we would need to add some material to Part 0 in the book on “Introduction to category theory”, including introductions to lcccs, 2-categories, bicategories, pseudofunctors, and biequivalences. But more profoundly, our biequivalence theorem differs from Lambek and Scott’s (and Seely’s) equivalence theorems in important respects, since we replace Seely’s category of Martin-Löf theories by a 2-category of categories with families (cwfs), with extra structure for type formers $\mathrm{I}_{\mathrm{ext}},\Sigma,\Pi$, and pseudo cwf-morphisms which preserve the structure up to isomorphism. Thus cwfs with extra structure replace Martin-Löf theories on the “syntactic” side of the biequivalence.

This style of presenting the correspondence between “syntax” and “semantics” for Martin-Löf’s dependent type theory applies equally well to the simply typed lambda calculus and the untyped lambda calculus, provided we consider subcategories of simply typed cwfs (scwfs), where types do not depend on variables, and of unityped cwfs (ucwfs), where there is only one type. As for full cwfs we need to provide extra structure for modelling $\lambda$-abstraction and application in the untyped $\lambda$-calculus and for modelling type formers in the simply typed $\lambda$-calculus.

This suggests that we ought to rewrite Lambek and Scott’s Part I “Cartesian closed categories and $\lambda$-calculus” in a way which harmonizes with our presentation of the biequivalence between Martin-Löf type theory and lcccs.

Categories wifh families (cwfs) model the most basic rules of dependent type theory, those which deal with substitution, context formation, assumption, and general reasoning about equality. A key feature of cwfs is that the definition can be unfolded to yield a generalized algebraic theory in Cartmell’s sense cartmell:apal. As such it suggests a language of cwf-combinators which can be used for the construction of initial cwfs (with extra structure for modelling type formers).

We prove several correspondence theorems between “syntax” in the guise of a number of cwf-based notions and “semantics” in the guise of some basic notions from category theory. Some of our theorems require “contextuality”, a notion introduced by Cartmell cartmell:apal for his contextual categories. Others require “democracy”, a notion introduced by Clairambault and Dybjer for their biequivalence theorems. Moreover, our equivalence theorems require strict preservation of chosen cwf-structure, while our biequivalence theorems only require preservation of cwf-structure up to isomorphism. In this way we can relate a number of notions from categorical logic such as cartesian operads, Lawvere’s algebraic theories, Obtułowicz’ algebraic theories of type $\lambda$-$\beta\eta$ Obtulowicz77, categories with finite products and limits, cccs, and lcccs, to the corresponding cwf-based notions. In addition to this we discuss different constructions of initial ucwfs, scwfs and cwfs (with extra structure) with and without explicit substitutions.

The purpose of our work is not so much to prove new results, but to suggest a new way to organize basic correspondence theorems in categorical logic, where the ucwf-scwf-cwf-sequence provides a smooth progression of the categorical model theory of untyped, simply typed, and dependently typed $\lambda$-calculi. We will also highlight some of the subtleties which arise when relating syntactic and semantic notions. Another important feature is that the correspondences between logical theories and categorical notions are now split into two phases: (i) equivalences and biequivalences between cwf-based notions and basic categorical notions, and (ii) the constructions of initial cwf-based notions. This yields an “abstract syntax” perspective of formal systems, where specific formalisms for untyped, simply typed and dependently typed $\lambda$-calculi are instances of the respective isomorphism classes of initial cwf-based notions. This is particularly important for dependent types and Martin-Löf type theory, since different authors make different choices in the exact formulation of the syntax and inference rules. Being initial in the appropriate category of cwfs is a suitable correctness criterion for these formulations.

In the text we have only discussed the relationship to some of the most important related notions in the literature. We would like to emphasise that we have not at all tried to give a comprehensive account of related work. Such an account would be a daunting task, since we would need to cover a multitude of works on models of the untyped and simply typed lambda calculus and of dependent type theory. Nevertheless, we would like to refer to Jacobs’ book Categorical Logic and Type Theory jacobs1999categorical which provides a comprehensive account of categorical type theory as fibred category theory. In particular, Chapter 2 on Simple Type Theory and Chapter 10 on First Order Dependent Type Theory contain much related material. In Jacobs’ work the notion of fibration takes centre stage while its role is only implicit in our cwf-based approach. In any cwf we can define an indexed category (and hence a fibration) of types indexed by contexts. However, an account of the precise correspondence between the two approaches is outside the scope of this paper.

Plan of the paper

In Section 2 we introduce cwfs and explain their connection to Martin-Löf type theory. We also define contextual and democratic cwfs. In Section 3 we consider unityped cwfs and show that contextual ucwfs are equivalent both to cartesian operads and to Lawvere theories. We then add extra structure to model the untyped $\lambda\beta\eta$-calculus, and show how initial ucwfs can be built both as calculi of explicit and implicit substitutions. In Section 4 we consider simply typed cwfs. We first show the equivalence between contextual scwfs with finite product types and categories with finite products as structure. Then we show the biequivalence between democratic scwfs and categories with finite products as property. Moreover, we add function types to our contextual scwfs with finite product types and show their equivalence to cartesian closed categories as structure. This is our analogue of the equivalence between simply typed $\lambda$-calculi and cartesian closed categories in Lambek and Scott. In Section 5 we discuss alternative definitions of full dependently typed cwfs. We also show an explicit construction of a free cwf. Moreover, we present two biequivalences. The first is between categories with finite limits and democratic cwfs with extensional identity types and $\Sigma$-types. The other is between lcccs and democratic cwfs with extensional identity types, $\Sigma$-types and $\Pi$-types. Finally, we outline the construction of a free lccc, and show how we can use our biequivalence theorem to prove that equality in this lccc is undecidable. In this section we only give an overview of the theorems and refer the reader to the journal articles ClairambaultD14; castellan:lmcs for detailed proofs.

2 Dependent type theory and categories with families

We recall the general structure of judgments and inference rules of Martin-Löf type theory and explain its connection to the definition of cwfs.

2.1 Martin-Löf type theory

We here consider Martin-Löf type theory with extensional identity types in the style of martinlof:hannover; martinlof:padova.

Judgments

In Martin-Löf martinlof:hannover intuitionistic type theory is presented as a formal system with four forms of judgment:

[TABLE]

These respectively state that $A$ is a well-formed type; that $A$ and $A^{\prime}$ are equal types; that $a$ is a valid term of type $A$; and that $a$ and $a^{\prime}$ are equal terms of type $A$. These four forms of judgments are hypothetical, that is, relative to a context $\Gamma=x_{1}:A_{1},\ldots,x_{n}:A_{n}$ which assigns types $A_{i}$ to free variables $x_{i}$.

Martin-Löf martinlof:gbg92 presents an alternative version of the theory in the form of a substitution calculus (see also tasistro:lic) with four additional forms of judgment:

[TABLE]

One aim is to make the rules for context formation explicit. Another is to formulate a calculus where substitution is a first-class citizen (a term constructor) and not just an operation defined by induction on the types and terms of the theory. Given $\Gamma=x_{1}:A_{1},\dots,x_{n}:A_{n}$, the judgment $\Delta\to\gamma:\Gamma$ expresses that $\gamma$ is a substitution (an assignment) of terms for free variables $x_{1}=a_{1},\ldots,x_{n}=a_{n}$, where $a_{1}:A_{1},\ldots,a_{n}:A_{n}$ are terms in context $\Delta$. Substitutions can be applied to both terms and types, e.g., if $\Delta\to\gamma:\Gamma$ and $\Gamma\vdash A\ \mathtt{type}$ and $\Gamma\vdash a:A$, then $\Delta\vdash A[\gamma]\ \mathtt{type}$ and $\Delta\vdash a[\gamma]:A[\gamma]$. But rather than defining $a[\gamma]$ and $A[\gamma]$ (which simultaneously substitute terms for free variables) by induction, they are instead explicit term constructors, and the effect of replacing a variable $x_{i}$ by a term $a_{i}$ is expressed a posteriori via judgmental equality.

Inference rules

The inference rules of intuitionistic type theory can be separated into two kinds. The first kind are the general rules, the most basic rules for reasoning with dependent types. They deal with substitution, context formation, assumption, and general equality reasoning. They form the backbone of the dependently typed structure, and carry no information yet about specific term and type formers. The second kind consists of the rules for type formers, such as $\Pi,\Sigma,$ and identity types. These rules are divided into formation, introduction, elimination, and equality rules (also called computation rules).

Categories with families capture models of the first kind of rules: the backbone of Martin-Löf type theory which is independent of type and term constructors.

2.2 Categories with families

We first give the definition and then explain the connection to type theory.

Definition

The definition uses the category $\mathrm{Fam}$ of families of sets. Its objects are families $(U_{x})_{x\in X}$. A morphism with source $(U_{x})_{x\in X}$ and target $(V_{y})_{y\in Y}$ is a pair consisting of a reindexing function $f:X\to Y$, and a family $(g_{x})_{x\in X}$ where for each $x\in X$, $g_{x}:U_{x}\to V_{f(x)}$ is a function.

Definition 1

A category with families (cwf) consists of the following:

• •

A category ${\cal C}$ with a terminal object $1$.

Notation and terminology. We use $\Gamma,\Delta,$ etc, to range over objects of ${\cal C}$, and refer to those as contexts. Likewise, we use $\delta,\gamma,$ etc, to range over morphisms, and refer to those as substitutions. We refer to $1$ as the empty context. We write $\langle\rangle_{\Gamma}\in{\cal C}(\Gamma,1)$ for the terminal map, representing the empty substitution.

• •

A $\mathrm{Fam}$-valued presheaf, i.e. a functor $T:{\cal C}^{\mathrm{op}}\to\mathrm{Fam}$.

Notation and terminology. If $T(\Gamma)=(U_{x})_{x\in X}$, we write $X=\mathrm{Ty}(\Gamma)$ and refer to its elements as types in context $\Gamma$ – we use $A,B,C$ to range over such types. For $A\in X=\mathrm{Ty}(\Gamma)$, we write $U_{A}=\mathrm{Tm}(\Gamma,A)$ and refer to its elements as terms of type $A$ in context $\Gamma$. Finally, for $\gamma:\Delta\to\Gamma$, the functorial action yields

[TABLE]

consisting of a pair of a reindexing function $\_\,[\gamma]:\mathrm{Ty}(\Gamma)\to\mathrm{Ty}(\Delta)$ referred to as substitution in types, and for each $A\in\mathrm{Ty}(\Gamma)$ a function $\_\,[\gamma]:\mathrm{Tm}(\Gamma,A)\to\mathrm{Tm}(\Delta,A[\gamma])$ referred to as substitution in terms.

• •

A context comprehension operation which to a given context $\Gamma\in{\cal C}_{0}$ and type $A\in\mathrm{Ty}(\Gamma)$ assigns a context $\Gamma\cdot A$ and two projections

[TABLE]

satisfying the following universal property: for all $\gamma:\Delta\to\Gamma$, for all $a\in\mathrm{Tm}(\Delta,A[\gamma])$, there is a unique $\langle\gamma,a\rangle:\Delta\to\Gamma\cdot A$ such that

[TABLE]

We say that $(\Gamma\cdot A,\mathrm{p}_{\Gamma,A},\mathrm{q}_{\Gamma,A})$ is a context comprehension of $\Gamma$ and $A$.

Observe the similarity between the universal properties of context comprehension and cartesian products – the former is a skewed dependently typed version of the latter. It is also closely related to Lawvere comprehension lawvere:hyperdoctrines.

This definition is the standard, historical definition of cwfs dybjer:torino. As notations and terminology suggest, it is closely connected to the syntax of type theory, and particularly to Martin-Löf’s substitution calculus.

Remark 1

The structure from Definition 1 exactly matches that of Martin-Löf’s substitution calculus mentioned before. The correspondence follows:

• •

$\Gamma\in{\cal C}_{0}$ models the judgment $\Gamma\ \mathtt{context}$ and $\Gamma=\Gamma^{\prime}\in{\cal C}_{0}$ models $\Gamma=\Gamma^{\prime}$.

• •

$\gamma\in{\cal C}(\Delta,\Gamma)$ models the judgment $\Delta\to\gamma:\Gamma$ and $\gamma=\gamma^{\prime}\in{\cal C}(\Delta,\Gamma)$ models $\Delta\to\gamma=\gamma^{\prime}:\Gamma$.

• •

$A\in\mathrm{Ty}(\Gamma)$ models the judgment $\Gamma\vdash A\ \mathtt{type}$ and $A=A^{\prime}\in\mathrm{Ty}(\Gamma)$ models $\Gamma\vdash A=A^{\prime}$.

• •

$a\in\mathrm{Tm}(\Gamma,A)$ models the judgment $\Gamma\vdash a:A$ and $a=a^{\prime}\in\mathrm{Tm}(\Gamma,A)$ models $\Gamma\vdash a=a^{\prime}:A$.

The connection with Martin-Löf’s substitution calculus contributes to the appeal of cwfs: they give rise to categorical combinators for dependent types just as cccs give rise to categorical combinators for the simply typed $\lambda$-calculus Curien86. However, Definition 1 has sometimes been criticized for being too close to the syntax, or for relying on less standard mathematical objects such as $\mathrm{Fam}$-valued presheaves. In Section 5.1 we will discuss alternative formulations of cwfs highlighting other aspects of the structure.

Remark 2

A key feature of the notion of cwf is that it can be presented as a generalized algebraic theory in the sense of Cartmell cartmell:apal.

• •

The generalized algebraic theory of categories introduces the sorts ${\cal C}_{0}$ and ${\cal C}(\Delta,\Gamma)$, the operations $\gamma\circ\delta$ and $\mathrm{id}_{\Gamma}$, and associativity and identity laws.

• •

The $\mathrm{Fam}$-valued presheaf adds the sorts $\mathrm{Ty}(\Gamma)$ and $\mathrm{Tm}(\Gamma,A)$, the operations $A[\gamma]$ and $a[\gamma]$, and associativity and identity laws for both.

• •

The terminal object adds the operation 1 and $\langle\rangle$, and its uniqueness law.

• •

Context comprehension adds the operations $\Gamma\cdot A,\mathrm{p}_{\Gamma,A},\mathrm{q}_{\Gamma,A}$, and $\langle\gamma,a\rangle$, and the projection and surjective pairing laws.

See dybjer:torino for a complete presentation of the generalized algebraic theory of cwfs. We remark that we have suppressed some of the arguments of the operations. For example, composition is officially an operation with five arguments: $\Xi,\Delta,\Gamma\in{\cal C}_{0},\delta\in{\cal C}(\Xi,\Delta)$, and $\gamma\in{\cal C}(\Delta,\Gamma)$, but we suppress the three first when we write $\delta\circ\gamma$. Similar remarks hold for the operations $A[\gamma],a[\gamma],\langle\rangle$, and $\langle\gamma,a\rangle$. We sometimes drop even more arguments to simplify notation and for example write $\mathrm{p}_{A}$ or $\mathrm{p}$ for the official $\mathrm{p}_{\Gamma,A}$, etc. Moreover, we sometimes write $\gamma:\Delta\to\Gamma$ for $\gamma\in{\cal C}(\Delta,\Gamma)$.

A cwf is thus a structure $({\cal C},T,1,\langle\rangle,\cdot,\mathrm{p},\mathrm{q},\langle-,-\rangle)$, subject to some equations. However, we often refer to a cwf by the first two components $({\cal C},T)$ or even the first component ${\cal C}$.

As already mentioned, cwfs only organize the core of dependent type theory, the basic structure and operations on contexts, types, terms, and substitutions. We will see later how cwfs naturally generalize well-known notions in categorical logic to dependent types. We will also see how they may be enriched with type and term formers, in order to capture Martin-Löf type theory with $\Sigma$-types, $\Pi$-types and identity types. Finally, we will see that the syntax of Martin-Löf type theory may be defined as the initial cwf in a precise sense.

Structure of contexts

The definition of cwfs just contains two operations on contexts: the terminal object representing the empty context and an operation mapping a context $\Gamma$ and a type $A\in\mathrm{Ty}(\Gamma)$ to a new context $\Gamma\cdot A$. It is however not required that all contexts are generated by repeated application of these two rules. In contrast to this, Cartmell cartmell:apal adds such a constraint on the structure of context for his contextual categories. We shall use the following formulation, which is equivalent to Cartmell’s:

Definition 2 (Contextuality)

A cwf is contextual iff there is

[TABLE]

a length function, such that $l(\Gamma)=0$ iff $\Gamma=1$, and $l(\Gamma)=n+1$ iff there are unique $\Delta\in{\cal C}_{0}$ and $A\in\mathrm{Ty}(\Delta)$ such that $\Gamma=\Delta\cdot A$, and $l(\Delta)=n$.

Although this requirement will be used in some of our equivalence theorems, it is not part of our definition of cwf. The reason is that unlike the other parts of the definition of cwfs, it does not correspond to an inference rule of dependent type theory, and it is not expressed in the language of generalized algebraic theories. However, the free cwf is contextual.

Without going as far as requiring all contexts to be defined inductively, we sometimes wish to overcome the intrinsic distinction between contexts and types by asking that up to isomorphism, every context is represented by a type ClairambaultD11; ClairambaultD14.

Definition 3 (Democracy)

A cwf is democratic provided each context $\Gamma$ is represented by a type $\overline{\Gamma}$ in the sense that there is an isomorphism

[TABLE]

Democracy does not imply contextuality. However, in the presence of unit types and $\Sigma$-types, the converse holds: any context $1\cdot A_{1}\cdot\ldots\cdot A_{n}$ may be represented by the iterated $\Sigma$-type $\Sigma(A_{1},\Sigma(A_{2},\dots,\Sigma(A_{n-1},A_{n})\cdots))\in\mathrm{Ty}(1)$. Like contextuality, democracy does not correspond to an inference rule of dependent type theory. However, unlike contextuality, democracy can be expressed in the language of generalized algebraic theories.

Strict morphisms of cwfs

We will now introduce a notion of morphisms between cwfs.

Definition 4

A (strict) cwf-morphism between cwfs $({\cal C},T_{\cal C})$ and $({\cal D},T_{\cal D})$ is a pair $(F,\sigma)$ where $F:{\cal C}\to{\cal D}$ is a functor preserving $1$ on the nose, and

[TABLE]

is a natural transformation between $\mathrm{Fam}$-valued presheaves, preserving context comprehension on the nose.

Thus we have

[TABLE]

[TABLE]

for $\Gamma\in{\cal C}_{0}$ and $A\in\mathrm{Ty}(\Gamma)$.

It is convenient to simplify notations and write all the components of a cwf-morphism as $F$ so that we write $F(A)$ for $\sigma_{\Gamma}(A)$ and $F(a)$ for $\sigma^{A}_{\Gamma}(a)$. Naturality of $\sigma$ amounts to preservation of substitution, i.e., for all $\gamma:\Delta\to\Gamma$ in ${\cal C}$, we have

[TABLE]

Finally, preservation of context comprehension on the nose means that $F(\Gamma\cdot A)=F\Gamma\cdot FA$, with $F(\mathrm{p}_{\Gamma,A})=\mathrm{p}_{F\Gamma,FA}$ and $F(\mathrm{q}_{\Gamma,A})=\mathrm{q}_{F\Gamma,FA}$.

Small cwfs and strict cwfs-morphisms form a category, written $\mathbf{Cwf}$.

3 Unityped cwfs

As we explained in the introduction, a key feature of the notion of cwf is that it can be presented as a generalized algebraic theory. As a consequence it can be seen both as a notion of model and as an (idealized) language for dependent type theory. It is therefore a suitable intermediary between traditional formal systems for dependent type theory and categorical notions of models. This paper is based on the observation that restricted classes of cwfs can play a similar role for untyped and simply typed systems.

In this section we will look at cwfs with only one type and claim that they play a similar role for untyped systems as cwfs do for dependently typed systems.

3.1 Plain ucwfs

The definition of cwfs with only one type can be simplified as follows.

Definition 5

A unityped category with families (ucwf) consists of the following:

• •

A category ${\cal C}$ with a terminal object, written [math].

Notation and terminology. We use $n,m,$ etc to range over objects of ${\cal C}$, and refer to those as contexts. Likewise, we use $\delta,\gamma,$ etc to range over morphisms, and refer to those as substitutions. We refer to [math] as the empty context. We write $\langle\rangle_{n}\in{\cal C}(n,0)$ for the terminal morphism, representing the empty substitution.

• •

A presheaf $\mathrm{Tm}:{\cal C}^{\mathrm{op}}\to\mathrm{Set}$.

Notation and terminlogy. We refer to the elements of $\mathrm{Tm}(n)$ as the terms of arity $n$ – we use $a,b,$ etc to range over terms. Finally, for $\gamma:n\to m$, the functorial action of $\mathrm{Tm}$ yields a substitution operation

[TABLE]

• •

A context comprehension operation which to a given context $n\in{\cal C}_{0}$ assigns a context $s(n)\in{\cal C}_{0}$ along with two projections

[TABLE]

satisfying the following universal property: for all $\gamma:m\to n$, for all $a\in\mathrm{Tm}(m)$, there is a unique $\langle\gamma,a\rangle:m\to s(n)$ such that

[TABLE]

Remark 3

The context comprehension operation for ucwfs amounts to the assignment of a representation $s(n)$ of the presheaf

[TABLE]

for all $n\in{\cal C}_{0}$.

If $n\in\mathbb{N}$ is a natural number, we write $\underline{n}=s^{n}(0)$ for the context obtained by $n$ applications of the context comprehension operation. If the ucwf is contextual, all objects of ${\cal C}$ have the form $\underline{n}$ for $n\in\mathbb{N}$. We think of the terms in $\mathrm{Tm}(\underline{n})$ as boxes with $n$ inputs and one output. Substitutions $\gamma:\underline{m}\to\underline{n}$ are boxes with $m$ inputs and $n$ outputs. We have

[TABLE]

for $a_{1},\ldots,a_{n}\in\mathrm{Tm}(\underline{m})$. For convenience we write $\gamma=\langle a_{1},\dots,a_{n}\rangle$. For $a\in\mathrm{Tm}(\underline{m})$, performing the substitution $a[\gamma]$ amounts to connecting the box $a_{i}$ to the $i$-th input of the box $a$, see Figure 1.

Figure 1 reminds us of other categorical notions that aim to capture algebraic theories, such as Lawvere theories. We will come back later to this similarity. However, Figure 1 is misleading in one respect: it suggests that the boxes $a_{1},\dots,a_{n}$ have free variables in $\mathrm{Var}(m)=\{1,\dots,m\}$. In reality, in the context of ucwfs, these free variables are not first-class citizens but are obtained indirectly through sequences of projections. More precisely, the term

[TABLE]

will serve in place of the free variable $i$ in the context of size $m$. With the notations introduced, we then have the expected equation

[TABLE]

These notations suggest a correspondence to cartesian operads trimble:nlab, and we will come back to this connection. Before that, writing $\mathbf{Ucwf}$ for the category of small ucwfs and strict cwf-morphisms, we note:

Proposition 1

The category $\mathbf{Ucwf}$ has an initial object.

Construction 1. From the definition of ucwf it is immediately clear that an initial ucwf ${\cal T}_{\mathrm{ucwf}}$ can be generated inductively: we simultaneously define the three families ${\cal C}_{0},{\cal C}(n,m)$, and $\mathrm{Tm}(n)$ where the ucwf-operations become introduction rules. Then we take the quotients with respect to the equivalence relations generated by the ucwf-equations.

Construction 2. Alternatively, we can construct it as the presheaf of variables over the category of renamings.

• •

The category ${\cal N}$ of renamings, with objects ${\cal N}_{0}=\mathbb{N}$ and ${\cal N}(n,m)=\mathrm{Var}(n)^{m}$.

• •

The presheaf $\mathrm{Tm}:{\cal N}^{\mathrm{op}}\to\mathrm{Set}$ is defined by $\mathrm{Tm}(n)=\mathrm{Var}(n)$ and $i[(a_{1},\ldots,a_{m})]=a_{i}$.

• •

Context comprehension is defined by $s(n)=n+1$, $\mathrm{p}_{n}=(1,\dots,n)$, and $\mathrm{q}_{n}=n+1$.

This construction and its isomorphism with ${\cal T}_{\mathrm{ucwf}}$ have been formalized in Agda by Brilakis Brilakis18.

Interestingly, this is the same as the free cartesian operad. This initial ucwf is contextual. As we will see, this requirement is necessary for the connection with cartesian operads.

3.2 Contextual ucwfs

Cartesian operads

Let us now consider the special case of a contextual ucwf ${\cal C}$, where the length function induces a bijection ${\cal C}_{0}\cong\mathbb{N}$. It follows from the laws of cwfs that

[TABLE]

From right to left we use the $n$-ary tupling introduced above, while from left-to-right we apply projections. This is essentially the same data as for cartesian operads.

Definition 6

A cartesian operad consists of the following:

• •

a family $\mathrm{Tm}(n)$, where $n\in\mathbb{N}$, of n-ary operations;

• •

an operation of operad composition which maps $a\in\mathrm{Tm}(m)$ and $\gamma\in\mathrm{Tm}(n)^{m}$ to $a[\gamma]\in\mathrm{Tm}(n)$ and satisfies identity and associativity laws;

• •

projections $\pi^{n}_{i}\in\mathrm{Tm}(n)$, such that $\pi_{i}^{n}[(a_{1},\ldots,a_{n})]=a_{i}\,.$

Focusing on contextual ucwfs allows us to extract the mechanism for terms and substitutions that is at play in full cwfs, but without considering types.

Writing $\mathbf{Ucwf}_{\mathrm{ctx}}$ of $\mathbf{Ucwf}$ having as objects contextual ucwfs, and $\mathbf{Cop}$ for the category of cartesian operads, we have:

Theorem 3.1

The categories $\mathbf{Ucwf}_{\mathrm{ctx}}$ and $\mathbf{Cop}$ are equivalent.

Rather than formally define $\mathbf{Cop}$ and prove this equivalence, we shall detail it for Lawvere theories, which form a category equivalent to $\mathbf{Cop}$ trimble:nlab.

Lawvere theories

Contextual ucwfs are also equivalent to Lawvere theories. The following definition is from HylandP07.

Definition 7

A Lawvere theory consists of a small category ${\cal C}$ with (necessarily strictly associative) finite products and a strict finite-product preserving identity-on-objects functor $L:{\cal N}\to{\cal C}$. Here, ${\cal N}$ refers to the category of renamings introduced in the proof of Proposition 1, with terminal object [math] and binary products defined by $+$.

A map of Lawvere theories from $(L,{\cal C})$ to $(L^{\prime},{\cal C}^{\prime})$ is a (necessarily strict) finite-product preserving functor from ${\cal C}$ to ${\cal C}^{\prime}$ that commutes with the functors $L$ and $L^{\prime}$. Lawvere theories and their maps form a category $\mathbf{Law}$.

Note that $L:{\cal N}\to{\cal C}$ is usually (equivalently) presented as ${\cal N}^{\mathbf{op}}_{0}\to{\cal C}$, where ${\cal N}_{0}$, a skeleton of the category of finite sets and functions, has an initial object [math] and finite coproducts given by the sum of integers.

Theorem 3.2

The categories $\mathbf{Ucwf}_{\mathrm{ctx}}$ and $\mathbf{Law}$ are equivalent.

Proof

Let $({\cal C},T_{\cal C})$ be a contextual ucwf. We already noted that ${\cal C}_{0}\cong\mathbb{N}$. Moreover, we observe that there is a unique contextual ucwf $({\cal D},T_{\cal D})$, isomorphic to $({\cal C},T_{\cal C})$ and such that ${\cal D}_{0}=\mathbb{N}$ with [math] terminal and $s(n)=n+1$ for all $n\in{\cal D}_{0}$. Hence we assume from now on that contextual ucwfs have natural numbers as objects. By Proposition 1 below, ${\cal N}$ is the base category of the initial ucwf. Hence, if $({\cal C},T_{\cal C})$ is a contextual ucwf, there is a unique functor

[TABLE]

which is the first component of a cwf-morphism. In particular, $L$ preserves the terminal object and context comprehension on the nose. It follows that it is identity-on-objects and strictly finite-product preserving.

If $(F,\sigma)$ is a cwf-functor between contextual ucwfs (assuming w.l.o.g. that these ucwfs have $\mathbb{N}$ as objects), it follows that $F$ is a morphism between the corresponding Lawvere theories. Conversely, for any morphism $F$ between the corresponding Lawvere theories, $\sigma$ can be uniquely recovered from $F$ and projection. This yields a full and faithful functor from $\mathbf{Ucwf}_{\mathrm{ctx}}$ to $\mathbf{Law}$.

Finally this functor is surjective on objects: from $(L,{\cal C})$ a Lawvere theory, there is a ucwf with category ${\cal C}$; terms $\mathrm{Tm}(n)={\cal C}(n,1)$, and context comprehension $s(n)=n+1$. The universal property follows from that of the finite product. From all that, it follows that $\mathbf{Ucwf}_{\mathrm{ctx}}$ and $\mathbf{Law}$ are equivalent.

Remark 4

In a recent paper Fiore and Voevodsky VoevodskyF17 prove a closely related result about C-systems, a variant of Cartmell’s contextual categories. They prove that their category of Lawvere theories is isomorphic to the subcategory of C-systems whose length functions (in the definition of contextuality) are bijections.

3.3 $\lambda\beta\eta$-ucwfs

Ucwfs give rise to a generalized algebraic theory which captures the combinatorics of terms and substitution in a similar way as cartesian operads and Lawvere theories. This primitive structure may then be enriched with operations and equations for capturing specific theories, such as the pure $\lambda\beta\eta$-calculus.

Definition 8

A $\lambda\beta\eta$-ucwf is a ucwf $({\cal C},\mathrm{Tm})$ with two more operations:

[TABLE]

for all $n\in{\cal C}_{0}$, and four more equations:

[TABLE]

for $\gamma:m\to n$, $b\in\mathrm{Tm}(s(n))$, and $c,a\in\mathrm{Tm}(n)$. A $\lambda\beta$-ucwf has the same operations, but it not subject to the $(\eta)$ equation.

The definition above is natural and close to the syntax. As we will see later on, it is the direct simplification of the notions of arrow and $\Pi$-types in the simply-typed and the dependently typed case discussed later on. However, in the unityped case, this definition can be simplified dramatically.

Proposition 2

Let $({\cal C},\mathrm{Tm})$ be a ucwf. Then, $\lambda\beta\eta$-structures on ${\cal C}$ are equivalently defined as natural isomorphisms between presheaves

[TABLE]

where the functorial action of $\mathrm{s}$ is defined as $\mathrm{s}(\gamma)=\langle\gamma\circ\mathrm{p}_{m},\mathrm{q}_{m}\rangle$. More precisely, (1) for any $\lambda\beta\eta$-structure $\lambda$ is such a natural isomorphism, and (2) given such a natural isomorphism, there is a unique $\lambda\beta\eta$-structure giving rise to it.

Proof

For (1), given a $\lambda\beta\eta$-structure on $({\cal C},\mathrm{Tm})$, we first observe that $\lambda_{n}$ is natural by the substitution law. For $c\in\mathrm{Tm}(n)$ we set $\lambda_{n}^{-1}(c)=\mathrm{ap}_{\mathrm{s}(n)}(c[\mathrm{p}_{n}],\mathrm{q}_{n})\in\mathrm{Tm}(\mathrm{s}(n))$ – using $\beta,\eta$ and the substitution law for $\lambda$, $\lambda_{n}$ and $\lambda_{n}^{-1}$ are inverse.

For (2), given a natural iso $\lambda_{n}$, we set $\mathrm{ap}_{n}(c,a)=\lambda_{n}^{-1}(c)[\langle\mathrm{id}_{n},a\rangle]$. The $\beta$-rule follows from the fact that $\lambda_{n}^{-1}\circ\lambda_{n}$ is the identity. The $\eta$-rule follows from the naturality of $\lambda^{-1}$ plus the fact that $\lambda_{n}\circ\lambda_{n}^{-1}$ is the identity. The substitution law for $\lambda$ is by naturality of $\lambda$, and the substitution law for $\mathrm{ap}$ is by naturality of $\lambda^{-1}$. Finally, uniqueness of the $\lambda\beta\eta$-structure (i.e. of $\mathrm{ap}_{n}$) relies on the substitution rule for $\mathrm{ap}$.

Some related models of the untyped $\lambda$-calculus

There are many notions of model of $\lambda$-calculus, see for example Barendregt barendregt:lambda. We will only briefly discuss the ones given by Obtułowicz Obtulowicz77, Aczel aczel:frege, and Lambek and Scott LS86.

Obtułowicz’s algebraic theories of type $\lambda$–$\beta\eta$ are Lawvere theories similar to the Lawvere theories corresponding to contextual $\lambda\beta\eta$-ucwfs, but use an evaluation morphism $\mathrm{\varepsilon}$ as a primitive instead of $\mathrm{ap}$. These operations are interdefinable, via $\mathrm{\varepsilon}=\mathrm{ap}(\pi^{2}_{1},\pi^{2}_{2})\in\mathrm{Tm}(2)$ and $\mathrm{ap}(c,a)=\mathrm{\varepsilon}[\langle c,a\rangle]\in\mathrm{Tm}(n)$ for $c,a\in\mathrm{Tm}(n)$.

As a basis for his notion of Frege structure, Aczel introduces a notion of lambda structure. This in turn is based on the notion of an explicitly closed family, which is a cartesian operad where $\mathrm{Tm}(n)\subseteq\mathrm{Tm}(0)^{n}\to\mathrm{Tm}(0)$, so that $a[\gamma]$ is function composition, and projections are the projections in the metalanguage. It is thus a cartesian operad which is well-pointed in the sense that $a,a^{\prime}\in\mathrm{Tm}(n)$ and $a[\gamma]=a^{\prime}[\gamma]$ for all $\gamma\in{\cal C}(0,n)$ implies $a=a^{\prime}$. To model the $\lambda\beta$-calculus Aczel adds two operations

[TABLE]

The resulting notion of lambda structure is equivalent to well-pointed $\lambda\beta$-ucwfs. Since terms are functions, there is a unique way to define the operations $\lambda_{n}$ and $\mathrm{ap}_{n}$ for $n>0$ so that they satisfy the substitution laws of $\lambda\beta$-ucwfs:

[TABLE]

for $\gamma\in{\cal C}(0,n)$. The general substitution rules follow from this definition.

Lambek and Scott propose C-monoids as their notion of model of the untyped $\lambda$-calculus. These are monoids with extra structure coming from combinators of cartesian closed categories. C-monoids capture the equational behaviour of closed rather than open terms. Like in $\lambda\beta\eta$-ucwfs and cartesian closed categories, variables are dealt with indirectly as projections. But in $\lambda\beta\eta$-ucwfs, variable addressing is external, that is, handled by the ucwf structure. There are no term constructors for pairs and projections – in particular closed terms, i.e., terms in $\mathrm{Tm}(0)$, do not form a C-monoid as they support no pairing and projection operations. In contrast, C-monoids handle variable addressing through pairs and projections at the term level.

We expect a strong relationship between C-monoids and $\lambda\beta\eta$-ucwfs with term-level pairs and projections. The proof should follow LS86, encoding open terms and substitution within C-monoids via functional completeness.

Initial $\lambda\beta\eta$-ucwfs

To conclude the discussion about $\lambda\beta\eta$-ucwfs, we include a construction of the untyped $\lambda$-calculus as the initial such structure. For that, let us say that a strict cwf-morphism $F$ between $\lambda\beta\eta$-ucwfs $({\cal C},\mathrm{Tm}_{\cal C})$ and $({\cal D},\mathrm{Tm}_{\cal D})$ is a strict $\lambda\beta\eta$-ucwf-morphism iff the action of $F$ on terms preserves all the term constructors on the nose. Let us write $\mathbf{Ucwf}^{\lambda\beta\eta}$ for the category of small $\lambda\beta\eta$-ucwfs and strict $\lambda\beta\eta$-ucwf-morphisms. Then, we have:

Proposition 3

The category $\mathbf{Ucwf}^{\lambda\beta\eta}$ has an initial object.

Construction 1. The most direct method is similar to Construction 1 of an initial ucwf. We simultaneously define the three families ${\cal C}_{0},{\cal C}(n,m)$, and $\mathrm{Tm}(n)$ where the $\lambda\beta\eta$-ucwf-operations become introduction rules. Then we take the quotients with respect to the equivalence relations generated by the $\lambda\beta\eta$-ucwf-equations. This construction can be viewed as a well-scoped variable free version of the $\lambda\sigma$-calculus of Abadi, Cardelli, Curien, and Lévy AbadiCCL90.

Construction 2. Another initial $\lambda\beta\eta$-ucwf can be constructed from the (well-scoped) $\lambda\beta\eta$-calculus. We let ${\cal C}_{0}=\mathbb{N}$ and generate the family $\mathrm{Tm}(n)$ by the following rules

[TABLE]

quotiented by the equivalence relation $\sim$ generated by $\beta$ and $\eta$:

[TABLE]

Note that the variables $\mathrm{var}_{n}(i)$ where $i\in\mathrm{Var}(n)$ were simply represented by the number $i$ in the corresponding construction in Proposition 1.

We let ${\cal C}(n,m)=\mathrm{Tm}(n)^{m}$ and define substitution by induction on $\mathrm{Tm}(n)$:

[TABLE]

for $\gamma\in{\cal C}(m,n)$.

Note that this construction is an extension of Construction 2 of an initial plain ucwf.

The two constructions, and the fact that both give rise to initial $\lambda\beta\eta$-ucwfs, have been formalised in Agda by Brilakis Brilakis18.

4 Simply-typed cwfs

En route to full cwfs, we now add types yielding simply-typed cwfs (scwfs) (called non-dependent cwfs in Clairambault and Dybjer clairambault:london). We will then study the relationship with cartesian and cartesian closed categories. (By cartesian category we here mean categories with finite products, whereas some of the literature including Johnstone johnstone2002sketches uses this term for categories with finite limits.)

4.1 Plain scwfs

A simply-typed cwf (scwf) is a cwf where the presheaf of types $\mathrm{Ty}:{\cal C}^{\mathrm{op}}\to\mathrm{Set}$ is constant, i.e. forms a set $\mathrm{Ty}$ not depending on the context and invariant under substitution. We can thus simplify the definition as follows:

Definition 9

An scwf consists of the following:

• •

A category ${\cal C}$ with a terminal object $1$.

• •

A set $\mathrm{Ty}$.

• •

A family of presheaves $\mathrm{Tm}_{A}:{\cal C}^{\mathrm{op}}\to\mathrm{Set}$ for $A\in\mathrm{Ty}$. (We also write $\mathrm{Tm}(\Gamma,A)$ for $\mathrm{Tm}_{A}(\Gamma)$.)

• •

A context comprehension operation which to $\Gamma\in{\cal C}_{0}$ and $A\in\mathrm{Ty}$ assigns a context $\Gamma\cdot A$ and two projections

[TABLE]

satisfying the following universal property: for all $\gamma:\Delta\to\Gamma$, for all $a\in\mathrm{Tm}(\Delta,A)$, there is a unique $\langle\gamma,a\rangle:\Delta\to\Gamma\cdot A$ such that

[TABLE]

We say that $(\Gamma\cdot A,\mathrm{p}_{\Gamma,A},\mathrm{q}_{\Gamma,A})$ is a context comprehension of $\Gamma$ and $A$.

Remark 5

Context comprehension for scwfs amounts to a representation $\Gamma\cdot A$ of the presheaf

[TABLE]

for all $\Gamma\in{\cal C}_{0}$ and $A\in\mathrm{Ty}$.

An scwf is a particular kind of cwf, and a (strict) scwf-morphism is simply a (strict) cwf-morphism between scwfs. Small scwfs and strict cwf-morphisms form a category $\mathbf{Scwf}$.

$\mathbf{Scwf}$ has an initial object, but it is not very interesting since its set of types is empty and its base category is restricted to the terminal object. Therefore we fix a set ${\cal B}$ of basic types and consider the category ${\cal B}$-$\mathbf{Scwf}$ where objects are small scwfs $({\cal C},\mathrm{Ty}_{\cal C},\mathrm{Tm}_{\cal C})$ together with an interpretation function $\llbracket-\rrbracket_{\cal C}:{\cal B}\to\mathrm{Ty}$. Morphisms are strict scwfs-morphisms that commute with the interpretation.

Proposition 4

For all sets ${\cal B}$ the category ${\cal B}$-$\mathbf{Scwf}$ has an initial object.

Proof

The initial ${\cal B}$-scwf, also called the free scwf over a set of types ${\cal B}$, can be constructed in much the same two ways as we constructed initial ucwfs.

We can either proceed as in Construction 1 where the operations become introduction rules for inductively generating the objects, and terms, and the equations inductively generate an equivalence relation.

Alternatively, we can proceed as in Construction 2, and construct a typed version of the category ${\cal N}$ of Proposition 1. For the second construction we let $\mathrm{Ty}={\cal B}$. Then we define

[TABLE]

where $\mathrm{Tm}(\Gamma,A)=\{\mathrm{var}_{n}(i)\mid A=A_{i}\}$ containing the $i$th variable, where $\Gamma=[A_{1},\dots,A_{n}]$. Moreover, we define the projections as

[TABLE]

and substitution

[TABLE]

Just as for ucwfs, the free scwf over a set ${\cal B}$ is contextual. In analogy with Section 3.2 we could relate scwfs to coloured cartesian operads (multicategories) and multi-sorted Lawvere theories, but we omit the unsurprising details. Instead, we discuss their relationship with cartesian categories.

4.2 Finite products as structure

Cartesian categories (categories with finite products) are categories with a terminal object and binary cartesian products. Straightforward as it seems, this definition hides some subtleties which are put to the forefront when one considers the associated notions of morphism between cartesian categories. Namely, does the mere existence of a product for any two objects suffice to obtain a cartesian category, or are the finite products part of the data of a cartesian category? Texts in category theory adopt one view or the other, not always explicitely. In Lambek and Scott’s book, the latter view is explicitely adopted; and morphisms between cartesian categories must preserve this explicit data on the nose.

Definition 10

A cartesian category (with structure) consists of the following:

• •

A category ${\cal C}$ with a terminal object $1$, where $\langle\rangle_{X}:X\to 1$ denotes the unique arrow into it.

• •

A product operation which to any $A,B\in{\cal C}_{0}$ assigns an object $A\times B\in{\cal C}_{0}$ and two projections

[TABLE]

satisfying the following universal property: for all $a:X\to A$, for all $b:X\to B$, there is a unique $\langle a,b\rangle:X\to A\times B$ such that

[TABLE]

A strict cartesian functor from cartesian category ${\cal C}$ (leaving implicit the other components) to ${\cal D}$ is a functor $F:{\cal C}\to{\cal D}$ preserving the structure on the nose, i.e. for all $A,B\in{\cal C}_{0}$, $F(A\times_{\cal C}B)=F(A)\times_{\cal D}F(B)$, and

[TABLE]

We write $\mathbf{CCs}$ for the category of small cartesian categories (with structure) and strict cartesian functors, preserving the structure on the nose.

We will later consider another notion of cartesian category, where we are content with the mere existence of a terminal object and a cartesian product for any two objects, and the only data part of the structure is the basic category ${\cal C}$ – there are no chosen products. This, of course, constrains the maps: the notion of strict cartesian morphisms as above would make no sense without chosen structure.

We observe in passing that from the preservation of projections and the universal property, it follows directly that strict cartesian functors also preserve tuples on the nose, in the sense that $F(\langle\rangle_{X})=\langle\rangle_{F(X)}$ and $F(\langle a,b\rangle)=\langle F(a),F(b)\rangle$.

Finite product types

We now wish to compare cartesian categories with structure, as above, with scwfs. They are similar, but the main difference is that scwfs distinguish contexts and types; whereas cartesian categories do not have this distinction. In particular, when constructing an scwf from a cartesian category we must recover the types as the objects of ${\cal C}$. It follows that the resulting scwfs support a finite product operation on types. Looking for an equivalence, we define what it means for an scwf to support finite product types and introduce a binary product type $A\times B$, and a unit type ${\mathbb{N}_{1}}$.

Definition 11

An ${\mathbb{N}_{1}}$-structure on an scwf ${\cal C}$ consists of a type ${\mathbb{N}_{1}}\in\mathrm{Ty}$, and for each $\Gamma$ a term ${0_{1}}\in\mathrm{Tm}_{\cal C}(\Gamma,{\mathbb{N}_{1}})$ such that for all $c\in\mathrm{Tm}(\Gamma,{\mathbb{N}_{1}})$, $0_{1}=c$.

Definition 12

A $\times$-structure on an scwf ${\cal C}$ consists of, for each $A,B\in\mathrm{Ty}$, a type $A\times B\in\mathrm{Ty}$ such that for all $\Gamma\in{\cal C}_{0}$ there are term formers

[TABLE]

such that

[TABLE]

We thus have a type formation rule for $A\times B$ and term formation rules for projections and pairs. The first three equations are the usual rules for product types with surjective pairing, while the last one states stability under substitution. By an scwf with finite product types we mean an scwf with an ${\mathbb{N}_{1}}$-structure and a $\times$-structure.

Remark 6

Having a $\times$-structure on an scwf ${\cal C}$ amounts to requiring that there is a binary type former $\times$ and a natural isomorphism of presheaves

[TABLE]

Likewise, an ${\mathbb{N}_{1}}$-structure corresponds to a type ${\mathbb{N}_{1}}$ and a natural isomorphism between $\mathrm{Tm}_{\cal C}(-,{\mathbb{N}_{1}})$ and the constant singleton presheaf.

The product type structure on scwfs should be preserved by morphisms.

Definition 13

If ${\cal C},{\cal D}$ are scwfs with finite product types, then a strict scwf-morphism $F:{\cal C}\to{\cal D}$ (strictly) preserves ${\mathbb{N}_{1}}$-structure if $F({\mathbb{N}_{1}}^{\cal C})={\mathbb{N}_{1}}^{\cal D}$, and $F(0_{1}^{\cal C})=0_{1}^{\cal D}$. Similarly, it (strictly) preserves $\times$-structure if $F(A\times^{\cal C}B)=F(A)\times^{\cal D}F(B)$, $F(\mathrm{fst}_{A,B}^{\cal C}(c))=\mathrm{fst}_{FA,FB}^{\cal D}(F(c))$ and $F(\mathrm{snd}_{A,B}^{\cal C}(c))=\mathrm{snd}_{FA,FB}^{\cal D}(F(c))$.

We write $\mathbf{Scwf}^{{\mathbb{N}_{1}},\times}$ for the category where the objects are small scwfs with product types, and morphisms are strict structure-preserving cwf-morphisms.

Given an scwf with finite product types we construct a cartesian category as follows. First, we define the category of types and terms in context.

Definition 14

Let ${\cal C}$ be an scwf with finite product types. We define the category ${\cal T}\!\mathit{y}(\Gamma)$ of types and terms in context $\Gamma\in{\cal C}_{0}$ as having: (1) as objects, $\mathrm{Ty}$; (2) as morphisms from $A\in\mathrm{Ty}$ to $B\in\mathrm{Ty}$, the terms $b\in\mathrm{Tm}(\Gamma\cdot A,B)$. If $b\in\mathrm{Tm}(\Gamma\cdot A,B)$ and $c\in\mathrm{Tm}(\Gamma\cdot B,C)$, then their composition is

[TABLE]

with identity $\mathrm{id}_{\Gamma,A}=\mathrm{q}_{\Gamma,A}\in\mathrm{Tm}(\Gamma\cdot A,A)$.

It follows that ${\cal T}\!\mathit{y}(\Gamma)$ is a cartesian category with structure for all $\Gamma\in{\cal C}_{0}$.

Lemma 1

For any $\Gamma$, we let ${\mathbb{N}_{1}}$ be the chosen terminal object in ${\cal T}\!\mathit{y}(\Gamma)$. For every $A,B\in\mathrm{Ty}$, we let their product be $A\times B\in\mathrm{Ty}$ and the projections

[TABLE]

We omit the (straightforward) proof. This entails that given an scwf with finite product types ${\cal C}$, there is a canonical cartesian category with structure, the cartesian category of closed terms ${\cal T}\!\mathit{y}_{\cal C}(1_{\cal C})$.

Proposition 5

There is a functor

[TABLE]

which to any scwf with products ${\cal C}$ associates ${\cal T}\!\mathit{y}_{\cal C}(1_{\cal C})$, and to any structure-preserving cwf-morphism $F:{\cal C}\to{\cal D}$ associates ${\bf C}(F):{\cal T}\!\mathit{y}_{\cal C}(1_{\cal C})\to{\cal T}\!\mathit{y}_{\cal D}(1_{\cal D})$ given by the action of $F$ on types and terms.

From cartesian categories to scwfs

Since ${\bf C}$ forgets the structure of contexts and only remembers closed types, we expect a functor ${\bf L}$ in the opposite direction to somehow reconstruct contexts. There are two natural candidates for this. The first is to reverse the effect of ${\bf C}$ by reconstructing the context formally, in an operation analogous to the construction of the cartesian category of polynomials in Lambek and Scott. We will detail this below. In this way we do not directly get an equivalence, because if ${\cal C}$ is an arbitrary scwf, the contexts of ${\bf L}{\bf C}({\cal C})$ are generated inductively from types. However, we get an equivalence for contextual scwfs.

The other option is to let the category of contexts of ${\bf L}({\cal C})$ be ${\cal C}$, reflecting the dual role of objects in cartesian categories as both contexts and types. Context comprehension is defined via finite products. As simple as it looks, this construction does not yield an equivalence even when restricting scwfs. (It would if one restricted to democratic scwfs such that for each $\Gamma\in{\cal C}_{0}$, we have $\Gamma=1\cdot\overline{\Gamma}$, but this is not a natural hypothesis since it is not satisfied by the syntax). It is, however, behind the biequivalence between scwfs and cartesian categories as property that we shall discuss in the following subsection.

Definition 15

If ${\cal C}$ is a cartesian category with structure, we define an scwf ${\bf L}({\cal C})$ analogously to the free scwf in Proposition 4. The set of types is $\mathrm{Ty}={\cal C}_{0}$. We define

[TABLE]

where $\Pi[B_{1},\dots,B_{m}]=(\dots(B_{1}\times B_{2})\dots\times B_{m})$ and $\Pi[]=1$. The terms are

[TABLE]

Substitution is defined as

[TABLE]

for $(\gamma_{1},\dots,\gamma_{n}):\Delta\to[A_{1},\dots,A_{n}]$ and $a\in\mathrm{Tm}(\Gamma,A)$ and composition in ${\bf L}({\cal C})$ by $(a_{1},\dots,a_{n})\circ\gamma=(a_{1}[\gamma],\dots,a_{n}[\gamma])$.

For $\Gamma=[A_{1},\dots,A_{n}]$ and $1\leq i\leq n$, we write $\mathrm{var}_{n}(i)\in\mathrm{Tm}(\Gamma,A_{i})$ for the corresponding variable, obtained as the $n$-ary projection. For $\Gamma=[A_{1},\dots,A_{n}]\in{\bf L}({\cal C})_{0}$ and $A\in\mathrm{Ty}$ we let $\Gamma\cdot A=[A_{1},\dots,A_{n},A]$. The projections are defined by

[TABLE]

We thus get an scwf with finite product types: the ${\mathbb{N}_{1}}$-structure is the terminal object of ${\cal C}$ and $A\times B$ is given by the cartesian product of ${\cal C}$. If $c\in\mathrm{Tm}(\Gamma,A\times B)$, the projections

[TABLE]

are immediate. (Note the overloading of $\mathrm{fst}$ and $\mathrm{snd}$.)

We observe that our construction yields that ${\bf C}({\bf L}({\cal C}))={\cal C}$ for each cartesian category with structure ${\cal C}$. This construction can be lifted to a functor

[TABLE]

where, given $F:{\cal C}\to{\cal D}$, ${\bf L}(F):{\bf L}({\cal C})\to{\bf L}({\cal D})$ is obtained by letting $F$ act component-wise. It is thus clear that all structure is preserved. Finally, ${\bf C}$ and ${\bf L}$ do not yet form an equivalence. Indeed, ${\bf L}({\bf C}({\cal C}))$ is always contextual since its contexts are inductively generated, whereas ${\cal C}$ might not be. For instance, any context of ${\cal C}$ which is not obtained as an iterated context extension of types is not accounted for in ${\bf L}({\bf C}({\cal C}))$. However, we have:

Theorem 4.1

The functors ${\bf C}$ and ${\bf L}$ form an equivalence of categories:

[TABLE]

Proof

It only remains to observe that for any contextual scwf ${\cal C}$ with finite products types we have the isomorphism ${\cal C}\cong{\bf L}({\bf C}({\cal C}))$, where this isomorphism sends a context $1\cdot A_{1}\cdot\dots\cdot A_{n}$ to $[A_{1},\dots,A_{n}]$.

4.3 Finite products as property

Cartesian categories as property

We now define a notion of cartesian category where finite products are defined as a property of a category.

Definition 16

Let ${\cal C}$ be a category. It is cartesian (as a property) if there exists a terminal object in ${\cal C}$, and if for any two objects $A,B\in{\cal C}_{0}$, there exists a cartesian product of $A$ and $B$, i.e. a triple $(P,\pi,\pi^{\prime})$ with $P\in{\cal C}_{0}$, $\pi:P\to A$, $\pi^{\prime}:P\to B$ satisfying the usual universal property.

By “there exists”, we mean mere existence. The choice of terminal objects and the assignment of $(P,\pi,\pi^{\prime})$ from $A$ and $B$ are not part of the structure. A cartesian category is just a particular kind of category with no additional data. Likewise, cartesian functors may be defined as:

Definition 17

A functor $F:{\cal C}\to{\cal D}$ is cartesian if the image of a terminal object is terminal, and the image of a product $(P,\pi,\pi^{\prime})$ is a product $(FP,F\pi,F\pi^{\prime})$. We let $\mathbf{CCp}^{2}$ be the $2$-category of small cartesian categories (with property) as objects, cartesian functors as $1$-cells, and natural transformations as $2$-cells.

Thus cartesian functors are just certain functors with no additional data. We regard $\mathbf{CCp}^{2}$ as a $2$-category because we will prove a biequivalence rather than an equivalence. Indeed, scwfs have chosen structure while cartesian categories (with property) do not. Going from an scwf to a cartesian category and back the structure is forgotten and then chosen again, and we cannot recover the original scwf up to isomorphism, only up to equivalence.

Remark 7

We could also introduce a notion of scwf with property, where context comprehension is only a property and not part of the structure. We will discuss this option briefly in the chapter about full cwfs.

Pseudo scwf-morphisms

Previously, we defined a notion of strict scwf-morphism, but this does not match the notion of cartesian functor as property. To address this mismatch we need a notion of pseudo cwf-morphism where structure is only preserved up to isomorphism.

Definition 18

A pseudo scwf-morphism from the scwf ${\cal C}$ to the scwf ${\cal D}$ consists of a functor $F:{\cal C}\to{\cal D}$, a function $F^{\mathrm{Ty}}:\mathrm{Ty}^{\cal C}\to\mathrm{Ty}^{\cal D}$, and a family

[TABLE]

of natural transformations. We write $F^{\mathrm{Tm}}_{\Gamma,A}$ for the component of $F^{\mathrm{Tm}}_{A}$ on $\Gamma$.

These data are subject to the conditions that (1) $F1$ is terminal in ${\cal D}$, and (2) for all $\Gamma\in{\cal C}_{0}$, $A\in\mathrm{Ty}^{\cal C}(\Gamma)$, the triple $(F(\Gamma\cdot A),F(\mathrm{p}_{\Gamma,A}),F_{\Gamma,A}^{\mathrm{Tm}}(\mathrm{q}_{\Gamma,A}))$ is a context comprehension of $F\Gamma$ and $F^{\mathrm{Ty}}(A)$ in ${\cal D}$.

For strict cwf-morphisms, the triple $(F(\Gamma\cdot A),F(\mathrm{p}_{\Gamma,A}),F_{\Gamma,A}^{\mathrm{Tm}}(\mathrm{q}_{\Gamma,A}))$ must coincide with the context comprehension of $F\Gamma$ and $F^{\mathrm{Ty}}(A)$ chosen by the scwf structure of ${\cal D}$. Here, we drop that assumption.

For related reasons, the equivalence will work slightly differently than in Section 4.2. There the equivalence followed the slogan “the cartesian category corresponding to a scwf is its category of closed terms”. However, in Theorem 4.1 products in a cartesian category ${\cal C}$ are used in a central way in the definition of terms in ${\bf L}({\cal C})$. These can be chosen once and for all, but the preservation of products up to isomorphism leads to an unwieldy definition of the functorial action of ${\bf L}$. Instead, we adopt a simpler approach under the slogan “the cartesian category corresponding to an scwf is its base category”. With the aim of getting a biequivalence rather than an equivalence, the requirement of contextuality will be replaced by the weaker democracy. This additional structure must then also be preserved.

Definition 19

A democratic pseudo scwf-morphism between democratic scwfs ${\cal C}$ and ${\cal D}$ additionally has, for each $\Gamma\in{\cal C}_{0}$, as isomorphism $\mathrm{d}_{\Gamma}:F^{\mathrm{Ty}}(\overline{\Gamma})\cong\overline{F\Gamma}$ in the category ${\cal T}\!\mathit{y}^{\cal C}(1)$, subject to a coherence diagram expressing that $F(\gamma_{\Gamma})=\gamma_{F\Gamma}$ modulo some transports111Using the existing structure one can define a canonical morphism from $\overline{F\Gamma}$ to $F^{\mathrm{Ty}}(\overline{\Gamma})$ in ${\cal T}\!\mathit{y}^{\cal C}(1)$. The coherence diagram amounts to $d_{\Gamma}$ being its inverse – hence $F$ being democratic amounts to requiring that the canonical map from $\overline{F\Gamma}$ to $F^{\mathrm{Ty}}(\overline{\Gamma})$ is an iso. (see ClairambaultD14, p.19).

A democratic scwf always has finite product types defined by ${\mathbb{N}_{1}}=\overline{1}$ and $A\times B=\overline{1\cdot A\cdot B}$. So our biequivalence holds without adding these as extra structure.

Definition 20

We write $\mathbf{Scwf}_{\mathrm{dem}}^{2}$ for the $2$-category with democratic small scwfs as objects, democratic pseudo scwf-morphisms as $1$-cells, and natural transformations between the underlying functors as $2$-cells.

One may wonder why the definition of $2$-cells does not have a type component. Such a component could be added, but then the biequivalence requires a coherence law which makes it redundant (see castellan:lmcs, p.7 and the expanded discussion in Appendix B).

The biequivalence

We now provide the components of the biequivalence. First we observe that there is a forgetful $2$-functor

[TABLE]

which maps a democratic scwf to its base category, a democratic pseudo cwf-morphism to its base functor, and leaves $2$-cells unchanged. That this is well-defined relies on the facts that (1) if ${\cal C}$ is a democratic scwf, then, the base category ${\cal C}$ is cartesian (with property), because products in ${\cal C}$ may be defined as $\Gamma\times\Delta=\Gamma\cdot\overline{\Delta}$; (2) if $F$ is a democratic pseudo cwf-morphism, then the fact that the base functor preserves products follows from preservation of context comprehension and democracy.

We now construct a $2$-functor in the other direction.

Proposition 6

There is a $2$-functor ${\bf L}^{2}:\mathbf{CCp}^{2}\to\mathbf{Scwf}_{\mathrm{dem}}^{2}$.

Proof

In every cartesian category (with property) ${\cal C}$ we choose a terminal object $1$ and a product $(A\times B,\mathrm{fst}_{A,B},\mathrm{snd}_{A,B})$ for every $A,B\in{\cal C}_{0}$.

We now turn ${\cal C}$ into an scwf in the following way. Its category of contexts is ${\cal C}$. Its set of types is $\mathrm{Ty}={\cal C}_{0}$. If $\Gamma\in{\cal C}_{0}$ and $A\in\mathrm{Ty}$, the terms are $\mathrm{Tm}_{\cal C}(\Gamma,A)={\cal C}(\Gamma,A)$. Context comprehension is given by finite products. Democracy is the isomorphism $\Gamma\cong 1\times\Gamma$. Likewise, a cartesian functor $F:{\cal C}\to{\cal D}$ is extended to types and terms in the obvious way, and yields a democratic pseudo cwf-morphism.

Theorem 4.2

The $2$-functors ${\bf C}^{2}$ and ${\bf L}^{2}$ form a biequivalence of $2$-categories:

[TABLE]

Proof

We have ${\bf C}^{2}{\bf L}^{2}=\mathrm{I}_{\mathbf{CCp}}$. To obtain a biequivalence we must construct pseudonatural transformations of $2$-functors (or pseudofunctors)

[TABLE]

which are inverses up to invertible modifications. Concretely, we construct, for each democratic scwf ${\cal C}$, pseudo cwf-morphisms $\eta_{\cal C}:{\cal C}\to{\bf L}^{2}{\bf C}^{2}{\cal C}$ and $\epsilon_{\cal C}:{\bf L}^{2}{\bf C}^{2}{\cal C}\to{\cal C}$, both with the identity functor as base component. Besides we have $\eta_{\cal C}^{\mathrm{Ty}}(A)=1.A$ and $\epsilon_{\cal C}^{\mathrm{Ty}}(\Gamma)=\overline{\Gamma}$ on types, and

[TABLE]

on terms. These two pseudo cwf-morphisms are pseudonatural in ${\cal C}$, and form an equivalence in $\mathbf{Scwf}^{2}_{\mathrm{dem}}$: $\eta_{\cal C}\circ\epsilon_{\cal C}$ and $\mathrm{id}_{{\bf C}^{2}{\bf L}^{2}{\cal C}}$ (resp. $\epsilon_{\cal C}\circ\eta_{\cal C}$ and $\mathrm{id}_{{\cal C}}$) are related by invertible $2$-cells with the identity as component. Finally, by unfolding definitions it follows that the invertible $2$-cells satisfy the coherence condition for modifications between pseudonatural transformations.

Together, Theorems 4.1 and 4.2 give two different points of view on the correspondence between scwfs and cartesian categories. It is interesting that we need to use a biequivalence not just for Martin-Löf’s type theory and locally cartesian closed categories as in ClairambaultD14, but already for cartesian categories if we omit chosen structure. For cartesian categories we can build both an equivalence (with structure) and a biequivalence (with property), whereas it seems that only the latter is possible for finitely complete categories and locally cartesian closed categories.

4.4 Adding function types

Before going on to the dependently typed case, we mention how to add function types to the previous equivalences and biequivalences. First, we recall:

Definition 21

A cartesian closed category (with structure) is a cartesian category (with structure) and an operation which to $A,B\in{\cal C}_{0}$ assigns an object $A\Rightarrow B\in{\cal C}_{0}$ with an evaluation

[TABLE]

such that for all $f:C\times A\to B$, $\exists!h:C\to A\Rightarrow B$ s.t. $\mathrm{\varepsilon}_{A,B}\circ(h\times A)=f$.

We write $\mathbf{CCCs}$ for the category having small cccs (with structure) as objects, and as morphisms, functors $F:{\cal C}\to{\cal D}$ preserving the structure on the nose, i.e. $F(A\Rightarrow^{\cal C}B)=FA\Rightarrow^{\cal D}FB$, and $F(\mathrm{\varepsilon}^{\cal C}_{A,B})=\mathrm{\varepsilon}^{\cal D}_{FA,FB}$.

Likewise, we may add function types to scwfs in the following way.

Definition 22

A $\Rightarrow$-structure on an scwf ${\cal C}$ consists of, for each $\Gamma\in{\cal C}_{0}$ and $A,B\in\mathrm{Ty}$, a type $A\Rightarrow B$ together with term formers

[TABLE]

s.t., for $a\in\mathrm{Tm}(\Gamma,A),b\in\mathrm{Tm}(\Gamma\cdot A,B),c\in\mathrm{Tm}(\Gamma,A\Rightarrow B)$,$\gamma\in{\cal C}(\Delta,\Gamma)$:

[TABLE]

If ${\cal C},{\cal D}$ have $\Rightarrow$-structure, a (strict) cwf-morphism $F:{\cal C}\to{\cal D}$ preserves it if $F(A\Rightarrow^{\cal C}B)=FA\Rightarrow^{\cal D}FB$, and $F(\mathrm{ap}_{\Gamma,A,B}^{\cal C}(c,a))=\mathrm{ap}_{F\Gamma,FA,FB}^{\cal D}(F(c),F(a))$.

Remark 8

An $\Rightarrow$-type structure on $({\cal C},\mathrm{Ty},\mathrm{Tm})$ is equivalent to the data of a binary type former $\Rightarrow$ and a natural isomorphism of preheaves

[TABLE]

i.e. a representation of $\mathrm{Tm}(-\cdot A,B)$.

For $\gamma:\Delta\to\Gamma$, the functorial action $\mathrm{Tm}(\gamma\cdot A,B)$ takes $b\in\mathrm{Tm}(\Gamma\cdot A,B)$ to $b[\langle\gamma\circ\mathrm{p},\mathrm{q}\rangle]\in\mathrm{Tm}(\Delta\cdot A,B)$. We recover $\mathrm{ap}_{\Gamma,A,B}(f,a)=\lambda^{-1}(f)[\langle\mathrm{id},a\rangle]$ and derive the $\beta$ and $\eta$-rules, and vice versa.

Let us write $\mathbf{Scwf}_{\mathrm{ctx}}^{{\mathbb{N}_{1}},\times,\Rightarrow}$ for the category having as objects small contextual scwfs with an ${\mathbb{N}_{1}}$-structure, a $\times$-structure and a $\Rightarrow$-structure, and as morphisms the strict cwf-morphisms preserving this structure on the nose.

Theorem 4.3

The categories $\mathbf{CCCs}$ and $\mathbf{Scwf}_{\mathrm{ctx}}^{{\mathbb{N}_{1}},\times,\Rightarrow}$ are equivalent.

Proof

Straightforward extension of Theorem 4.1, which boils down to the definition of evaluation from application and vice versa.

This is our version of one of the main results of the Lambek and Scott book, namely Theorem 3.11, the equivalence between simply-typed $\lambda$-calculi and cartesian closed categories, where $\mathbf{Scwf}_{\mathrm{ctx}}^{{\mathbb{N}_{1}},\times,\Rightarrow}$ plays the role of the category of typed $\lambda$-calculi. And indeed, the simply-typed $\lambda$-calculus arises as the free scwf with $\Rightarrow$-structure over a set of types. If ${\cal B}$ is a set of basic types, we consider ${\cal B}$-$\mathbf{Scwf}_{\mathrm{ctx}}^{\Rightarrow}$ to be the category with objects scwfs with $\Rightarrow$-structure together with an interpretation function $\llbracket-\rrbracket_{\cal C}:{\cal B}\to\mathrm{Ty}$; and as morphisms the strict scwf-morphisms that preserve $\Rightarrow$-structure and commute with the interpretation. Then we have:

Proposition 7

For all sets ${\cal B}$, the category ${\cal B}$-$\mathbf{Scwf}^{\Rightarrow}$ has an initial object.

Construction 1. Just as for ucwfs and scwfs, we can immediately turn the definition of scwf with $\Rightarrow$-structure into an inductive definition of a free such. The resulting theory is a well-scoped variable-free version of the typed $\lambda\sigma$-calculus with base types in ${\cal B}$.

Construction 2. Alternatively, we can construct an scwf with $\Rightarrow$-structure free over ${\cal B}$ from a well-scoped version of the simply-typed $\lambda\beta\eta$-calculus. The construction follows that of Proposition 4, except that the terms are now inductively defined with the following three constructors:

[TABLE]

The definition of substitution is then extended with

[TABLE]

for $\gamma\in{\cal C}(\Delta,\Gamma)$. Finally we quotient with the equivalence relation generated by $\beta\eta$-conversion:

[TABLE]

The two constructions and the proof of their equivalence have been formalised in Agda by Brilakis Brilakis18.

We can of course construct free objects in $\mathbf{Scwf}^{{\mathbb{N}_{1}},\times,\Rightarrow}$ and other categories of scwfs with extra type structure in a similar way. Likewise, we can show a biequivalence between the $2$-category of cccs as property rather than structure, and the extension of the $2$-category $\mathbf{Scwf}^{2}_{\mathrm{dem}}$ where scwfs additionally have a $\Rightarrow$-structure, which is preserved up to isomorphism. We omit the details since they are similar to those in the proof of Theorem 4.2.

5 Dependently typed categories with families

We now return to full dependently typed cwfs. After discussing alternative definitions, we show an explicit construction of a free cwf. We then add the type formers $\mathrm{I},\Sigma,$ and $\Pi$ and give an overview of the biequivalence theorems in Clairambault and Dybjer ClairambaultD11; ClairambaultD14. Finally we outline the construction of a bifree lccc and the proof of undecidability of equality castellan:tlca2015; castellan:lmcs in this lccc.

5.1 Plain cwfs

Alternative definitions

Context comprehension via representable presheaves. First, observe that the family valued presheaf $T:{\cal C}^{\mathrm{op}}\to\mathrm{Fam}$ may equivalently be given by two $\mathrm{Set}$-valued presheaves

[TABLE]

where $\int^{\cal C}\mathrm{Ty}$ is the category of elements of the first presheaf. Context comprehension for full cwfs is equivalent to requiring that for all $\Gamma\in{\cal C}_{0}$ and $A\in\mathrm{Ty}(\Gamma)$, there is a representation $\Gamma\cdot A$ of the presheaf

[TABLE]

Remark 9

Alternatively, we could consider a weaker notion of cwf with context comprehension as a property rather than structure. We then only require that the above presheaves are representable, that is, we only require the mere existence of the representing presheaves.

Natural models. More radically, Awodey Awodey18 and Fiore Fiore12 propose to replace the $\mathrm{Fam}$-valued presheaf $T:{\cal C}^{\mathrm{op}}\to\mathrm{Fam}$ by two set valued presheaves

[TABLE]

and a natural transformation $\mathsf{typeof}:\mathrm{Tm}\Rightarrow\mathrm{Ty}$. One can then define context comprehension in terms of representable natural transformations. Let ${\mathrm{Y}}:{\cal C}\to\mathrm{Set}^{{\cal C}^{\mathrm{op}}}$ be the Yoneda embedding. A natural transformation $\sigma:G\Rightarrow F$ between presheaves on ${\cal C}$ is representable in the sense of Grothendieck, if for all $C\in{\cal C}_{0}$ and $c\in F(C)$, there are $D\in{\cal C}_{0},p\in{\cal C}(D,C)$, and $d\in G(D)$, such that the following diagram in the category of presheaves is a pullback:

[TABLE]

where $c$ and $d$ in the diagram are shorthand for the corresponding respective natural transformations $F(-)(c)$ and $G(-)(d)$ from the Yoneda lemma.

Hence, $\mathsf{typeof}:\mathrm{Tm}\Rightarrow\mathrm{Ty}$ is representable provided for all $\Gamma\in{\cal C}_{0}$ and $A\in\mathrm{Ty}(\Gamma)$, there is $\Gamma\cdot A\in{\cal C}_{0}$, $\mathrm{p}_{\Gamma,A}\in{\cal C}(\Gamma\cdot A,\Gamma)$, and $\mathrm{q}_{\Gamma,A}\in\mathrm{Tm}(\Gamma\cdot A)$, such that the following diagram is a pullback:

[TABLE]

We emphasize that the function that maps $\Gamma$ and $A$ to the triple $\Gamma\cdot A,\mathrm{p}_{\Gamma,A},\mathrm{q}_{\Gamma,A}$ is part of the structure – the natural transformation $\mathsf{typeof}:\mathrm{Tm}\Rightarrow\mathrm{Ty}$ is represented.

Awodey Awodey18 and Newstead Newstead:phd study this notion under the name natural models. We refer to their papers for further development of the theory. Note that this approach suggests an essentially algebraic view of cwfs rather than a generalized algebraic one. Here we have only one sort $\mathrm{Tm}(\Gamma)$ containing all terms $a$ of some type $A=\mathsf{typeof}(a)\in\mathrm{Ty}(\Gamma)$. In other words terms are “fibred” over types.

Remark 10

Alternatively, we get a notion of natural model with context comprehension as property if we only require the mere representability of the natural transformation $\mathsf{typeof}$. This notion is considered by Ahrens, Lumsdaine, and Voevodsky AhrensLV18.

Categories with attributes. There is a certain redundancy in the definition of categories with families, since we can show (using context comprehension) that terms are in one-to-one correspondence with certain morphisms of the base category:

[TABLE]

In other words, terms in $\mathrm{Tm}(\Gamma,A)$ correspond to sections of $\mathrm{p}_{\Gamma,A}$, the display map for the type $A$.

We can thus remove the term part of cwfs and get the closely related notion of a category with attributes (cwa) HofmannM:intttl. This consists of a category ${\cal C}$ with a terminal object, a presheaf $\mathrm{Ty}:{\cal C}^{\mathrm{op}}\to\mathrm{Set}$ for types and substitutions, and an operation which given $\Gamma\in{\cal C}_{0}$ and $A\in\mathrm{Ty}(\Gamma)$ associates a context $\Gamma\cdot A$ and a “display map” $\mathrm{p}_{\Gamma,A}:\Gamma\cdot A\to\Gamma$; and for each $\gamma:\Delta\to\Gamma$, a chosen pullback square:

[TABLE]

This follows the idea of “substitutions as pullbacks” familiar in categorical logic. This choice of pullbacks is finally required to be split, in the sense that the association of substitutions to pullback squares is functorial.

It is fairly easy to prove that categories with attributes are equivalent to categories with families hofmann:cambridge. This proof and several other proofs relating models of dependent type theory are formalized in the UniMath system by Ahrens, Lumsdaine, and Voevodsky AhrensLV18.

Categories with attributes predate categories with families. In fact categories with families were originally introduced dybjer:torino as a modification of cwas. The main point of the change was to obtain a definition that can be expressed as a generalised algebraic theory with a transparent connection with Martin-Löf’s explicit substitution calculus formulation of dependent type theory. This was achieved by making the family of terms into an explicit part of the definition and formalize the sets of types and terms and their substitution operations as a family valued presheaf. In this way the pullback property of type substitution could be removed from the definition since it can be derived from the other part of the structure.

A free cwf

As in the previous sections, we next show how to build a free cwf. Recall that in the simply-typed case, we built a free scwf over a set ${\cal B}$ of basic types, and we could do the same here. However, for simplicity, and because it suffices to prove the undecidability theorem, we will assume that there is only one basic type $o$. The rules used for the construction of this plain free cwf (except the rule for the base type) correspond to the general rules for dependent type theory. This construction can then be extended to the case where we add rules for specific type formers.

The construction of initial ucwfs and free scwfs are rather immediate from the definitions: simply turn the definitions into simultaneous inductive definitions of the families of terms and substitutions, and then define equality of terms and substitutions by another simultaneous inductive definition. Unfortunately, the construction of free full cwfs is no longer as direct. What complicates the matter is the type-equality rule, which means that typability of terms may depend on proofs of equality of types. Thus we have to define equality of contexts, context morphisms, types, and terms simultaneously with their elements. Apart from this the recipe is similar: take the definition of the generalised algebraic theory of cwfs and turn it into a mutual inductive definition where all equality reasoning is made explicit.

To build the free cwf we first define raw contexts, raw substitutions, raw types, and raw terms.

[TABLE]

We then need to define the well-formed contexts and types, and the well-typed substitutions and terms. In Martin-Löf’s substitution calculus these are defined by a system of inference rules for all the eight forms of judgments. Here we choose a more economical way, by only defining well-formed equal contexts and types, and the well-typed equal substitutions and terms. Thus we define four families of partial equivalence relations (pers), corresponding to the four forms of equality judgments, by a mutual inductive definition:

[TABLE]

where $\Gamma,\Gamma^{\prime}\in{\tt Ctx},\gamma,\gamma^{\prime}\in{\tt Sub},A,A^{\prime}\in{\tt Ty},$ and $a,a^{\prime}\in{\tt Tm}$. The basic judgment forms can then be defined as the reflexive instances of the pers:

• •

$\Gamma\vdash$ abbreviates $\Gamma=\Gamma\vdash$,

• •

$\Gamma\vdash A$ abbreviates $\Gamma\vdash A=A$,

• •

$\Delta\vdash\gamma:\Gamma$ abbreviates $\Delta\vdash\gamma=\gamma:\Gamma$,

• •

$\Gamma\vdash a:A$ abbreviates $\Gamma\vdash a=a:A$.

The four families of partial equivalence relations (pers) are given by a simultaneous inductive definition with the following introduction rules:

** Per-rules **  {mathpar} \inferrule

Γ= Γ’ ⊢

Γ’ = Γ” ⊢ Γ= Γ” ⊢

\inferrule

Γ= Γ’ ⊢ Γ’ = Γ⊢

\inferrule

Δ⊢γ= γ’ : Γ

Δ⊢γ’ = γ” : Γ Δ⊢γ= γ” : Γ

\inferrule

Δ⊢γ= γ’ : Γ Δ⊢γ’ = γ: Γ

\inferrule

Γ⊢A = A’

Γ⊢A’ = A” Γ⊢A = A”

\inferrule

Γ⊢A = A’ Γ⊢A’ = A

\inferrule

Γ⊢a = a’ : A

Γ⊢a’ = a” : A Γ⊢a = a” : A

\inferrule

Γ⊢a = a’ : A Γ⊢a’ = a : A

** Preservation rules for judgments **  {mathpar} \inferrule

Γ = Γ’ ⊢

Δ = Δ’ ⊢

Γ ⊢γ= γ’: Δ Γ’ ⊢γ= γ’ : Δ’

\inferrule

Γ = Γ’ ⊢

Γ ⊢A = A’ Γ’ ⊢A = A’

\inferrule

Γ = Γ’ ⊢

Γ⊢A = A’

Γ ⊢a = a’ : A Γ’ ⊢a = a’ : A’

** Congruence rules for operators **  {mathpar} \inferrule

1 = 1 ⊢

\inferrule

Γ= Γ’ ⊢

Γ⊢A = A’ Γ⋅A = Γ’ ⋅A’⊢

\inferrule

Γ⊢A=A’

Δ⊢γ= γ’ : Γ Δ⊢A[γ] = A’[γ’]

\inferrule

Γ= Γ’ ⊢ Γ⊢id_Γ= id_Γ’ : Γ

\inferrule

Γ= Γ’ ⊢ Γ⊢⟨⟩_Γ= ⟨⟩_Γ’ : 1

\inferrule

Γ ⊢δ= δ’ : Δ

Δ ⊢γ= γ’: Θ Γ ⊢γ∘δ= γ’ ∘δ’ : Θ

\inferrule

Γ⊢A = A’ Γ⋅A ⊢p_A = p_A’ : Γ

\inferrule

Γ⊢A = A’

Δ⊢γ= γ’ : Γ

Δ⊢a = a’ : A[γ] Δ⊢⟨γ,a ⟩_A = ⟨γ’,a’ ⟩_A’ : Γ⋅A

\inferrule

Γ⊢a = a’ : A

Δ⊢γ= γ’ : Γ Δ⊢a[γ] = a’[γ’] : A[γ]

\inferrule

Γ⊢A = A’ Γ⋅A ⊢q_A = q_A’ : A[p_A]

** Conversion rules **  {mathpar} \inferrule

Δ⊢θ: Θ

Γ⊢δ: Δ

Ξ⊢γ: Γ Ξ⊢(θ∘δ) ∘γ= θ∘(δ∘γ) : Θ

\inferrule

Γ⊢γ: Δ Γ⊢γ= id_Δ∘γ: Δ

\inferrule

Γ⊢γ: Δ Γ⊢γ= γ∘id_Γ: Δ

\inferrule

Γ⊢A

Δ⊢γ: Γ

Θ⊢δ: Δ Θ⊢A[γ∘δ] = (A[γ])[δ]

\inferrule

Γ⊢A Γ⊢A[id_Γ] = A

\inferrule

Γ⊢a : A

Δ⊢γ: Γ

Θ⊢δ: Δ Θ⊢a[γ∘δ] = (a[γ])[δ] : (A[γ])[δ]

\inferrule

Γ⊢a : A Γ⊢a[id_Γ] = a : A

\inferrule

Γ⊢γ: 1 Γ⊢γ= ⟨⟩_Γ : 1

\inferrule

Γ⊢A

Δ⊢γ: Γ

Δ⊢a : A[γ] Δ⊢p_A ∘⟨γ,a ⟩_A = γ: Γ

\inferrule

Γ⊢A

Δ⊢γ: Γ

Δ⊢a : A[γ] Δ⊢q_A[⟨γ,a ⟩_A] = a : A[γ]

\inferrule

Δ⊢γ: Γ⋅A Δ⊢γ= ⟨p_A ∘γ, q_A[γ] ⟩_A : Γ⋅A

These rules correspond to the general rules for intuitionistic type theory, that is, the rules which are given before the rules for the type formers, see the discussion in Section 2.1.

Finally, we have a rule for the base type:

** Base type **  {mathpar} \inferrule

1 ⊢o = o

Theorem 5.1

The cwf ${\cal T}$, defined with the following data:

• •

${\cal T}_{0}=\{{\Gamma}\ |\ \Gamma\vdash\}/\!\!=^{c}$, where ${\Gamma}=^{c}{\Gamma}^{\prime}$ if ${\Gamma}={\Gamma}^{\prime}\vdash$ is derivable.

• •

${\cal T}([{\Gamma}],[{\Delta}])=\{\gamma\ |\ \Gamma\vdash\gamma:{\Delta}\}/\!\!=^{\Gamma}_{\Delta}$* where $\gamma=^{\Gamma}_{\Delta}\gamma^{\prime}$ iff ${\Gamma}\vdash\gamma=\gamma^{\prime}:{\Delta}$ is derivable. Note that this makes sense since it only depends on the equivalence classes $[\Gamma]$ and $[\Delta]$ of $\Gamma$ and $\Delta$ (morphisms and morphism equality are preserved by object equality).*

• •

$\mathrm{Ty}_{\cal T}([{\Gamma}])=\{A\ |\ \Gamma\vdash A\}/=^{\Gamma}$* where $A=^{\Gamma}B$ if $\Gamma\vdash A=B$.*

• •

$\mathrm{Tm}_{\cal T}([{\Gamma}],[A])=\{a\ |\ \Gamma\vdash a:A\}/=^{\Gamma}_{A}$* where $a=^{\Gamma}_{A}a^{\prime}$ if $\Gamma\vdash a=a^{\prime}:A$.*

is the free cwf on one base type.

By free cwf on one base type we mean that it is initial in the category $\mathbf{Cwf}^{o}$ having as objects small cwfs with a chosen type $o\in\mathrm{Ty}(1)$, and as morphisms the strict cwf-morphisms which preserve the chosen base type. We refer to Castellan, Clairambault, and Dybjer castellan:tlca2015; castellan:lmcs for the proof of freeness of ${\cal T}$.

In the papers mentioned above, we show that the free cwf is also bifree in the fully dependent version $\mathbf{Cwf}_{\mathrm{dem}}^{2}$of the $2$-category $\mathbf{Scwf}_{\mathrm{dem}}^{2}$ of Section 4.3 (with a base type). Before we consider additional structure, let us define the morphisms of this $2$-category, which will play an important role later on.

Definition 23

A pseudo-cwf morphism from a cwf ${\cal C}$ to a cwf ${\cal D}$ is a pair $(F,\sigma)$ where $F:{\cal C}\rightarrow{\cal D}$ is a functor and for each $\Gamma\in{\cal C}_{0}$, $\sigma_{\Gamma}$ is a Fam-morphism from $T\Gamma$ to $T^{\prime}F\Gamma$ preserving the structure up to isomorphism. In particular there are isomorphisms (again writing $F$ for all components):

[TABLE]

where $\cong_{F\Gamma}$ means that it is an isomorphism in the category $\mathrm{Ty}^{\cal D}(F\Gamma)$ of types over $F\Gamma$ in ${\cal D}$. These data must satisfy some coherence diagrams (see ClairambaultD14, Definition 3.1 for details).

We can now prove the following.

Theorem 5.2

The cwf ${\cal T}$ is bifree over one base type, i.e. it is bi-initial in the $2$-category $\mathbf{Cwf}_{o}^{2}$ having as objects small cwfs with one base type, as $1$-cells pseudo cwf-morphisms preserving the base type up to iso, and as $2$-cells natural transformations between the base functors.

Proof

We refer the reader to castellan:lmcs for details and proofs. We remark that ${\cal T}$ is democratic and also bi-initial in $\mathbf{Cwf}_{o,\mathrm{dem}}^{2}$.

Previously we defined initial ucwfs and scwfs (with extra structure) in two ways: with and without explicit substitutions. The above construction of the free cwf gives rise to a calculus with explicit substitutions. There is an analogous construction of a free cwf where substitution is instead defined as a meta-operation, which is close to the standard formulation of the general rules for dependent type theory. We do not have space to spell out this construction with implicit substitutions here, but refer to Streicher streicher:semtt.

5.2 Extensional identity types, $\Sigma$-types, and finite limits

Extensional identity types and $\Sigma$-types

We now add extensional identity types and $\Sigma$-types to cwfs.

Definition 24

An $\mathrm{I}_{\mathrm{ext}}$-structure on cwf ${\cal C}$ consists of for each $\Gamma\in{\cal C}_{0}$, $A\in\mathrm{Ty}(\Gamma)$ and $a,a^{\prime}\in\mathrm{Tm}(\Gamma,A)$, a type $\mathrm{I}_{A}(a,a^{\prime})$; and a term

[TABLE]

such that if $c\in\mathrm{Tm}(\Gamma,\mathrm{I}_{A}(a,a^{\prime}))$ then $a=a^{\prime}$ and $c=\mathrm{r}_{A,a}$, and such that

[TABLE]

for any $\gamma\in{\cal C}(\Delta,\Gamma)$.

This captures extensional, rather than intensional, identity types. The difference is that the two equations $a=a^{\prime}$ and $c=\mathrm{r}_{A,a}$ whenever $\mathrm{Tm}(\Gamma,\mathrm{I}_{A}(a,a^{\prime}))$ is inhabited are only valid for extensional identity types. It follows that the reflexivity term is preserved by substitution as well: $\mathrm{r}_{A,a}[\gamma]$ is forced to coincide with $\mathrm{r}_{A[\gamma],a[\gamma]}$ since the two both inhabit $\mathrm{I}_{A[\gamma]}(a[\gamma],a[\gamma])$.

As in the previous sections, strict cwf-functors between cwfs equipped with an extensional identity type structure are said to preserve it strictly if the action on morphisms maps the components of the source to the components of the target, on the nose. In the remainder of this paper, a more important role will be played by morphisms preserving this structure up to isomorphism. If $F:{\cal C}\to{\cal D}$ is a pseudo cwf-morphism where ${\cal C}$ and ${\cal D}$ are equipped with an $\mathrm{I}_{\mathrm{ext}}$-structure, we say that it preserves it provided there is, for any $A\in\mathrm{Ty}^{\cal C}(\Gamma)$, $a,a^{\prime}\in\mathrm{Tm}^{\cal C}(\Gamma,A)$, an isomorphism

[TABLE]

in $\mathrm{Ty}^{\cal D}(\Gamma)$.

Definition 25

The definition of an ${\mathbb{N}_{1}}$-structure for a cwf is the same as for an scwf, except that ${\mathbb{N}_{1}}$ now is also required to be stable under substitution, i.e., a natural transformation of type presheaves

[TABLE]

and, as before, a natural isomorphism between preheaves

[TABLE]

where again $1$ is the constant singleton presheaf.

If a cwf is democratic it has an ${\mathbb{N}_{1}}$-structure, since ${\mathbb{N}_{1}}$ may be defined as $\overline{1}\in\mathrm{Ty}(1)$.

Definition 26

A $\Sigma$-structure on a cwf ${\cal C}$ consists of, for each $\Gamma\in{\cal C}_{0}$, $A\in\mathrm{Ty}(\Gamma)$, $B\in\mathrm{Ty}(\Gamma\cdot A)$, a type $\Sigma(A,B)\in\mathrm{Ty}(\Gamma)$, and term formers

[TABLE]

subject to the same equations as in Definition 12, plus the additional

[TABLE]

A $\Sigma$-type structure thus gives rise to a natural transformation $\Sigma$ of type presheaves

[TABLE]

and isomorphisms

[TABLE]

which are stable under substitution (see Definition 12). Note the difference between this and the characterization of a $\times$-structure as natural isomorphisms between presheaves. Since $A\in\mathrm{Ty}(\Gamma)$ and $B\in\mathrm{Ty}(\Gamma\cdot A)$ are dependent types the two sides of the isomorphism are no longer presheaves.

It follows by induction on the length of a context that a contextual cwf with an ${\mathbb{N}_{1}}$-structure and a $\Sigma$-structure is democratic.

As usual, a strict cwf-morphism between cwfs with $\Sigma$-structure preserves it if it maps the structure in the source cwf to the structure in the target cwf on the nose. For pseudo-morphisms, it turns out that there is nothing to add. In any cwf ${\cal C}$ with a $\Sigma$-structure, for any $\Gamma\in{\cal C}_{0}$, $A\in\mathrm{Ty}(\Gamma)$ and $B\in\mathrm{Ty}(\Gamma\cdot A)$, we have the isomorphism $\Gamma\cdot A\cdot B\cong\Gamma\cdot\Sigma(A,B)$. Since pseudo cwf-morphisms are already known to preserve context extension, it follows that they automatically preserve $\Sigma$-structures, in the following sense.

Proposition 8

A pseudo cwf-morphism $F$ from ${\cal C}$ to ${\cal D}$, where both cwfs have a $\Sigma$-structure, also preserves it in the sense that there is an isomorphism:

[TABLE]

such that projections and pairs are preserved, modulo some transports (notably following $s_{A,B}$, see Proposition 3.5 in ClairambaultD14 for details).

Let us write $\mathbf{Cwf}_{\mathrm{dem}}^{2,\mathrm{I}_{\mathrm{ext}},\Sigma}$ for the $2$-category having as objects small democratic cwfs with an $\mathrm{I}_{\mathrm{ext}}$-structure and a $\Sigma$-structure; as morphisms the pseudo cwf-morphisms preserving these structures up to isomorphism, and as $2$-cells natural transformations between the base functors.

The biequivalence with finitely complete categories

In Theorem 4.2, we proved a biequivalence between democratic scwfs and cartesian categories. We now sketch the dependently typed version: a biequivalence between democratic cwfs with $\mathrm{I}_{\mathrm{ext}}$- and $\Sigma$-structures; and finitely complete (also called left exact) categories.

Definition 27

A category ${\cal C}$ is finitely complete if it has all finite limits. A functor $F:{\cal C}\to{\cal D}$ between finitely complete categories is left exact if it preserves finite limits: the image of a limiting cone is a limiting cone.

We write $\mathbf{FL}$ for the $2$-category with small finitely complete categories as objects, left exact functors as $1$-cells, and natural transformations as $2$-cells.

In the light of Section 4, it is natural to insist that we consider finitely complete categories to be categories with property, rather than with additional structure. How could we make a corresponding notion of finitely complete categories with structure? One could ask for a cartesian category with structure additionally equipped with a choice of equalizers; one could ask for a choice of pullbacks (and a terminal object); or one could directly ask for a choice of a limit of any finite diagram. One could then consider a category of these, where structure is preserved on the nose. However, the strict equivalence of Theorem 4.3 does not to extend to this situation: whereas in the simply-typed case we may prove an equivalence with structure or a biequivalence with property, it seems that the only possibility to relate the two in the present case is the biequivalence. We will comment again on that later.

Let us now give some information about the main ingredients of the biequivalence. The first observation is that if ${\cal C}$ is a cwf with $\mathrm{I}_{\mathrm{ext}}$ and $\Sigma$-structures, then for each $\Gamma\in{\cal C}_{0}$ there is an equivalence between the category of types over a context $\mathrm{Ty}(\Gamma)$, and the slice category ${\cal C}/\Gamma$. Indeed, each type $A\in\mathrm{Ty}(\Gamma)$ yields a display map $\mathrm{p}_{\Gamma,A}:\Gamma\cdot A\to\Gamma$ regarded as an object in ${\cal C}/\Gamma$. In the other direction, any $\gamma:\Delta\to\Gamma$ is isomorphic (in ${\cal C}/\Gamma$) to

[TABLE]

a projection corresponding to a type $\mathsf{Inv}(\gamma)\in\mathrm{Ty}(\Gamma)$, the “inverse image”, defined as (a cwf formalization of) $x:\Gamma\vdash\Sigma_{y:\Delta}(\gamma(x)=y)\mathrm{~{}type}$. Via this equivalence of categories it follows that for each $\Gamma\in{\cal C}_{0}$ the slice category ${\cal C}/\Gamma$ has products, that is, ${\cal C}$ has pullbacks. Since it has a terminal object, it has all finite limits. Likewise, if $F:{\cal C}\to{\cal D}$ is a $1$-cell in $\mathbf{Cwf}_{\mathrm{dem}}^{2,\mathrm{I}_{\mathrm{ext}},\Sigma}$ then it preserves pullbacks in ${\cal C}$ – in fact, we have an equivalence:

Lemma 2

Let ${\cal C}$ and ${\cal D}$ be democratic cwfs with $\mathrm{I}_{\mathrm{ext}}$- and $\Sigma$-structures and $F:{\cal C}\to{\cal D}$ be a pseudo cwf-morphism preserving democracy. Then, $F$ preserves the $\mathrm{I}_{\mathrm{ext}}$-structure if and only if $F$ preserves pullbacks.

Proof

The harder direction is only if, which boils down to the preservation of the inverse image. This can be proved from intricate calculations on cwf combinators. Details appear in ClairambaultD14, Lemma 4.3 and Proposition 4.4.

We can then show that there is a forgetful $2$-functor:

[TABLE]

The other direction is much more complicated. The equivalence of categories $\mathrm{Ty}(\Gamma)\simeq{\cal C}/\Gamma$ together with Seely’s approach to interpreting type theory in locally cartesian closed categories SeelyRAG:locccc suggest, from a finitely complete category ${\cal C}$, to redefine the types over $\Gamma$ as the objects of the slice category ${\cal C}/\Gamma$. Now the question is how to define substitution, i.e.

[TABLE]

for $\gamma:\Delta\to\Gamma$? In categorical logic, substitution is usually defined by pullback. However, the problem is that for an arbitrary choice of pullbacks, there is no reason why this assignment should be functorial. Consider the following two pullback squares:

[TABLE]

There is no reason why the left hand side diagram, which is a composition of chosen pullbacks, and the right hand side diagram, which is a chosen pullback, should coincide – although they are always isomorphic. In other words the codomain fibration is not split, whereas the fibration implicit in a cwf is always split. This is a fundamental issue: Seely’s proposed interpretation SeelyRAG:locccc sends types that are provably equal in the syntax to morphisms in ${\cal C}$ that are only known to be isomorphic. This coherence problem may be solved in two ways: Curien curien:fi proposes to change the syntax by weakening equality to isomorphism in the syntax, enriching it with explicit coercions between isomorphic types, and showing the extended syntax equivalent to the original via a difficult coherence theorem. We refer to Curien, Garner, and Hofmann CurienGH14 for details.

In hofmann:csl, Hofmann proposes instead to solve the problem by exploiting a construction of Bénabou BenabouJ:fibcfn, which associates to each fibration an equivalent split fibration. This construction can be extended to dependent types: given a category ${\cal C}$ with finite limits, we build a cwf whose types are no longer just objects of ${\cal C}/\Gamma$, but objects of ${\cal C}/\Gamma$ with a pre-chosen substitution pullback, for every possible substitution – such that this choice is split. For details, the reader is referred to ClairambaultD14, Section 5. As we show there, Hofmann’s construction yields a pseudofunctor:

[TABLE]

This is not a functor: when sending $F:{\cal C}\to{\cal D}$ to $\mathbf{Cwf}_{\mathrm{dem}}^{2,\mathrm{I}_{\mathrm{ext}},\Sigma}$, one must extend $F$ to types, i.e. display maps $\mathrm{p}$ together with a fixed choice of substitution pullbacks. But the choice of substitution pullbacks for $\mathrm{p}$ in ${\cal C}$ does not suffice to completely determine a choice of substitution pullbacks for $F\mathrm{p}$ in ${\cal D}$, hence those must be chosen; causing ${\bf L}$ to fail functoriality on the nose.

For this reason, it seems unlikely that switching to finite limit categories with structure would yield an equivalence of categories with strict maps, unless one considers categories with finite limits with a split choice of pullbacks222One reviewer pointed out that one should not attribute the weakness of the equivalence solely to the pseudo-functoriality of ${\bf L}$. Indeed, the reviewer suggests that a version of ${\bf L}$ based on Lumsdaine-Warren’s “left adjoint splitting” DBLP:journals/tocl/LumsdaineW15 rather than Bénabou-Hofmann’s construction might be functorial, yet still only yield a biequivalence..

Theorem 5.3

There is a biequivalence of $2$-categories $\mathbf{FL}^{2}\simeq\mathbf{Cwf}_{\mathrm{dem}}^{2,\mathrm{I}_{\mathrm{ext}},\Sigma}$.

Proof

Once the mediating pseudofunctors are constructed, the proof is fairly close to that of Theorem 4.2. The reader is referred to ClairambaultD14, Section 6 for details.

5.3 $\Pi$-types and locally cartesian closed categories

We now add $\Pi$-types and extend the results of Section 5.2. We shall sketch that Theorem 5.3 yields a biequivalence with locally cartesian closed categories.

$\Pi$-types

Definition 28

A $\Pi$-type structure on a cwf ${\cal C}$ consists of, for each $\Gamma\in{\cal C}_{0}$, $A\in\mathrm{Ty}(\Gamma)$, $B\in\mathrm{Ty}(\Gamma\cdot A)$, a type $\Pi(A,B)\in\mathrm{Ty}(\Gamma)$, and term formers

[TABLE]

subject to the equations of Definition 22, plus the additional

[TABLE]

We note that a $\Pi$-type structure gives rise to a natural transformation $\Pi$ of type presheaves:

[TABLE]

and isomorphisms

[TABLE]

which are stable under substitution (see Definition 22). Note the difference between this and the characterization of an $\Rightarrow$-structure as natural isomorphisms between presheaves. Since $A\in\mathrm{Ty}(\Gamma)$ and $B\in\mathrm{Ty}(\Gamma\cdot A)$ are dependent types $\mathrm{Tm}_{\cal C}(\Gamma\cdot A,B)$ and $\mathrm{Tm}_{\cal C}(\Gamma,\Pi_{\Gamma}(A,B))$ are no longer families of presheaves.

Strict cwf-morphisms between cwfs with $\Pi$-structure preserve it if they map all components of the $\Pi$-structure in the source cwf to the same component in the target cwf, on the nose. For pseudo-morphisms, we define:

Definition 29

A pseudo cwf-morphism $F$ from ${\cal C}$ to ${\cal D}$, where both cwfs have a $\Pi$-structure, also preserves it provided for all $\Gamma\in{\cal C}_{0}$, $A\in\mathrm{Ty}(\Gamma)$ and $B\in\mathrm{Ty}(\Gamma\cdot A)$ there is an isomorphism in $\mathrm{Ty}^{\cal D}(F\Gamma)$

[TABLE]

such that application is preserved, modulo some transports (notably by $i_{A,B}$, see Definition 9 in ClairambaultD14 for details).

It is sufficient to require preservation of application, preservation of abstraction then follows. This follows the situation in cartesian closed categories with structure where evaluation is part of the structure, whereas abstraction is defined uniquely by the universal property – and although functors are only required to preserve evaluation, it follows that they preserve abstraction too.

Let us write $\mathbf{Cwf}_{\mathrm{dem}}^{2,\mathrm{I}_{\mathrm{ext}},\Sigma,\Pi}$ for the $2$-category where the objects are small democratic cwfs with $\mathrm{I}_{\mathrm{ext}}$-structure, $\Sigma$-structure and $\Pi$-structure; the morphisms are pseudo cwf-morphisms preserving this structure (up to isomorphism), and the $2$-cells are natural transformations between the base functors.

The biequivalence with locally cartesian closed categories

Let us first recall locally cartesian closed categories.

Definition 30

A category ${\cal C}$ is locally cartesian closed (lccc) if it has a terminal object and if for all $\Gamma\in{\cal C}_{0}$, the slice category ${\cal C}/\Gamma$ is cartesian closed.

Again, this definition is in terms of property rather than structure. This is one of the two usual definitions of locally cartesian closed categories. Equivalently, one could ask ${\cal C}$ to have finite limits, and require that for all $\gamma:\Delta\to\Gamma$, the pullback functor $\gamma^{*}:{\cal C}/\Gamma\to{\cal C}/\Delta$, which associates to any $f:\cdot\to\Delta$ the left hand side morphism of the pullback diagram

[TABLE]

obtained via finite limits, has a right adjoint $\Pi_{\delta}:{\cal C}/\Delta\to{\cal C}/\Gamma$. It is this right adjoint that was proposed by Seely for the interpretation of $\Pi$-types.

As usual, this right adjoint to the pullback functor may be equivalently described as the data of cofree objects. Instantiated here, a right adjoint to $\gamma^{*}:{\cal C}/\Gamma\to{\cal C}/\Delta$ consists of, for all $\delta:\cdot\to\Delta$ an object of ${\cal C}/\Delta$, an object $\Pi_{\gamma}(\delta):\cdot\to\Gamma$ in ${\cal C}/\Gamma$ together with a co-unit $\epsilon_{\delta}:\gamma^{*}(\Pi_{\gamma}(\delta))\to\delta$ (a morphism in ${\cal C}/\Delta$) satisfying the universal property of co-free objects. These data, along with the universal property, amount to a dependent product diagram333It was pointed out by a reviewer that those were called “distributivity pullbacks” by Weber weber:

[TABLE]

which is universal among any such diagram over $\delta$ and $\gamma$, as described below.

[TABLE]

In other words, a locally cartesian closed category may be defined as a category ${\cal C}$ with finite limits such that, additionally, for every $\cdot\stackrel{{\scriptstyle\delta}}{{\to}}\Delta\stackrel{{\scriptstyle\gamma}}{{\to}}\Gamma$ in ${\cal C}$ there is a dependent product diagram as above. A locally cartesian closed functor may then be defined as a left exact functor (the image of a terminal object is terminal and the image of a pullback diagram is a pullback diagram) such that the image of a dependent product diagram is a dependent product diagram. There is a $2$-category $\mathbf{LCC}^{2}$ having small lcccs as objects, locally cartesian closed functors as $1$-cells, and natural transformations as $2$-cells.

Now we can build our biequivalence. First, we define a forgetful $2$-functor

[TABLE]

which omits all components and only keeps the base category, as in Section 5.2. We must prove that if ${\cal C}$ is the base category of a democratic cwf with $\mathrm{I}_{\mathrm{ext}}$-structure, $\Sigma$-structure and $\Pi$-structure, then ${\cal C}$ is locally cartesian closed. This is straightforward: using $\Pi$-types it is easy to show that for each $\Gamma$, $\mathrm{Ty}(\Gamma)$ is cartesian closed, but $\mathrm{Ty}(\Gamma)$ is equivalent to ${\cal C}/\Gamma$ as shown in Section 5.2. Alternatively one may construct dependent products: from $\cdot\stackrel{{\scriptstyle\delta}}{{\to}}\Delta\stackrel{{\scriptstyle\gamma}}{{\to}}\Gamma$ one may construct an isomorphic (in the obvious sense) sequence of projections via inverse image:

[TABLE]

For any such sequence of projections $\Gamma\cdot A\cdot B\to\Gamma\cdot A\to\Gamma$ there is a dependent product diagram, called the chosen dependent product diagram:

[TABLE]

where $\mathrm{\varepsilon}_{A,B}=\langle\mathrm{p},\mathrm{ap}(\mathrm{q},\mathrm{q}[\mathrm{p}])\rangle$. Combined with inverse image, this shows that any $\cdot\stackrel{{\scriptstyle\delta}}{{\to}}\Delta\stackrel{{\scriptstyle\gamma}}{{\to}}\Gamma$ has a dependent product diagram. Dependent product diagrams also permit a nice characterisation of the preservation of $\Pi$-structures:

Lemma 3

Let $F:{\cal C}\to{\cal D}$ be a pseudo cwf-morphism between cwfs with $\Pi$-structure. Then $F$ preserves the $\Pi$-structure if and only if the image of any chosen dependent product diagrams is a dependent product diagram.

Proof

Proved through intricate calculations – see ClairambaultD14, Proposition 4.8, for details.

This completes the definition of the forgetful $2$-functor ${\bf C}:\mathbf{Cwf}_{\mathrm{dem}}^{2,\mathrm{I}_{\mathrm{ext}},\Sigma,\Pi}\to\mathbf{LCC}^{2}$. In the other direction, the construction is the same as for Theorem 5.3; the fact that the pseudofunctor ${\bf L}$ yields pseudo cwf-morphisms preserving $\Pi$-structures follows from Lemma 3. We conclude:

Theorem 5.4

There is a biequivalence of $2$-categories $\mathbf{LCC}^{2}\simeq\mathbf{Cwf}_{\mathrm{dem}}^{2,\mathrm{I}_{\mathrm{ext}},\Sigma,\Pi}$.

Undecidability in the bifree locally cartesian closed category

The construction of a free cwf in Theorem 5.1 can easily be extended when we add $\mathrm{I}_{\mathrm{ext}},{\mathbb{N}_{1}},\Sigma$ and $\Pi$-types. This is done by adding the per-rules corresponding to formation, introduction, elimination, and equality rules for $\mathrm{I}_{\mathrm{ext}},{\mathbb{N}_{1}},\Sigma$ and $\Pi$. We do not have room for explicitly displaying those rules, but they can be found in Castellan, Clairambault, and Dybjer castellan:lmcs. We can thus construct a free cwf ${\cal T}^{\mathrm{I}_{\mathrm{ext}},{\mathbb{N}_{1}},\Sigma,\Pi,o}$ with $\mathrm{I}_{\mathrm{ext}},{\mathbb{N}_{1}},\Sigma$ and $\Pi$-type structures. It is both a free cwf (with the extra structure) on one base type and with respect to strict morphisms, and a bifree cwf (with the extra structure) on one base type and with respect to pseudo morphisms.

Theorem 5.5

The cwf ${\cal T}^{\mathrm{I}_{\mathrm{ext}},{\mathbb{N}_{1}},\Sigma,\Pi,o}$ is initial in the category $\mathbf{Cwf}^{\mathrm{I}_{\mathrm{ext}},{\mathbb{N}_{1}},\Sigma,\Pi,o}$, as well as bi-initial in the $2$-category $\mathbf{Cwf}^{2,\mathrm{I}_{\mathrm{ext}},{\mathbb{N}_{1}},\Sigma,\Pi,o}$. Moreover, it is democratic and bi-initial in $\mathbf{Cwf}_{\mathrm{dem}}^{2,\mathrm{I}_{\mathrm{ext}},\Sigma,\Pi,o}$.

Proof

Details appear in castellan:lmcs.

An object $I$ is bi-initial in a $2$-category iff for any $A$ there is an arrow $I\to A$ and for any two arrows $f,g:I\to A$ there exists a unique 2-cell $\theta:f\Rightarrow g$. It follows that $\theta$ is invertible, and that bi-initial objects are equivalent. In the statement above, $o$ denotes a base type. The objects of both $\mathbf{Cwf}^{\mathrm{I}_{\mathrm{ext}},{\mathbb{N}_{1}},\Sigma,\Pi,o}$ and $\mathbf{Cwf}^{2,\mathrm{I}_{\mathrm{ext}},{\mathbb{N}_{1}},\Sigma,\Pi,o}_{\mathrm{dem}}$ have a distinguished type $o\in\mathrm{Ty}(1)$, preserved on the nose for $\mathbf{Cwf}^{\mathrm{I}_{\mathrm{ext}},{\mathbb{N}_{1}},\Sigma,\Pi,o}$ and up to isomorphism for $\mathbf{Cwf}^{2,\mathrm{I}_{\mathrm{ext}},{\mathbb{N}_{1}},\Sigma,\Pi,o}_{\mathrm{dem}}$.

The presence of the base type $o$ does not affect the biequivalence in Theorem 5.4, which extends to a biequivalence $\mathbf{Cwf}^{2,\Sigma,\Pi,o}_{\mathrm{dem}}\simeq\mathbf{LCC}^{2,o}$ where the latter has a distinguished object $o\in{\cal C}_{0}$ preserved by functors up to isomorphism. As bi-initial objects are transported to bi-initial objects via a biequivalence, it follows from Theorem 5.5 that the base category of the cwf ${\cal T}^{\mathrm{I}_{\mathrm{ext}},{\mathbb{N}_{1}},\Sigma,\Pi,o}$ is bi-initial in $\mathbf{LCC}^{2,o}$:

Theorem 5.6

The base category of ${\cal T}^{\mathrm{I}_{\mathrm{ext}},{\mathbb{N}_{1}},\Sigma,\Pi,o}$ is the bifree lccc on one object.

Having constructed a bifree lccc, it is natural to consider its word problem: given two (syntactic) substitutions $\gamma,\gamma^{\prime}:\Delta\to\Gamma$ in ${\cal T}^{\mathrm{I}_{\mathrm{ext}},{\mathbb{N}_{1}},\Sigma,\Pi,o}$, is it decidable whether they are equal, or equivalently whether they have the same interpretation in any locally cartesian closed category? As $\gamma,\gamma^{\prime}$ are syntactic constructs in extensional type theory, one expects undecidability. However, prior undecidability proofs for extensional type theory rely on structure not available in our case. The folklore argument uses a universe and Hofmann’s undecidability proof hofmann:thesis uses a type of natural numbers.

In castellan:lmcs, we generalize the folklore result to hold with only one base type, i.e. in ${\cal T}^{\mathrm{I}_{\mathrm{ext}},{\mathbb{N}_{1}},\Sigma,\Pi,o}$, but without natural numbers or a universe. This relies on an encoding of combinatory logic in Martin-Löf type theory with $\mathrm{I}$-types, $\Pi$-types, and a base type $o$; as a context $\Gamma_{\mathsf{CL}}$ containing:

[TABLE]

where the left-associative binary infix symbol “$\cdot$” stands for application. While the above uses the syntax of type theory, it is easy to set up the same context just using the cwf combinators available in ${\cal T}^{\mathrm{I}_{\mathrm{ext}},{\mathbb{N}_{1}},\Sigma,\Pi,o}$, hence reducing the decision of equality between terms $M,N$ in combinatory logic to deciding

[TABLE]

e.g. an equality of two terms $M,N\in\mathrm{Tm}(\Gamma_{\mathsf{CL}},o)$. We conclude:

Theorem 5.7

Equality is undecidable in the bifree locally cartesian closed category on one base type.

Acknowledgements.

Pierre Clairambault was supported by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program “Investissements d’Avenir” (ANR-11-IDEX-0007) operated by the French National Research Agency (ANR). Peter Dybjer was supported by the Centre for Advanced Study at the Norwegian Academy of Science and Letters in Oslo, where he was a fellow in the Homotopy Type Theory and Univalent Foundations project while working on this paper. Finally, we would like to thank the anonymous reviewers for several useful suggestions.