Categories with Dependence and Semantics of Dependent Types

TL;DR

This paper introduces a generalized categorical framework called cartesian closed categories with dependence, providing a new semantics for dependent type theories that aligns with both categorical structures and syntactic precision.

Contribution

It extends cartesian closed categories to include dependence, supporting complex type structures like Sigma and Pi types in a strict categorical setting.

Findings

Developed a new categorical semantics for dependent type theories

Supported strict Sigma and Pi types in the new framework

Bridged categorical models with syntactic type theories

Abstract

The present paper gives a generalization of cartesian closed categories, called cartesian closed categories with dependence, whose strict version induces categories with families that support 1-, Sigma- and Pi-types in the strict sense. Consequently, we have obtained a new semantics of dependent type theories that is both categorical and true-to-syntax.

Equations

$$(\text{textsc}Ctx-Emp)\frac{}{⊢♢\mathsf{ctx}}(\text{textsc}Ctx-Ext)\frac{\mathsf{\Gamma }⊢\mathsf{A}\mathsf{type}\mathsf{x}\in \mathcal{V}\setminus \mathcal{FV}(\mathsf{\Gamma })}{⊢\mathsf{\Gamma },\mathsf{x}:\mathsf{A}\mathsf{ctx}}$$

$$(\text{textsc}Ctx-ExtEq)\frac{⊢\mathsf{\Gamma }=\mathsf{\Delta }\mathsf{ctx}\mathsf{\Gamma }⊢\mathsf{A}=\mathsf{B}\mathsf{type}\mathsf{x}\in \mathcal{V}\setminus \mathcal{FV}(\mathsf{\Gamma })\mathsf{y}\in \mathcal{V}\setminus \mathcal{FV}(\mathsf{\Delta })}{⊢\mathsf{\Gamma },\mathsf{x}:\mathsf{A}=\mathsf{\Delta },\mathsf{y}:\mathsf{B}\mathsf{ctx}}$$

$$(\text{textsc}Var)\frac{⊢{\mathsf{x}}_1:{\mathsf{A}}_1,{\mathsf{x}}_2:{\mathsf{A}}_2,\dots ,{\mathsf{x}}_{\mathsf{n}}:{\mathsf{A}}_{\mathsf{n}}\mathsf{ctx}j\in \{1,2,\dots ,n\}}{{\mathsf{x}}_1:{\mathsf{A}}_1,{\mathsf{x}}_2:{\mathsf{A}}_2,\dots ,{\mathsf{x}}_{\mathsf{n}}:{\mathsf{A}}_{\mathsf{n}}⊢{\mathsf{x}}_{\mathsf{j}}:{\mathsf{A}}_{\mathsf{j}}}(\text{textsc}Ct-EqRefl)\frac{⊢\mathsf{\Gamma }\mathsf{ctx}}{⊢\mathsf{\Gamma }=\mathsf{\Gamma }\mathsf{ctx}}$$

$$(\text{textsc}Ct-EqSym)\frac{⊢\mathsf{\Gamma }=\mathsf{\Delta }\mathsf{ctx}}{⊢\mathsf{\Delta }=\mathsf{\Gamma }\mathsf{ctx}}(\text{textsc}Ct-EqTrans)\frac{⊢\mathsf{\Gamma }=\mathsf{\Delta }\mathsf{ctx}⊢\mathsf{\Delta }=\mathsf{\Theta }\mathsf{ctx}}{⊢\mathsf{\Gamma }=\mathsf{\Theta }\mathsf{ctx}}$$

$$(\text{textsc}Ty-EqRefl)\frac{\mathsf{\Gamma }⊢\mathsf{A}\mathsf{type}}{\mathsf{\Gamma }⊢\mathsf{A}=\mathsf{A}\mathsf{type}}(\text{textsc}Ty-EqSym)\frac{\mathsf{\Gamma }⊢\mathsf{A}=\mathsf{B}\mathsf{type}}{\mathsf{\Gamma }⊢\mathsf{B}=\mathsf{A}\mathsf{type}}$$

$$(\text{textsc}Ty-EqTrans)\frac{\mathsf{\Gamma }⊢\mathsf{A}=\mathsf{B}\mathsf{type}\mathsf{\Gamma }⊢\mathsf{B}=\mathsf{C}\mathsf{type}}{\mathsf{\Gamma }⊢\mathsf{A}=\mathsf{C}\mathsf{type}}(\text{textsc}Tm-EqRefl)\frac{\mathsf{\Gamma }⊢\mathsf{a}:\mathsf{A}}{\mathsf{\Gamma }⊢\mathsf{a}=\mathsf{a}:\mathsf{A}}$$

$$(\text{textsc}Tm-EqSym)\frac{\mathsf{\Gamma }⊢\mathsf{a}={\mathsf{a}}^{\prime }:\mathsf{A}}{\mathsf{\Gamma }⊢{\mathsf{a}}^{\prime }=\mathsf{a}:\mathsf{A}}(\text{textsc}Tm-EqTrans)\frac{\mathsf{\Gamma }⊢\mathsf{a}={\mathsf{a}}^{\prime }:\mathsf{A}\mathsf{\Gamma }⊢{\mathsf{a}}^{\prime }={\mathsf{a}}^{\prime \prime }:\mathsf{A}}{\mathsf{\Gamma }⊢\mathsf{a}={\mathsf{a}}^{\prime \prime }:\mathsf{A}}$$

$$(\text{textsc}Ty-Con)\frac{⊢\mathsf{\Gamma }=\mathsf{\Delta }\mathsf{ctx}\mathsf{\Gamma }⊢\mathsf{A}\mathsf{type}}{\mathsf{\Delta }⊢\mathsf{A}\mathsf{type}}(\text{textsc}Tm-Con)\frac{\mathsf{\Gamma }⊢\mathsf{a}:\mathsf{A}⊢\mathsf{\Gamma }=\mathsf{\Delta }\mathsf{ctx}\mathsf{\Gamma }⊢\mathsf{A}=\mathsf{B}\mathsf{type}}{\mathsf{\Delta }⊢\mathsf{a}:\mathsf{B}}$$

$$(\text{textsc}Weak)\frac{\mathsf{\Gamma },\mathsf{\Delta }⊢\mathsf{J}\mathsf{\Gamma }⊢\mathsf{A}\mathsf{typ}{\mathsf{e}}_{\mathsf{i}}\mathsf{x}\in \mathcal{V}\setminus \mathcal{FV}(\mathsf{\Gamma },\mathsf{\Delta })}{\mathsf{\Gamma },\mathsf{x}:\mathsf{A},\mathsf{\Delta }⊢\mathsf{J}}$$

$$(\text{textsc}Subst)\frac{\mathsf{\Gamma },\mathsf{x}:\mathsf{A},\mathsf{\Delta }⊢\mathsf{J}\mathsf{\Gamma }⊢\mathsf{a}:\mathsf{A}}{\mathsf{\Gamma },\mathsf{\Delta }[a/x]⊢\mathsf{J}[a/x]}$$

$$\displaystyle(\textsc{$\mathsf{1}$-Form})\frac{\ \mathsf{\vdash\Gamma\ ctx}\ }{\ \mathsf{\Gamma\vdash 1\ type}\ }\ \ \ (\textsc{$\mathsf{1}$-Intro})\frac{\ \mathsf{\vdash\Gamma\ ctx}\ }{\ \mathsf{\Gamma\vdash\star:\bm{1}}\ }\ \ \ (\textsc{$\mathsf{1}$-Uniq})\frac{\ \mathsf{\Gamma\vdash t:1}\ }{\ \mathsf{\Gamma\vdash t=\star:1}\ }$$

$$\displaystyle(\textsc{$\mathsf{1}$-Elim})\frac{\ \mathsf{\Gamma,x:\bm{1}\vdash P\ type\ \ \ \Gamma\vdash p:P[\star/x]\ \ \ \Gamma\vdash t:\bm{1}}\ }{\ \mathsf{\Gamma\vdash R^{\bm{1}}(P,p,t):P[t/x]}\ }$$

$$\displaystyle(\textsc{$\mathsf{1}$-Comp})\frac{\ \mathsf{\Gamma,x:\bm{1}\vdash P\ type\ \ \ \Gamma\vdash p:P[\star/x]}\ }{\ \mathsf{\Gamma\vdash R^{\bm{1}}(P,p,\star)=p:P[\star/x]}\ }$$

$$\displaystyle(\textsc{$\mathsf{\Pi}$-Form})\frac{\ \mathsf{\Gamma\vdash A\ type}\ \ \ \mathsf{\Gamma,x:A\vdash B\ type}\ }{\ \mathsf{\Gamma\vdash\Pi_{x:A}B\ type}\ }\ \ \ (\textsc{$\mathsf{\Pi}$-Intro})\frac{\ \mathsf{\Gamma,x:A\vdash b:B}\ }{\ \mathsf{\Gamma\vdash\lambda x^{A}.b:\Pi_{x:A}B}\ }$$

$$\displaystyle(\textsc{$\Pi$-Elim})\frac{\ \mathsf{\Gamma\vdash f:\Pi_{x:A}B}\ \ \ \mathsf{\Gamma\vdash a:A}\ }{\ \mathsf{\Gamma\vdash f(a):B[a/x]}\ }\ \ \ (\textsc{$\mathsf{\Pi}$-Comp})\frac{\ \mathsf{\Gamma,x:A\vdash b:B}\ \ \ \mathsf{\Gamma\vdash a:A}\ }{\ \mathsf{\Gamma\vdash(\lambda x^{A}.b)(a)=b[a/x]:B[a/x]}\ }$$

$$\displaystyle(\textsc{$\mathsf{\Pi}$-Uniq})\frac{\ \mathsf{\Gamma\vdash f:\Pi_{x:A}B}\ \ \ \mathsf{x}\not\in\mathscr{FV}(\mathsf{\Gamma})\ }{\ \mathsf{\Gamma\vdash\lambda x^{A}.f(x)=f:\Pi_{x:A}B}\ }$$

$$\displaystyle(\textsc{$\mathsf{\Sigma}$-Form})\frac{\ \mathsf{\Gamma\vdash A\ type}\ \ \ \mathsf{\Gamma,x:A\vdash B\ type}\ }{\ \mathsf{\Gamma\vdash\Sigma_{x:A}B\ type}\ }$$

$$\displaystyle(\textsc{$\mathsf{\Sigma}$-Intro})\frac{\ \mathsf{\Gamma,x:A\vdash B\ type\ \ \ \Gamma\vdash a:A\ \ \ \Gamma\vdash b:B[a/x]}\ }{\ \mathsf{\Gamma\vdash\langle a,b\rangle:\Sigma_{x:A}B}\ }$$

$$\displaystyle(\textsc{$\mathsf{\Sigma}$-Elim})\frac{\ \mathsf{\Gamma,z:\Sigma_{x:A}B\vdash C\ type\ \ \ \Gamma,x:A,y:B\vdash g:C[\langle x,y\rangle/z]\ \ \ \Gamma\vdash p:\Sigma_{x:A}B}\ }{\ \mathsf{\Gamma\vdash R^{\Sigma}_{[z:\Sigma_{x:A}B]C}([x:A,y:B]g,p):C[p/z]}\ }$$

$$\displaystyle(\textsc{$\mathsf{\Sigma}$-Comp})\frac{\ \mathsf{\Gamma,z:\Sigma_{x:A}B\vdash C\ type\ \ \ \Gamma,x:A,y:B\vdash g:C[\langle x,y\rangle/z]\ \ \ \Gamma\vdash a:A\ \ \ \Gamma\vdash b:B[a/x]}\ }{\ \mathsf{\Gamma\vdash R^{\Sigma}_{[z:\Sigma_{x:A}B]C}([x:A,y:B]g,\langle a,b\rangle)=g[a/x,b/y]:C[\langle a,b\rangle/z]}\ }$$

$$\displaystyle(\textsc{$\mathsf{\Sigma}$-Uniq})\frac{\ \mathsf{\Gamma\vdash p:\Sigma_{x:A}B}\ }{\ \mathsf{\Gamma\vdash\langle\pi^{A,B}_{1}(p),\pi^{A,B}_{2}(p)\rangle=p:\Sigma_{x:A}B}\ }$$

$$\mathsf{\Gamma }⊢{\pi }_1^{\mathsf{A},\mathsf{B}}(\mathsf{p})\stackrel{df.}{\equiv }{\mathsf{R}}_{[\mathsf{z}:{\mathsf{\Sigma }}_{\mathsf{x}:\mathsf{A}}\mathsf{B}]\mathsf{A}}^{\mathsf{\Sigma }}([\mathsf{x}:\mathsf{A},\mathsf{y}:\mathsf{B}]\mathsf{x},\mathsf{p}):\mathsf{A};$$

$$\mathsf{\Gamma }⊢{\pi }_2^{\mathsf{A},\mathsf{B}}(\mathsf{p})\stackrel{df.}{\equiv }{\mathsf{R}}_{[\mathsf{z}:{\mathsf{\Sigma }}_{\mathsf{x}:\mathsf{A}}\mathsf{B}]\mathsf{B}[{\pi }_1^{\mathsf{A},\mathsf{B}}(\mathsf{z})/x]}^{\mathsf{\Sigma }}([\mathsf{x}:\mathsf{A},\mathsf{y}:\mathsf{B}]\mathsf{y},\mathsf{p}]):\mathsf{B}[{\pi }_1^{\mathsf{A},\mathsf{B}}(\mathsf{p})/x]$$

$$\mathsf{\Delta }$$

$$⋮$$

$$\mathsf{\Delta }$$

$$⋮$$

$$\mathsf{\Delta }$$

$$\mathsf{E}[{\mathsf{g}}_1/{\mathsf{x}}_1,{\mathsf{g}}_2/{\mathsf{x}}_2,\dots ,{\mathsf{g}}_{\mathsf{n}}/{\mathsf{x}}_{\mathsf{n}}]$$

$$\mathsf{g}\circ \mathsf{f}\stackrel{df.}{\equiv }({\mathsf{g}}_1[\mathsf{f}],{\mathsf{g}}_2[\mathsf{f}],\dots ,{\mathsf{g}}_{\mathsf{n}}[\mathsf{f}]).$$

$${id}_{\mathsf{\Gamma }}\stackrel{df.}{\equiv }({\mathsf{x}}_1,{\mathsf{x}}_2,\dots ,{\mathsf{x}}_{\mathsf{n}}):\mathsf{\Gamma }\to \mathsf{\Gamma }.$$

$$\text{textsc}(Type-Const)\frac{\mathsf{C}\in C_{\mathcal{T}}({\mathsf{A}}_1,{\mathsf{A}}_2,\dots ,{\mathsf{A}}_{\mathsf{k}})\mathsf{\Delta }\equiv {\mathsf{x}}_1:{\mathsf{A}}_1,{\mathsf{x}}_2:{\mathsf{A}}_2,\dots ,{\mathsf{x}}_{\mathsf{k}}:{\mathsf{A}}_{\mathsf{k}}\mathsf{f}:\mathsf{\Gamma }\to \mathsf{\Delta }}{\mathsf{\Gamma }⊢\mathsf{C}\mathsf{f}\mathsf{type}}$$

$$\text{textsc}(Term-Const)\frac{\mathsf{F}\in C_{\mathcal{T}}({\mathsf{A}}_1,{\mathsf{A}}_2,\dots ,{\mathsf{A}}_{\mathsf{k}};\mathsf{B})\mathsf{\Delta }\equiv {\mathsf{x}}_1:{\mathsf{A}}_1,{\mathsf{x}}_2:{\mathsf{A}}_2,\dots ,{\mathsf{x}}_{\mathsf{k}}:{\mathsf{A}}_{\mathsf{k}}\mathsf{f}:\mathsf{\Gamma }\to \mathsf{\Delta }\mathsf{\Delta }⊢\mathsf{B}\mathsf{type}}{\mathsf{\Gamma }⊢\mathsf{F}\mathsf{f}:\mathsf{B}[\mathsf{f}/{\mathsf{x}}_1,{\mathsf{x}}_2,\dots ,{\mathsf{x}}_{\mathsf{k}}]}$$

$$\text{textsc}(Type-Eq)\frac{\mathsf{\Delta }⊢\mathsf{A}\mathsf{type}\mathsf{\Delta }⊢{\mathsf{A}}^{\prime }\mathsf{type}\mathsf{f}:\mathsf{\Gamma }\to \mathsf{\Delta }\mathsf{A}={\mathsf{A}}^{\prime }:\mathsf{Ty}\in A_{\mathcal{T}}}{\mathsf{\Gamma }⊢\mathsf{A}[\mathsf{f}]={\mathsf{A}}^{\prime }[\mathsf{f}]\mathsf{type}}$$

$$\text{textsc}(Term-Eq)\frac{\mathsf{\Delta }⊢\mathsf{a}:\mathsf{A}\mathsf{\Delta }⊢{\mathsf{a}}^{\prime }:\mathsf{A}\mathsf{f}:\mathsf{\Gamma }\to \mathsf{\Delta }\mathsf{a}={\mathsf{a}}^{\prime }:\mathsf{A}\in A_{\mathcal{T}}}{\mathsf{\Gamma }⊢\mathsf{a}[\mathsf{f}]={\mathsf{a}}^{\prime }[\mathsf{f}]:\mathsf{A}[\mathsf{f}]}$$

$${\mathsf{R}}_{\mathsf{P}}^{\mathsf{N}}(\mathsf{x},{\mathsf{c}}_{\mathsf{z}},{\mathsf{c}}_{\mathsf{s}})[zero/y]={\mathsf{c}}_{\mathsf{z}}:\mathsf{P}[zero/y]$$

$${\mathsf{R}}_{\mathsf{P}}^{\mathsf{N}}(\mathsf{x},{\mathsf{c}}_{\mathsf{z}},{\mathsf{c}}_{\mathsf{s}})[\mathsf{succ}(\mathsf{y})/y]={\mathsf{c}}_{\mathsf{s}}({\mathsf{R}}_{\mathsf{P}}^{\mathsf{N}}(\mathsf{x},{\mathsf{c}}_{\mathsf{z}},{\mathsf{c}}_{\mathsf{s}})):\mathsf{P}[\mathsf{succ}(\mathsf{y})/y]$$

$$\mathsf{\Gamma }{⊢}_{\mathcal{N}}{\mathsf{R}}_{\mathsf{P}}^{\mathsf{N}}(\mathsf{x},{\mathsf{c}}_{\mathsf{z}},{\mathsf{c}}_{\mathsf{x}})[zero/y]={\mathsf{c}}_{\mathsf{z}}:\mathsf{P}[zero/y]$$

$$\mathsf{\Gamma },\mathsf{y}:\mathsf{N}{⊢}_{\mathcal{N}}{\mathsf{R}}_{\mathsf{P}}^{\mathsf{N}}(\mathsf{x},{\mathsf{c}}_{\mathsf{z}},{\mathsf{c}}_{\mathsf{x}})[\mathsf{succ}(\mathsf{y})/y]={\mathsf{c}}_{\mathsf{s}}({\mathsf{R}}_{\mathsf{P}}^{\mathsf{N}}(\mathsf{x},{\mathsf{c}}_{\mathsf{z}},{\mathsf{c}}_{\mathsf{s}})):\mathsf{P}[\mathsf{succ}(\mathsf{y})/y]$$

$${\mathsf{R}}_{\mathsf{P}}^{\mathsf{Id}}(\mathsf{x},\mathsf{p},\mathsf{w},\mathsf{w},\mathsf{ref}{\mathsf{l}}_{\mathsf{B}}(\mathsf{x},\mathsf{w}))=\mathsf{p}:\mathsf{P}[w/y,w/z,\mathsf{ref}{\mathsf{l}}_{\mathsf{B}}(\mathsf{x},\mathsf{w})/v]$$

Full text

As a main theorem, we prove that CCCwDs give a sound and complete interpretation of the ($\mathsf{1}$, $\mathsf{\Pi}$, $\mathsf{\Sigma}$)-fragment of Martin-Löf type theory (MLTT), a canonical representative of DTTs. Moreover, we establish a 2-equivalence between the 2-category of contextual (in a suitable sense similar to contextual categories by Cartmell) CCCwDs and the 2-category of MLTTs. In addition, we show that the 2-category of constant (in a suitable sense that abstractly captures simple types) contextual CCCwDs is 2-equivalent to the 2-category of contextual CCCs, which is well-known to be 2-equivalent to the 2-category of simply-typed $\lambda$-calculi equipped with $\mathsf{1}$- and $\mathsf{\times}$-types, a canonical representative of STTs. In this manner, we show that the categorical path from constant contextual CCCwDs to contextual CCCwDs corresponds to the syntactic path from STTs to DTTs, and also clarify its relation with the interpretation of STTs in CCCs.

As a ‘by-product’, fundamental concepts in category theory, e.g., categories, isomorphisms, functors, natural transformations, limits, adjoints, etc. are naturally generalized. Hence, the present work also sets out a general theory of ‘categories for dependence’.

1. 1 Introduction

2. 2 Preliminaries

3. 2.1 The Syntax of Martin-Löf Type Theories

4. 2.1.1 Contexts

5. 2.1.2 Structural Rules

6. 2.1.3 Unit Type

7. 2.1.4 Dependent Function Types

8. 2.1.5 Dependent Pair Types

9. 2.1.6 Context Morphisms and Generalized Substitution

10. 2.1.7 Martin-Löf Type Theories as Algebraic Theories

11. 2.1.8 Pre-Syntax

12. 2.1.9 Simply-Typed Lambda-Calculi as Sub-Theories

13. 2.2 Categories with Families

14. 2.2.1 Categories with Families

15. 2.2.2 Interpretation of MLTTs in CwFs

16. 2.2.3 Interpretation of STLCs in CCCs

17. 3 Categories with Dependence

18. 3.1 Categories and Functors with Dependence

19. 3.1.1 Categories with Dependence

20. 3.1.2 Functors with Dependence

21. 3.2 Semi-Cartesian Categories, Functors and Natural Transformations with Dependence

22. 3.2.1 Semi-Cartesian Categories with Dependence

23. 3.2.2 Semi-Cartesian Functors with Dependence

24. 3.2.3 Natural Transformations with Dependence

25. 3.2.4 The 2-Category of Semi-Cartesian Categories with Dependence

26. 3.2.5 Categories of Dependent Objects

27. 3.2.6 Isomorphisms between Dependent Objects

28. 3.3 Cartesian Categories and Functors with Dependence

29. 3.3.1 Cartesian Categories with Dependence

30. 3.3.2 Dependent Limits

31. 3.3.3 Cartesian Functors with Dependence

32. 3.3.4 The 2-Category of Cartesian Categories with Dependence

33. 3.4 Cartesian Closed Categories and Functors with Dependence

34. 3.4.1 Cartesian Closed Categories with Dependence

35. 3.4.2 Cartesian Closed Functors with Dependence

36. 3.4.3 The 2-Category of Cartesian Closed Categories with Dependence

37. 4 Equivalence between CtxCCCs and ConCtxCCCwDs

38. 4.1 Contextual Cartesian Closed Categories

39. 4.2 Contextual Cartesian Closed Categories with Dependence

40. 4.3 Equivalence between CtxCCCs and ConCtxCCCwDs

41. 5 Correspondence between MLTTs and CCCwDs

42. 5.1 Algebras for MLTTs

43. 5.2 Theory-Category Correspondence between MLTTs and CCCwDs

44. 6 Conclusion and Future Work

1 Introduction

In mathematics, category theory [ML13] studies algebra of morphisms, which originated from the work in algebraic topology by Samuel Eilenberg and Saunders Mac Lane in 1940s. Later, it has turned out to be extremely general, giving a synthetic formulation of various concepts in mathematics, physics, logic and computer science [BS10, MM12, Pie91, LS88].

In logic and computer science, type theories [Hin97, Pie02] refer to a particular kind of formal logical systems or programming languages, in which proofs or terms are always typed in contexts. Historically, the concept of types was first introduced to his theory of types by Bertrand Russell in 1900s to circumvent the well-known paradox in foundations of mathematics discovered by himself, and later types were also incorporated by Alonzo Church into his $\lambda$-calculus in 1940s to save it from another yet similar paradox, which led to type theories in their modern form.

An important concept in type theories is dependent types [Hof97], which are types that may contain free variables. A type theory is dependent if it has dependent types; otherwise it is (and its types are) simple. Under the Curry-Howard isomorphism [SU06], the generalization of simple type theories (STTs) to dependent type theories (DTTs) corresponds in logic to the path from propositional logic to predicate logic, where simple types and dependent types correspond to propositions and predicates, respectively. For concreteness, we focus on simply-typed $\lambda$-calculi (STLCs) [Chu40] and Martin-Löf type theories (MLTTs) [ML82, ML84, ML98] in this article for they are canonical representatives of STTs and DTTs, respectively.

Categorical logic [Pit01, Jac99, LS88] is the study of connections between categories and type theories. In categorical logic, syntax and semantics of type theories are both captured by categories with additional structures, and interpretations by functors preserving those structures. For syntax, such a categorical reformulation abstracts tedious syntactic formalisms (such as capture-free substitution) and enables one to focus on the abstract essence of type theories; also, neat categorical structures in a sense ‘justify’ the corresponding syntactic concepts. For semantics, on the other hand, categorical semantics provides a convenient framework to establish concrete semantics of type theories as in general it is simpler and subsumes more interpretations than the traditional set-theoretic semantics. Moreover, by theory-category correspondences [Pit01, Tay99], one may regard categories as a syntax-independent abstraction of type theories, or conversely, type theories as a symbolic presentation of (strict) categories.

Categorical semantics of STTs has been well-established, namely cartesian closed categories (CCCs) [Pit01, Jac99, LS88], but it is not quite the case for DTTs. More specifically, abstract semantics of DTTs is typically either:

Categorical yet indirect (in the sense that there is no counterpart of terms); or 2. 2.

Direct yet not categorical (often called algebraic or equational).

Note that CCCs are a categorical concept, and they give a direct semantics of STTs, in which terms are interpreted by morphisms.

$\blacktriangleright$ Remark.

Categorical concepts are usually defined in terms of universal properties, and thus they are weak, i.e., identified only up to isomorphisms, while type-theoretic concepts are strict, i.e., identified on-the-nose. Therefore, strictly speaking, one must employ strict structures to give a semantics of type theories; for instance, a fibred category has a substitution as a part of the structure [Jac99]. However, as long as a semantics employs the strict version of weak concepts, it would be fair to regard the semantics as categorical.

In fact, categorical semantics of DTTs has mathematical elegance, capturing type-theoretic phenomena in terms of categorical concepts, but usually they do not directly correspond to the syntax, having no counterpart of terms in particular. We regard this indirectness as a problem:

• $\blacktriangleright$

It would be difficult to say that indirect semantics faithfully captures DTTs since terms are a primitive concept that plays a central role in the syntax;

• $\blacktriangleright$

Direct semantics of DTTs would be interesting as an abstraction of type dependence as it is a natural and fundamental phenomenon which arises not only in DTTs but also in a variety of mathematical instances, e.g., see the set-theoretic example below; and

• $\blacktriangleright$

It is harder to work with indirect semantics of DTTs since intuition from the syntax is not directly applicable.

For instance, in locally cartesian closed categories (LCCCs) [See84] and categories with attributes (CwAs) [Car86, Mog91, Pit01], each term $\mathsf{\Gamma\vdash f:A}$ in a DTT is identified with the context morphism [Hof97, Pit01] $(\mathit{id}_{\mathsf{\Gamma}},\mathsf{f}):\mathsf{\Gamma}\to\mathsf{\Gamma,x:A}$ because there is no direct counterpart of terms in these frameworks. In the syntax, however, $\mathsf{f}$ and $(\mathit{id}_{\mathsf{\Gamma}},\mathsf{f})$ are not identified, and the former is clearly more primitive than the latter. In terms of the set-theoretic semantics, a context $\mathsf{\vdash\Gamma\ ctx}$, a type $\mathsf{\Gamma\vdash A\ type}$ and a term $\mathsf{\Gamma\vdash f:A}$ in a DTT should be, intuitively speaking, interpreted respectively as a set $\Gamma$, an indexed set $A=(A_{\gamma})_{\gamma\in\Gamma}$ and a function $f:\Gamma\to\bigcup_{\gamma\in\Gamma}A_{\gamma}$ such that $f(\gamma)\in A_{\gamma}$ for all $\gamma\in\Gamma$, but those categorical frameworks, specialized to the set-theoretic semantics, interpret the term $\mathsf{\Gamma\vdash f:A}$ as the function $\langle\mathit{id}_{\Gamma},f\rangle:(\gamma\in\Gamma)\mapsto(\gamma,f(\gamma))\in\Gamma\times\bigcup_{\gamma\in\Gamma}A_{\gamma}$. This point holds also for other categorical semantics of DTTs such as comprehension categories [Jac99], display map categories [Lam89, Tay87, HP89, Tay99] and indexed categories [Cur89, Obt89].

In contrast, algebraic semantics of DTTs such as categories with families (CwFs) [Dyb96, Hof97] is closer to the syntax, having a direct counterpart of terms, but it appears mathematically ad-hoc because it just employs an equational characterization that is not the strict version of weak concepts, i.e., it is not quite categorical. Indeed, this point is one of the main motivations for the recent work on natural models of homotopy type theory (NMs) [Awo16] by Awodey; it gives a categorical reformulation of CwFs. However, it seems difficult to take the resulting categorical structure as a generalization of CCCs; at least, its relation with the standard interpretation of STLCs in CCCs remains unclear. This point is unsatisfactory if one takes account of the rather simple relation between STTs and DTTs.

To summarize, we have not yet found a categorical and direct counterpart of the path from STTs to DTTs. We are concerned with such a counterpart for mathematical as well as practical points of view. From the mathematical standpoint, such a categorical structure is of interest in its own right because it would accurately capture the abstract essence of dependent types, which are a natural and fundamental concept not only in logic and computation but also (as we shall see) in many other mathematical instances, e.g., in sets as illustrated above.

From the practical viewpoint, a direct correspondence with the syntax would make it much more convenient as a tool to establish concrete semantics of DTTs since each semantic concept has a direct type-theoretic counterpart, which delivers useful intuition. If a direct semantics is in addition defined categorically, then in general it has fewer structures and axioms than an algebraic semantics so that it is simpler to verify that a concrete structure forms a semantics of DTTs through the former than the latter.

Motivated by these points, we introduce cartesian closed categories with dependence (CCCwDs) in order to capture DTTs in a mathematically natural as well as true-to-syntax fashion. Roughly, categories with dependence (CwDs) are categories equipped with direct counterparts of types and terms, called dependent (D-) objects and dependent (D-) morphisms, respectively, that satisfy certain axioms, where categories constitute a special case. A CwD is semi-cartesian if it has a terminal object and semi-dependent pair spaces (semi-$\Sigma$-spaces), which correspond respectively to the empty context and context extensions in DTTs. Let us note that strict semi-cartesian CwDs (SCCwDs) coincide with CwFs, and thus they are nothing new; our contribution is in defining a natural cartesian closed structure on SCCwDs. An SCCwD is cartesian if it has a unit D-object and dependent pair spaces ($\Sigma$-spaces), which are generalizations of a terminal object and binary products in the sense that they are defined in terms of universal properties that naturally generalize those of a terminal object and binary products, respectively; in fact, a unit D-object and $\Sigma$-spaces form instances of generalized limits, called dependent (D-) limits. An SCCwD is closed if it has dependent map spaces ($\Pi$-spaces), which are, similarly to $\Sigma$-spaces, a generalization of exponentials. As a mathematical ‘justification’ of these structures as a natural generalization of CCCs, we prove that unit D-objects, $\Sigma$- and $\Pi$-spaces satisfy certain expected properties, e.g., they are unique up to isomorphisms, $\Sigma$- and $\Pi$-spaces are respectively left and right adjoints to each other (up to projections), etc., and give several non-syntactic instances of CCCwDs.

We then show that CCCwDs give a sound and complete semantics of the ($\mathsf{1}$, $\mathsf{\Pi}$, $\mathsf{\Sigma}$)-fragment of MLTT. Moreover, we establish a 2-equivalence between the 2-category $\mathsf{Ctx}\mathbb{CCC_{D}}$ of contextual (in a suitable sense similar to contextual categories by Cartmell) CCCwDs (CtxCCCwDs) and the 2-category $\mathbb{MLTT}$ of MLTTs, which can be seen as a dependent version of the theory-category correspondence between STLCs and CCCs [Pit01, Cro93]. In addition, we verify that the 2-category $\mathsf{ConCtx}\mathbb{CCC_{D}}$ of constant (in a suitable sense that abstractly captures simple types) CtxCCCwDs is 2-equivalent to the 2-category $\mathsf{Ctx}\mathbb{CCC}$ of contextual CCCs (CtxCCCs). In this manner, we demonstrate that the categorical path from constant CtxCCCwDs to CtxCCCwDs corresponds to the syntactic path from STTs to DTTs, and also clarify its relation with the standard interpretation of STTs in CCCs. These results may be summarized schematically as: {diagram} where the conventional 2-equivalence between $\mathsf{Ctx}\mathbb{CCC}$ and the 2-category $\mathbb{STLC}$ of STLCs is recovered by composing the two 2-equivalences on the lower side in the diagram.

Notably, CCCwDs interpret MLTTs by giving rise to CwFs that support strict $1$-, $\Pi$- and $\Sigma$-types. This construction is rather canonical, and the term models of MLTTs form such CwFs via CtxCCCwDs; in this sense, CCCwDs are a refinement of CwFs. Also, constant CtxCCCwDs refine CtxCCCs for the former more faithfully captures STLCs than the latter.

Finally, as a ‘by-product’, fundamental concepts in category theory such as categories, isomorphisms, functors, natural transformations, limits and adjoints are naturally generalized. Thus, the present work also sets out a general theory of ‘categories of dependence’ though we mostly focus on what is relevant to the main results to keep the paper of a reasonable length, leaving a more thorough treatment as future work.

Related Work.

NMs by Awodey [Awo16] are another categorical and direct semantics of MLTTs, and thus most relevant to the present work. The mathematical structures of CCCwDs are, however, a priori very different from those of NMs, in particular the relation between NMs and CCCs is not immediately clear, though we leave a detailed comparison of the two as future work. Also, to the best of our knowledge, the theory-category correspondences between CtxCCCwDs and MLTTs as well as between constant CtxCCCwDs and CtxCCCs are new.

Plan of the Paper.

The rest of the paper proceeds as follows. We first review the syntax of MLTTs in Section 2.1 and the interpretation of MLTTs in CwFs in Section 2.2, where we also present the syntax of STLCs and the interpretation of them in CCCs. Then, we introduce CwDs and morphisms between them in Section 3.1, and SCCwDs and morphisms between them in Section 3.2. We then consider generalized terminal objects and binary products in SCCwDs and show that they interpret $\mathsf{1}$- and $\mathsf{\Sigma}$-types in Section 3.3, and we present generalized exponentials and prove that they interpret $\mathsf{\Pi}$-types in Section 3.4. Along with these developments, we give a basic theory of CwDs, generalizing some basic part of category theory. The next two sections are devoted to certain 2-equivalences: Section 4 establishes a 2-equivalence between $\mathsf{ConCtx}\mathbb{CCC_{D}}$ and $\mathsf{Ctx}\mathbb{CCC}$, and Section 5 gives a theory-category correspondence between MLTTs and CtxCCCwDs. Finally, Section 6 draws a conclusion and proposes future work.

2 Preliminaries

As a preparation, we review the syntax of MLTTs (in Section 2.1) and the interpretation of them in CwFs (in Section 2.2). If the reader is already familiar with these concepts, then she or he is encouraged to skip the present section and come back later in the ‘call-by-need’ fashion.

There are, however, mainly four reasons to present these concepts explicitly:

To define the term models (or the classifying CwFs) of MLTTs; 2. 2.

To show that strict CCCwDs are a refinement of CwFs that support $1$-, $\Sigma$- and $\Pi$-types; 3. 3.

To prove a theory-category correspondence between MLTTs and contextual CCCwDs; and 4. 4.

To explain a gap between the CCC- and CwF-semantics of STLCs.

2.1 The Syntax of Martin-Löf Type Theories

We first review the syntax of MLTTs, following the presentations of [Hof97, Pit01], and also present the syntax of STLCs as sub-theories of MLTTs. Note that we mainly focus on the syntax; see, e.g., [NPS90, ML84] for a general introduction to MLTTs.

A Martin-Löf type theory (MLTT) [ML75, ML84, ML98] is a formal logical system similar to natural deduction [Gen35, TS00] except that vertices of a derivation tree are judgements, for which we usually write $\mathcal{J}$ possibly with subscripts. There are the following six kinds of judgements (followed by their intended meanings):

• $\blacktriangleright$

$\mathsf{\vdash\Gamma\ ctx}$ ($\mathsf{\Gamma}$ is a context);

• $\blacktriangleright$

$\mathsf{\Gamma\vdash A\ type}$ ($\mathsf{A}$ is a type in the context $\mathsf{\Gamma}$);

• $\blacktriangleright$

$\mathsf{\Gamma\vdash a:A}$ ($\mathsf{a}$ is a term (or program) of type $\mathsf{A}$ in the context $\mathsf{\Gamma}$);

• $\blacktriangleright$

$\mathsf{\vdash\Gamma=\Delta\ ctx}$ ($\mathsf{\Gamma}$ and $\mathsf{\Delta}$ are (judgmentally) equal contexts);

• $\blacktriangleright$

$\mathsf{\Gamma\vdash A=B\ type}$ ($\mathsf{A}$ and $\mathsf{B}$ are (judgmentally) equal types in the context $\mathsf{\Gamma}$); and

• $\blacktriangleright$

$\mathsf{\Gamma\vdash a=a^{\prime}:A}$ ($\mathsf{a}$ and $\mathsf{a^{\prime}}$ are (judgmentally) equal terms of type $\mathsf{A}$ in the context $\mathsf{\Gamma}$).

That is, an MLTT consists of axioms $\frac{}{\ \mathcal{J}\ }$ and (inference) rules $\frac{\ \mathcal{J}_{1}\ \mathcal{J}_{2}\dots\mathcal{J}_{k}\ }{\mathcal{J}_{0}}$, which are to make a conclusion from hypotheses by constructing a derivation tree exactly as natural deduction does.

As often expressed as ‘an MLTT internalizes the Curry-Howard isomorphism [SU06]’, its contexts, types and terms represent respectively assumptions (or premises), formulas and proofs in logic as well. Therefore, e.g., the judgement $\mathsf{\Gamma\vdash a:A}$ can be read as ‘the formula $\mathsf{A}$ has a proof $\mathsf{a}$ under the assumption $\mathsf{\Gamma}$’, and so on.

$\blacktriangleright$ Convention.

We assume a countably infinite set $\mathscr{V}$ of variables, written $\mathsf{x}$, $\mathsf{y}$, $\mathsf{z}$, etc. possibly with subscripts. We write $\mathscr{FV}(\mathsf{E})$ for the set of all free variables occurring in an expression $\mathsf{E}$.

$\blacktriangleright$ Notation.

Greek capital letters $\mathsf{\Gamma}$, $\mathsf{\Delta}$, $\mathsf{\Theta}$, etc. range over contexts, capital letters A, B, C, etc. over types, and lower-case letters a, b, c, etc. over terms. Strictly speaking, they are equivalence classes of symbols with respect to $\alpha$-equivalence $\mathsf{\equiv}$ [Han94] as usual.

Each type construction in an MLTT is defined by its formation, introduction, elimination and computation rules. The formation rule stipulates how to form the type, and the introduction rule defines canonical terms of the type, which in turn defines terms of the type (including non-canonical ones). Then, the elimination and computation rules describe respectively how to consume terms of the type and the result of such a consumption (in the form of an equation), both of which are easily justified by the introduction rule.

Below, following the presentation of [Hof97], we first recall the MLTT with $\mathsf{1}$-, $\mathsf{\Pi}$- and $\mathsf{\Sigma}$-types in the strict sense, i.e., with uniqueness rules, for which we write $\mathsf{MLTT(1,\Pi,\Sigma)}$, in Sections 2.1.1-2.1.5. It is the minimal MLTT for us, and it corresponds to the dependently-typed version of the STLC equipped with $\mathsf{1}$- and $\mathsf{\times}$-types. We then introduce a general class of MLTTs based on the framework of dependently-typed algebraic theories [Pit01] (or generalized algebraic theories [Car86]) in Sections 2.1.6 and 2.1.7. Strictly speaking, this class is more general than what one usually considers as the class of MLTTs because additional types are not necessarily defined by the four kinds of rules mentioned above. We need this generality for the theory-category correspondence between the 2-categories of MLTTs and of contextual CCCwDs in Section 5.

2.1.1 Contexts

A context is a finite sequence $\mathsf{x_{1}:A_{1},x_{2}:A_{2},\dots,x_{n}:A_{n}}$ of pairs of a variable $\mathsf{x_{i}}$ and a type $\mathsf{A_{i}}$ such that the variables $\mathsf{x_{1},x_{2},\dots,x_{n}}$ are pair-wise distinct. We write $\mathsf{\diamondsuit}$ for the empty context, i.e., the empty sequence $\bm{\epsilon}$; we usually omit $\mathsf{\diamondsuit}$ when it occurs on the left-hand side of the turnstile $\vdash$.

We have the following axiom and rules for contexts:

[TABLE]

The rules Ctx-Emp and Ctx-Ext determine that contexts are exactly finite sequences of pairs of a variable and a type. The rule Ctx-ExtEq is a congruence rule, i.e., it states that judgmental equality is preserved under the rule Ctx-Ext, i.e., the ‘context extension’.

$\blacktriangleright$ Convention.

We will henceforth skip writing down congruence rules for other constructions.

2.1.2 Structural Rules

Next, we collect the inference rules for all types as structural rules:

[TABLE]

The rule Var states the reasonable idea that we may give an element $\mathsf{x_{j}:A_{j}}$ if it occurs in the context just by ‘copy-catting’ it. The next nine rules stipulate that every judgmental equality is an equivalence relation. The rules Ty-Conv and Tm-Conv formalize the idea that judgements should be preserved under the exchange of judgmentally equal contexts and/or types.

The following weakening and substitution rules are admissible (or derivable) in MLTTs, but it is convenient to present them explicitly:

[TABLE]

where $\mathsf{\mathsf{J}[a/x]}$ (resp. $\mathsf{\Delta[a/x]}$) denotes the capture-free substitution [Han94] of $\mathsf{a}$ for $\mathsf{x}$ in $\mathsf{J}$111Here, $\mathsf{J}$ denotes the righthand side of an arbitrary judgement. (resp. $\Delta$).

2.1.3 Unit Type

We proceed to introduce specific type constructions. Let us begin with the simplest type, called the unit type (or the $\bm{\mathsf{1}}$-type) $\mathsf{1}$ in the strict sense, which is the type that has just one canonical term $\mathsf{\star}$. Thus, from the logical point of view, it represents the simplest true formula.

Its rules are the following:

[TABLE]

The formation rule $\mathsf{1}$-Form states that $\mathsf{1}$ is an atomic type in the sense that we may form it without assuming any other types. The introduction rule $\mathsf{1}$-Intro defines that it has just one canonical term, viz., $\mathsf{\star}$. Thus, the uniqueness rule $\mathsf{1}$-Uniq should make sense, from which the remaining rules $\mathsf{1}$-Elim and $\mathsf{1}$-Comp immediately follow if we define $\mathsf{R^{1}(P,p,t)\stackrel{{\scriptstyle\mathrm{df.}}}{{\equiv}}p}$.

$\blacktriangleright$ Convention.

Thus, we henceforth omit the last two rules.

2.1.4 Dependent Function Types

Let us introduce a central non-atomic type construction, called dependent function types (or $\bm{\mathsf{\Pi}}$-types) in the strict sense. The $\mathsf{\Pi}$-type $\mathsf{\Pi_{x:A}B}$ is intended to represent the space of dependent functions from $\mathsf{A}$ to $\mathsf{B}$, and thus it is a generalization of the function type $\mathsf{A\Rightarrow B}$ in STLCs.

The rules of $\mathsf{\Pi}$-types are the following:

[TABLE]

$\blacktriangleright$ Notation.

We often omit the superscript $\mathsf{A}$ on $\mathsf{\lambda x^{A}.b}$ and write $\mathsf{A\Rightarrow B}$ for $\mathsf{\Pi_{x:A}B}$ if $\mathsf{x}\not\in\mathscr{FV}(\mathsf{B})$.

The formation rule $\mathsf{\Pi}$-Form states that we may form the $\mathsf{\Pi}$-type $\mathsf{\Pi_{x:A}B}$ from types $\mathsf{A}$ and $\mathsf{B}$, where $\mathsf{B}$ may depend on $\mathsf{A}$. The introduction rule $\mathsf{\Pi}$-Intro defines how to construct the canonical terms of $\mathsf{\Pi_{x:A}B}$, viz., $\lambda$-abstractions; it is the usual way of defining a function $\mathsf{f}$ from $\mathsf{A}$ to $\mathsf{B}$, i.e., to specify its output $\mathsf{f(a):B[a/x]}$ on each input $\mathsf{a:A}$. Then, the elimination and computation rules $\mathsf{\Pi}$-Elim and $\mathsf{\Pi}$-Comp should make sense by the introduction rule. Finally, the uniqueness rule $\mathsf{\Pi}$-Uniq stipulates that terms of $\mathsf{\Pi}$-types are only canonical ones.

2.1.5 Dependent Pair Types

Another important non-atomic type construction is dependent sum types (or $\bm{\mathsf{\Sigma}}$-types) in the strict sense. The $\mathsf{\Sigma}$-type $\mathsf{\Sigma_{x:A}B}$ represents the spaces of dependent pairs of $\mathsf{a:A}$ and $\mathsf{b:B[a/x]}$, and thus it is a generalization of the product type $\mathsf{A\times B}$ in STLCs.

The rules of $\mathsf{\Sigma}$-types are the following:

[TABLE]

where

[TABLE]

are projections constructed by $\mathsf{\Sigma}$-Elim.

$\blacktriangleright$ Notation.

We usually abbreviate $\mathsf{[z:\Sigma_{x:A}B]C}$, $\mathsf{[x:A,y:B]g}$ and $\mathsf{\pi^{A,B}_{i}(p)}$ respectively as $\mathsf{C}$, $\mathsf{g}$ and $\mathsf{\pi_{i}(p)}$ if it does not bring any confusion. We often write $\mathsf{A\times B}$ for $\mathsf{\Sigma_{x:A}B}$ if $\mathsf{x}\not\in\mathscr{FV}(\mathsf{B})$.

The formation rule $\mathsf{\Sigma}$-Form is the same as the case of $\mathsf{\Pi}$-types. The introduction rule $\mathsf{\Sigma}$-Intro specifies that canonical terms of a $\mathsf{\Sigma}$-type $\mathsf{\Sigma_{x:A}B}$ are pairs $\mathsf{\langle a,b\rangle:\Sigma_{x:A}B}$ of terms $\mathsf{a:A}$ and $\mathsf{b:B[a/x]}$; they are in particular dependent pairs for the type $\mathsf{B[a/x]}$ of the second component $\mathsf{b}$ depends on the first component $\mathsf{a:A}$. Again, the elimination and computation rules $\mathsf{\Sigma}$-Elim and $\mathsf{\Sigma}$-Comp should make sense by the introduction rule. Finally, the uniqueness rule $\mathsf{\Sigma}$-Uniq stipulates that terms of $\mathsf{\Sigma}$-types are only canonical ones, i.e., dependent pairs.

2.1.6 Context Morphisms and Generalized Substitution

We have presented the theory $\mathsf{MLTT(1,\Pi,\Sigma)}$. Next, let us review a derived concept in the syntax: A context morphism [Hof97, Pit01] from a context $\mathsf{\vdash\Delta\ ctx}$ to another $\mathsf{\vdash\Gamma\ ctx}$ such that $\mathscr{FV}(\mathsf{\Delta})\cap\mathscr{FV}(\mathsf{\Gamma})=\emptyset$, where we assume without loss of generality $\mathsf{\Gamma\equiv x_{1}:A_{1},x_{2}:A_{2},\dots,x_{n}:A_{n}\ ctx}$, is a finite sequence $\bm{\mathsf{g}}\equiv(\mathsf{g_{1}},\mathsf{g_{2}},\dots,\mathsf{g_{n}}):\mathsf{\Delta}\to\mathsf{\Gamma}$ of terms

[TABLE]

In addition, we say that parallel context morphisms $\mathsf{\bm{\mathsf{g,g^{\prime}}}:\Delta\to\Gamma}$ are (judgmentally) equal and write $\mathsf{\bm{\mathsf{g}}=\bm{\mathsf{g^{\prime}}}:\Delta\to\Gamma}$ if so are their corresponding component terms, i.e.,

[TABLE]

Given any syntactic expression $\mathsf{E}$, we define the generalized substitution $\mathsf{E}[\bm{\mathsf{g}}/\bm{\mathsf{x}}]$ of $\bm{\mathsf{g}}$ for $\bm{\mathsf{x}}$ in $\mathsf{E}$ (we often abbreviate it as $\mathsf{E}[\bm{\mathsf{g}}]$), where $\bm{\mathsf{x}}\equiv(\mathsf{x_{1}},\mathsf{x_{2}},\dots,\mathsf{x_{n}})$ and $\mathscr{FV}(\mathsf{E})\cap\mathscr{FV}(\bm{\mathsf{x}})=\emptyset$, to be the expression

[TABLE]

i.e., what is obtained from $\mathsf{E}$ by simultaneously substituting $\mathsf{g_{i}}$ for $\mathsf{x_{i}}$ in $\mathsf{E}$ for $i=1,2,\dots,n$. Then, it is shown in [Hof97] that if $\mathsf{\Gamma,\Theta\vdash E}$ is a judgement that is derivable in $\mathsf{MLTT(1,\Pi,\Sigma)}$, then so is the generalized substitution $\mathsf{\Delta,\Theta}[\bm{\mathsf{g}}]\vdash\mathsf{E}[\bm{\mathsf{g}}]$. Clearly, it subsumes the rules Weak and Subst.

Given another context morphism $\mathsf{\bm{\mathsf{f}}:\Theta\to\Delta}$, we define the composition $\mathsf{\bm{\mathsf{g}}\circ\bm{\mathsf{f}}:\Theta\to\Gamma}$ by:

[TABLE]

Also, we have the identity context morphism on $\mathsf{\vdash\Gamma\ ctx}$:

[TABLE]

It has been shown in [Hof97] that contexts and context morphisms derivable in $\mathsf{MLTT(1,\Pi,\Sigma)}$ modulo judgmental equality $=$ form a category. This suggests reformulating the derived notion of substitution as primitive, leading to the notion of CwFs in Section 2.2.

Note in particular that singleton lists of terms are context morphisms, but terms themselves are not. As we shall see in later sections, this point is captured by the CwF-semantics yet ignored by the CCC-semantics of STLCs.

2.1.7 Martin-Löf Type Theories as Algebraic Theories

Now, we are ready to present a general class of MLTTs, in which $\mathsf{MLTT(1,\Pi,\Sigma)}$ is the minimal theory. Our formulation is based on the framework of dependently-typed algebraic theories [Pit01] (or generalized algebraic theories [Car86]).

$\blacktriangleright$** Definition 2.1.1**** (GMLTTs).**

A generalized MLTT (GMLTT) is a quadruple $\mathcal{T}=(L_{\mathcal{T}},S_{\mathcal{T}},C_{\mathcal{T}},A_{\mathcal{T}})$, where:

• $\blacktriangleright$

$L_{\mathcal{T}}$ is a finite set of symbols, called the alphabet of $\mathcal{T}$, such that $L_{\mathcal{T}}\cap\mathscr{V}=\emptyset$ and it contains every non-variable symbol that occurs in a type or a term in $\mathsf{MLTT(1,\Pi,\Sigma)}$;

• $\blacktriangleright$

$S_{\mathcal{T}}$ is a subset of the set $(L_{\mathcal{T}}\cup\mathscr{V})^{\ast}$, whose elements are called sorts of $\mathcal{T}$;

• $\blacktriangleright$

$C_{\mathcal{T}}$ is a subset of the set $L_{\mathcal{T}}^{\ast}$, whose elements $\mathsf{C}$ are called constants of $\mathcal{T}$ and equipped with finite sequences $\mathscr{F}_{\mathcal{T}}(\mathsf{C})$ of the form $(\mathsf{A_{1}},\mathsf{A_{2}},\dots,\mathsf{A_{k}})\in S_{\mathcal{T}}^{\ast}$ or $((\mathsf{A_{1}},\mathsf{A_{2}},\dots,\mathsf{A_{k}}),\mathsf{B})\in S_{\mathcal{T}}^{\ast}\times S_{\mathcal{T}}$, called the format of $\mathsf{C}$; and

• $\blacktriangleright$

$A_{\mathcal{T}}$ is a set of judgements of the form $\mathsf{A=A^{\prime}:Ty}$ or $\mathsf{a=a^{\prime}:A}$, called axioms of $\mathcal{T}$, where $\mathsf{A},\mathsf{A^{\prime}}\in S_{\mathcal{T}}$ and $\mathsf{a},\mathsf{a^{\prime}}\in(L_{\mathcal{T}}\cup\mathscr{V})^{\ast}$.

$\blacktriangleright$ Convention.

Let $\mathcal{T}$ be a GMLTT. A constant $\mathsf{C}\in C_{\mathcal{T}}$ with a format of the form $(\mathsf{A_{1}}$, $\mathsf{A_{2}}$, …, $\mathsf{A_{k}})$ is particularly called a type-constant and written $\mathsf{C}\in C_{\mathcal{T}}(\mathsf{A_{1}}$, $\mathsf{A_{2}}$, …, $\mathsf{A_{k}})$. Similarly, a constant $\mathsf{F}\in C_{\mathcal{T}}$ with a format of the form $((\mathsf{A_{1}}$, $\mathsf{A_{2}}$, …, $\mathsf{A_{k}}),\mathsf{B})$ is particularly called a term-constant and written $\mathsf{F}\in C_{\mathcal{T}}(\mathsf{A_{1}}$, $\mathsf{A_{2}}$, …, $\mathsf{A_{k}};\mathsf{B})$; we also write $\mathscr{F}^{\mathit{dom}}_{\mathcal{T}}(\mathsf{F})$ for the sequence $(\mathsf{A_{1}}$, $\mathsf{A_{2}}$, …, $\mathsf{A_{k}})$ and $\mathscr{F}^{\mathit{cod}}_{\mathcal{T}}(\mathsf{F})$ for the sort $\mathsf{B}$. We write $C_{\mathcal{T}}^{\mathsf{Ty}}$ and $C_{\mathcal{T}}^{\mathsf{Tm}}$ for the set of all type-constants and the set of all term-constants in $\mathcal{T}$, respectively.

$\blacktriangleright$** Definition 2.1.2**** (Theorems of GMLTTs).**

Let $\mathcal{T}$ be a GMLTT. Contexts, types and terms in $\bm{\mathcal{T}}$ are judgements of the forms $\mathsf{\vdash\Gamma\ ctx}$, $\mathsf{\Gamma\vdash A\ type}$ and $\mathsf{\Gamma\vdash a:A}$, respectively, obtained by the axioms and rules in Sections 2.1.1-2.1.5 plus the following two rules:

[TABLE]

We define $\mathcal{T}(\mathsf{\Delta},\mathsf{\Gamma})$ to be the set of all context morphisms $\mathsf{\Delta}\to\mathsf{\Gamma}$ that consist of terms in $\mathcal{T}$, called context morphisms in $\bm{\mathcal{T}}$.

Equalities in $\bm{\mathcal{T}}$ are the judgements of the form $\mathsf{\vdash\Gamma=\Gamma^{\prime}\ ctx}$, $\mathsf{\Gamma\vdash A=A^{\prime}\ type}$ or $\mathsf{\Gamma\vdash a=a^{\prime}:A}$ obtained by the axioms and rules in Sections 2.1.1-2.1.5 plus the following two rules:

[TABLE]

Inhabited types and equalities in $\mathcal{T}$ are called theorems in $\bm{\mathcal{T}}$.

$\blacktriangleright$ Notation.

We write $\mathsf{\Gamma\vdash_{\mathcal{T}}J}$ to mean that the judgement $\mathsf{\Gamma\vdash J}$ is derivable in a GMLTT $\mathcal{T}$.

$\blacktriangleright$** Definition 2.1.3**** (Well-formed GMLTTs).**

A GMLTT $\mathcal{T}$ is well-formed if there is at least one rule to apply for each constant (resp. axiom) of $\mathcal{T}$.

Well-formedness of a GMLTT $\mathcal{T}$ virtually means that:

• $\blacktriangleright$

For each type-constant $\mathsf{C}\in C_{\mathcal{T}}(\mathsf{A_{1}},\mathsf{A_{2}},\dots,\mathsf{A_{k}})$, there is a context morphism $\bm{\mathsf{f}}:\mathsf{\Gamma}\to\mathsf{x_{1}:A_{1},x_{2}:A_{2},\dots,x_{k}:A_{k}}$ in $\mathcal{T}$;

• $\blacktriangleright$

For each term-constant $\mathsf{F}\in C_{\mathcal{T}}(\mathsf{A_{1}},\mathsf{A_{2}},\dots,\mathsf{A_{k}};\mathsf{B})$, there are a context morphism $\bm{\mathsf{f}}:\mathsf{\Gamma}\to\mathsf{x_{1}:A_{1},x_{2}:A_{2},\dots,x_{k}:A_{k}}$ in $\mathcal{T}$ and a type $\mathsf{x_{1}:A_{1},x_{2}:A_{2},\dots,x_{k}:A_{k}\vdash B\ type}$ in $\mathcal{T}$;

• $\blacktriangleright$

For each axiom of the form $\mathsf{A=A^{\prime}:Ty}\in A_{\mathcal{T}}$, there are a context morphism $\bm{\mathsf{f}}:\mathsf{\Gamma}\to\mathsf{\Delta}$ in $\mathcal{T}$ and types $\mathsf{\Delta\vdash A\ type}$ and $\mathsf{\Delta\vdash A^{\prime}\ type}$ in $\mathcal{T}$; and

• $\blacktriangleright$

For each axiom of the form $\mathsf{a=a^{\prime}:A}\in A_{\mathcal{T}}$, there are a context morphism $\bm{\mathsf{f}}:\mathsf{\Gamma}\to\mathsf{\Delta}$ in $\mathcal{T}$ and terms $\mathsf{\Delta\vdash a:A}$ and $\mathsf{\Delta\vdash a^{\prime}:A}$ in $\mathcal{T}$.

$\blacktriangleright$ Example 2.1.4.

Clearly, the minimal GMLTT $\Phi$ coincides with $\mathsf{MLTT(1,\Pi,\Sigma)}$.

$\blacktriangleright$ Example 2.1.5.

$\mathsf{MLTT(1,\Pi,\Sigma)}$ equipped with the natural number type $\mathsf{N}$, or $\mathsf{MLTT(1,\Pi,\Sigma,N)}$, can be presented as a well-formed GMLTT $\mathcal{N}$ such that:

• $\blacktriangleright$

$L_{\mathcal{N}}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}L_{\Phi}\cup\{\mathsf{N},\mathsf{zero},\mathsf{succ},\mathsf{R^{N}}\ \!\}$;

• $\blacktriangleright$

S_{\mathcal{N}}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\{\mathsf{A}\mid\mathsf{\Gamma\vdash_{\mathcal{N}}A\ type}\ \text{for some \mathsf{\vdash_{\mathcal{N}}\Gamma\ ctx}}\ \!\};

• $\blacktriangleright$

$C_{\mathcal{N}}$ contains the type-constant $\mathsf{N}\in C_{\mathcal{N}}(\bm{\epsilon})$ and the term-constants $\mathsf{zero}\in C_{\mathcal{N}}(\bm{\epsilon};\mathsf{N})$, $\mathsf{succ}\in C_{\mathcal{N}}(\mathsf{N};\mathsf{N})$ and $\mathsf{R^{N}_{P}}\in C_{\mathcal{N}}(\mathsf{A_{1}},\mathsf{A_{2}},\dots,\mathsf{A_{k}},\mathsf{P[zero/y]},\mathsf{P\Rightarrow P[succ(y)/y]};\mathsf{P})$ for each type of the form $\mathsf{x_{1}:A_{1},x_{2}:A_{2},\dots,x_{k}:A_{k},y:N\vdash_{\mathcal{N}}P\ type}$, where $\mathsf{R^{N}_{P}}$ is an abbreviation of $\mathsf{R^{N}(P)}$; and

• $\blacktriangleright$

$A_{\mathcal{N}}$ contains the equations

[TABLE]

for each triple of a type of the form $\mathsf{\Gamma,y:N\vdash_{\mathcal{N}}P\ type}$ and two terms of the forms $\mathsf{\Gamma\vdash_{\mathcal{N}}c_{z}:P[zero/y]}$ and $\mathsf{\Gamma,y:N\vdash_{\mathcal{N}}c_{s}:P\Rightarrow P[succ(y)/y]}$, where $\mathsf{\Gamma\equiv x_{1}:A_{1},x_{2}:A_{2},\dots,x_{k}:A_{k}}$ and $\bm{\mathsf{x}}\equiv\mathsf{x_{1},x_{2},\dots,x_{k}}$.

We may recover the conventional rules of $\mathsf{N}$-type as follows. Given a type $\mathsf{\Gamma,y:N\vdash_{\mathcal{N}}P\ type}$ and terms $\mathsf{\Gamma\vdash_{\mathcal{N}}c_{z}:P[zero/y]}$ and $\mathsf{\Gamma,y:N\vdash_{\mathcal{N}}c_{s}:P\Rightarrow P[succ(y)/y]}$, where $\mathsf{\Gamma\equiv x_{1}:A_{1},x_{2}:A_{2},\dots,x_{k}:A_{k}}$, we obtain $\mathsf{\Gamma\vdash_{\mathcal{N}}N\ type}$ by Type-Const, and $\mathsf{\Gamma\vdash_{\mathcal{N}}zero:N}$ and $\mathsf{\Gamma,y:N\vdash_{\mathcal{N}}succ(y):N}$ by Term-Const. Moreover, we get $\mathsf{\Gamma,y:N\vdash_{\mathcal{N}}c_{z}:P[zero/y]}$ by Weak, whence $\mathsf{\Gamma,y:N\vdash_{\mathcal{N}}R^{N}_{P}(\bm{\mathsf{x}},c_{z},c_{s}):P}$ by Term-Const, where $\bm{\mathsf{x}}\equiv\mathsf{x_{1}},\mathsf{x_{2}},\dots,\mathsf{x_{k}}$. Finally, we obtain the equations

[TABLE]

by Term-Eq.

$\blacktriangleright$ Example 2.1.6.

$\mathsf{MLTT(1,\Pi,\Sigma)}$ equipped with identity types $\mathsf{Id}$, or $\mathsf{MLTT(1,\Pi,\Sigma,Id)}$, can be presented as a well-formed GMLTT $\mathcal{I}$ such that:

• $\blacktriangleright$

$L_{\mathcal{I}}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}L_{\Phi}\cup\{\mathsf{Id},\mathsf{refl},\mathsf{R^{Id}}\ \!\}$;

• $\blacktriangleright$

S_{\mathcal{I}}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\{\mathsf{A}\mid\mathsf{\Gamma\vdash_{\mathcal{I}}A\ type}\ \text{for some \mathsf{\vdash_{\mathcal{I}}\Gamma\ ctx}}\ \!\};

• $\blacktriangleright$

$C_{\mathcal{I}}$ contains the type-constant $\mathsf{Id_{B}}\in C_{\mathcal{I}}(\mathsf{B},\mathsf{B})$ and the term-constants $\mathsf{refl_{B}}\in C_{\mathcal{I}}(\mathsf{A_{1}},\mathsf{A_{2}},\dots,\mathsf{A_{k}},\mathsf{B};\mathsf{Id_{B}(y,y)})$ and $\mathsf{R^{Id}_{P}}\in C_{\mathcal{I}}(\mathsf{A_{1}},\mathsf{A_{2}},\dots,\mathsf{A_{k}},\mathsf{P[w/y,w/z,refl_{B}(w)/v]},\mathsf{B},\mathsf{B},\mathsf{Id_{B}(y,z)};\mathsf{P})$ for each pair of types of the forms $\mathsf{\Gamma\vdash_{\mathcal{I}}B\ type}$ and $\mathsf{\Gamma,y:B,z:B,v:Id_{B}(y,z)\vdash_{\mathcal{I}}P\ type}$, where $\mathsf{\Gamma\equiv x_{1}:A_{1},x_{2}:A_{2},\dots,x_{k}:A_{k}}$, and $\mathsf{Id_{B}}$, $\mathsf{refl_{B}}$ and $\mathsf{R^{Id}_{P}}$ are abbreviations of $\mathsf{Id(B)}$, $\mathsf{refl(B)}$ and $\mathsf{R^{Id}(P)}$, respectively;

• $\blacktriangleright$

$A_{\mathcal{I}}$ contains the equation

[TABLE]

for each quadruple of types $\mathsf{\Gamma\vdash_{\mathcal{I}}B\ type}$ and $\mathsf{\Gamma,y:B,z:B,v:Id_{B}(y,z)\vdash_{\mathcal{I}}P\ type}$, and terms $\mathsf{\Gamma,w:B\vdash_{\mathcal{I}}p:P[w/y,w/z,refl_{B}(\bm{\mathsf{x}},w)/v]}$ and $\mathsf{\Gamma\vdash_{\mathcal{I}}b:B}$, where $\mathsf{\Gamma\equiv x_{1}:A_{1},x_{2}:A_{2},\dots,x_{k}:A_{k}}$ and $\bm{\mathsf{x}}\equiv\mathsf{x_{1}},\mathsf{x_{2}},\dots,\mathsf{x_{k}}$.

We may recover the conventional rules of $\mathsf{Id}$-types as follows. Given a type $\mathsf{\Gamma\vdash_{\mathcal{I}}B\ type}$ and terms $\mathsf{\Gamma\vdash_{\mathcal{I}}b:B}$ and $\mathsf{\Gamma\vdash_{\mathcal{I}}b^{\prime}:B}$, where $\mathsf{\Gamma\equiv x_{1}:A_{1},x_{2}:A_{2},\dots,x_{k}:A_{k}}$, we obtain the type $\mathsf{\Gamma\vdash_{\mathcal{I}}Id_{B}(b,b^{\prime})\ type}$ by Type-Const; also, we have $\mathsf{\Gamma,y:B\vdash_{\mathcal{I}}Id_{B}(y,y)\ type}$, whence we get the term $\mathsf{\Gamma\vdash_{\mathcal{I}}refl_{B}(\bm{\mathsf{x}},b):Id_{B}(b,b)}$ by Term-Const, where $\bm{\mathsf{x}}\equiv\mathsf{x_{1}},\mathsf{x_{2}},\dots,\mathsf{x_{k}}$. Moreover, given a type $\mathsf{\Gamma,y:B,z:B,v:Id_{B}(y,z)\vdash_{\mathcal{I}}P\ type}$ and terms $\mathsf{\Gamma,w:B\vdash_{\mathcal{I}}p:P[w/y,w/z,refl_{B}(\bm{\mathsf{x}},w)/v]}$ and $\mathsf{\Gamma\vdash_{\mathcal{I}}q:Id_{B}(b,b^{\prime})}$, we get the term $\mathsf{\Gamma,w:B\vdash_{\mathcal{I}}R^{Id}_{P}(\bm{\mathsf{x}},p,b,b^{\prime},q):P[b/y,b^{\prime}/z,q/v]}$ by Term-Const and the equality

[TABLE]

by Term-Eq.

$\blacktriangleright$ Convention.

Henceforth, we shall focus on well-formed GMLTTs and call them MLTTs.

2.1.8 Pre-Syntax

Contexts, types and terms in MLTTs have been given together with the judgement of typing. Alternatively, we may first give a larger class of (possibly non-valid) expressions by a simpler induction (on lengths of expressions), which should be called pre-contexts, pre-types and pre-terms, and then carve out the valid syntax as its subclass by the typing rules.

For certain purposes, pre-syntax is useful. For instance, the interpretation of MLTTs in CwFs is easier to give on pre-syntax than on syntax [Hof97, Pit01]. Following this method, we need pre-syntax in Section 5, and therefore we recall it here:

$\blacktriangleright$** Definition 2.1.7**** (Pre-syntax of MLTTs [Hof97]).**

The expressions called pre-contexts $\mathsf{\Gamma}$, pre-types $\mathsf{A}$, pre-terms $\mathsf{a}$ and pre-context morphisms $\bm{\mathsf{f}}$ in an MLTT $\mathcal{T}$ are given by the grammar:

[TABLE]

where $\mathsf{x}\in\mathscr{V}$, $\mathsf{C}\in C_{\mathcal{T}}^{\mathsf{Ty}}$ and $\mathsf{F}\in C_{\mathcal{T}}^{\mathsf{Tm}}$.

2.1.9 Simply-Typed Lambda-Calculi as Sub-Theories

Since we shall compare our semantics of simply-typed $\bm{\lambda}$-calculi (STLCs) with the standard CCC-semantics, we present them as sub-theories of MLTTs for a simple comparison of the two.

Let us first present the minimal STLC, which is equipped with finite product types $\mathsf{1}$ and $\mathsf{\times}$; it corresponds to the non-dependently-typed version of $\mathsf{MLTT(1,\Pi,\Sigma)}$, where $\mathsf{\Rightarrow}$- and $\mathsf{\times}$-types in the former correspond respectively to $\mathsf{\Pi}$- and $\mathsf{\Sigma}$-types in the latter. We call it the equational theory $\bm{\mathsf{\lambda^{=}_{1,\times}}}$. Roughly, the theory $\mathsf{\lambda^{=}_{1,\times}}$ is obtained from $\mathsf{MLTT(1,\Pi,\Sigma)}$ by restricting types to closed (i.e., with no free variables) ones and eliminating the rules for (judgmental) equalities between contexts and between types as there are only the trivial equalities (i.e., $\alpha$-equivalence).

Thus, it is a formal system to deduce the following judgements:

• $\blacktriangleright$

$\mathsf{\vdash\Gamma\ ctx}$ ($\mathsf{\Gamma}$ is a context);

• $\blacktriangleright$

$\mathsf{\vdash A\ type}$ ($\mathsf{A}$ is a (closed) type);

• $\blacktriangleright$

$\mathsf{\Gamma\vdash a:A}$ ($\mathsf{a}$ is a term of type $\mathsf{A}$ in the context $\mathsf{\Gamma}$); and

• $\blacktriangleright$

$\mathsf{\Gamma\vdash a=a^{\prime}:A}$ ($\mathsf{a}$ and $\mathsf{a^{\prime}}$ are equal terms of type $\mathsf{A}$ in the context $\mathsf{\Gamma}$).

Speifically, $\mathsf{\lambda^{=}_{1,\times}}$ consists of the following axioms and rules:

[TABLE]

where we again omit describing congruence rules. Following a standard convention, we write $\mathsf{A\Rightarrow B}$ and $\mathsf{A\times B}$ for $\mathsf{\Pi_{x:A}B}$ and $\mathsf{\Sigma_{x:A}B}$, respectively, since there are no dependent types in $\mathsf{\lambda^{=}_{1,\times}}$. Note that $\times$-Elim and $\times$-Comp are admissible in $\mathsf{MLTT(1,\Pi,\Sigma)}$ by $\Sigma$-Elim and $\Sigma$-Comp as described in [Hof97], and vice versa in $\mathsf{\lambda^{=}_{1,\times}}$; the other rules are just inherited from $\mathsf{MLTT(1,\Pi,\Sigma)}$.

It is easy to see that the theory $\mathsf{\lambda^{=}_{1,\times}}$ coincides with the standard equational (with respect to $\beta\eta$-equivalence) theory of the STLC equipped with finite product types [Cro93, Jac99, LS88].

Accordingly, the general class of STLCs is as follows:

$\blacktriangleright$** Definition 2.1.8**** (STLCs).**

An STLC is a quadruple $\mathcal{T}=(L_{\mathcal{T}},S_{\mathcal{T}},C_{\mathcal{T}},A_{\mathcal{T}})$, where:

• $\blacktriangleright$

$L_{\mathcal{T}}$ is a finite set of symbols, called the alphabet of $\mathcal{T}$, such that $L_{\mathcal{T}}\cap\mathscr{V}=\emptyset$ and it contains every non-variable symbol that occurs in a type or a term in $\mathsf{\lambda^{=}_{1,\times}}$;

• $\blacktriangleright$

$S_{\mathcal{T}}$ is a subset of the set $L_{\mathcal{T}}^{\ast}$, whose elements are called sorts of $\mathcal{T}$;

• $\blacktriangleright$

$C_{\mathcal{T}}$ is a subset of the set $L_{\mathcal{T}}^{\ast}$, whose elements $\mathsf{C}$ are called constants of $\mathcal{T}$ and equipped with finite sequences $\mathscr{F}_{\mathcal{T}}(\mathsf{C})$ of the form $\bm{\epsilon}\in S_{\mathcal{T}}^{\ast}$ or $((\mathsf{A_{1}},\mathsf{A_{2}},\dots,\mathsf{A_{k}}),\mathsf{B})\in S_{\mathcal{T}}^{\ast}\times S_{\mathcal{T}}$, called the format of $\mathsf{C}$; and

• $\blacktriangleright$

$A_{\mathcal{T}}$ is a set of judgements of the form $\mathsf{a=a^{\prime}:A}$, called axioms of $\mathcal{T}$, where $\mathsf{A}\in S_{\mathcal{T}}$ and $\mathsf{a},\mathsf{a^{\prime}}\in(L_{\mathcal{T}}\cup\mathscr{V})^{\ast}$

where the same convention is applied as in the case of MLTTs.

$\blacktriangleright$** Definition 2.1.9**** (Theorems of STLCs).**

Let $\mathcal{T}$ be an STLC. Contexts, types and terms in $\bm{\mathcal{T}}$ are judgements of the forms $\mathsf{\vdash\Gamma\ ctx}$, $\mathsf{\vdash A\ type}$ and $\mathsf{\vdash a:A}$, respectively, obtained by the axioms and rules given above in this section plus the following two rules:

[TABLE]

Equalities in $\bm{\mathcal{T}}$ are the judgements of the form $\mathsf{\Gamma\vdash a=a^{\prime}:A}$ obtained by the axioms and rules given above in this section plus the following rule:

[TABLE]

Inhabited types and equalities in $\mathcal{T}$ are also called theorems in $\bm{\mathcal{T}}$.

$\blacktriangleright$** Definition 2.1.10**** (Well-formed STLCs).**

An STLC $\mathcal{T}$ is well-formed if there is at least one rule to apply for each constant (resp. axiom) of $\mathcal{T}$.

$\blacktriangleright$ Convention.

We shall focus on well-formed STLCs and simply call them STLCs.

It is clear that STLCs are just the non-dependently-typed version of MLTTs, and our notion of STLCs coincides with the standard notion of (equational) STTs [LS88, Cro93, Pit01].

2.2 Categories with Families

Next, we review categories with families (CwFs) and their semantic type formers as well as the interpretation of $\mathsf{MLTT(1,\Pi,\Sigma)}$ in CwFs that support $1$-, $\Pi$- and $\Sigma$-types in the strict sense.

2.2.1 Categories with Families

$\blacktriangleright$** Definition 2.2.1**** (CwFs [Dyb96, Hof97]).**

A category with families (CwF) is a tuple

[TABLE]

where:

• $\blacktriangleright$

$\mathcal{C}$ is a category equipped with a specified terminal object $T\in\mathcal{C}$;

• $\blacktriangleright$

$\mathit{Ty}$ assigns, to each object $\Gamma\in\mathcal{C}$, a set $\mathit{Ty}(\Gamma)$, called the set of all types in the context $\Gamma$;

• $\blacktriangleright$

$\mathit{Tm}$ assigns, to each pair of an object $\Gamma\in\mathcal{C}$ and a type $A\in\mathit{Ty}(\Gamma)$, a set $\mathit{Tm}(\Gamma,A)$, called the set of all terms of type $A$ in the context $\Gamma$;

• $\blacktriangleright$

For each morphism $\phi:\Delta\to\Gamma$ in $\mathcal{C}$, $\_\{\_\}$ induces a function $\_\{\phi\}:\mathit{Ty}(\Gamma)\to\mathit{Ty}(\Delta)$, called the substitution on types, and a family $(\_\{\phi\}_{A}:\mathit{Tm}(\Gamma,A)\to\mathit{Tm}(\Delta,A\{\phi\}))_{A\in\mathit{Ty}(\Gamma)}$ of functions, called the substitutions on terms;

• $\blacktriangleright$

$\_.\_$ assigns, to each pair of a context $\Gamma\in\mathcal{C}$ and a type $A\in\mathit{Ty}(\Gamma)$, a context $\Gamma.A\in\mathcal{C}$, called the comprehension of $A$;

• $\blacktriangleright$

$\mathit{p}$ associates each pair of a context $\Gamma\in\mathcal{C}$ and a type $A\in\mathit{Ty}(\Gamma)$ with a morphism $\mathit{p}(A):\Gamma.A\to\Gamma$ in $\mathcal{C}$, called the first projection associated to $A$;

• $\blacktriangleright$

$\mathit{v}$ associates each pair of a context $\Gamma\in\mathcal{C}$ and a type $A\in\mathit{Ty}(\Gamma)$ with a term $\mathit{v}_{A}\in\mathit{Tm}(\Gamma.A,A\{\mathit{p}(A)\})$ called the second projection associated to $A$; and

• $\blacktriangleright$

$\langle\_,\_\rangle_{\_}$ assigns, to each triple of a morphism $\phi:\Delta\to\Gamma$ in $\mathcal{C}$, a type $A\in\mathit{Ty}(\Gamma)$ and a term $g\in\mathit{Tm}(\Delta,A\{\phi\})$, a morphism $\langle\phi,g\rangle_{A}:\Delta\to\Gamma.A$ in $\mathcal{C}$, called the extension of $\phi$ by $g$

that satisfies, for all $\Gamma,\Delta,\Theta\in\mathcal{C}$, $A\in\mathit{Ty}(\Gamma)$, $\phi:\Delta\to\Gamma$, $\varphi:\Theta\to\Delta$, $f\in\mathit{Tm}(\Gamma,A)$ and $g\in\mathit{Tm}(\Delta,A\{\phi\})$, the following equations:

• $\blacktriangleright$

(Ty-Id) $A\{\mathit{id}_{\Gamma}\}=A$;

• $\blacktriangleright$

(Ty-Comp) $A\{\phi\circ\varphi\}=A\{\phi\}\{\varphi\}$;

• $\blacktriangleright$

(Tm-Id) $f\{\mathit{id}_{\Gamma}\}_{A}=f$;

• $\blacktriangleright$

(Tm-Comp) $f\{\phi\circ\varphi\}_{A}=f\{\phi\}_{A}\{\varphi\}_{A\{\phi\}}$;

• $\blacktriangleright$

(Cons-L) $\mathit{p}(A)\circ\langle\phi,g\rangle_{A}=\phi$;

• $\blacktriangleright$

(Cons-R) $\mathit{v}_{A}\{\langle\phi,g\rangle_{A}\}_{A\{\mathit{p}(A)\}}=g$;

• $\blacktriangleright$

(Cons-Nat) $\langle\phi,g\rangle_{A}\circ\varphi=\langle\phi\circ\varphi,g\{\varphi\}_{A\{\phi\}}\rangle_{A}$;

• $\blacktriangleright$

(Cons-Id) $\langle\mathit{p}(A),\mathit{v}_{A}\rangle_{A}=\mathit{id}_{\Gamma.A}$.

$\blacktriangleright$ Notation.

We often omit the subscript $A$ in $\_\{\_\}_{A}$ and $\langle\_,\_\rangle_{A}$ if it does not cause any ambiguity.

CwFs are very close to the syntax, which is best described by the following term model:

$\blacktriangleright$** Definition 2.2.2**** (The term model $\mathcal{T}(1,\Pi,\Sigma)$ [Hof97]).**

The CwF of contexts and context morphisms of $\mathsf{MLTT(1,\Pi,\Sigma)}$ modulo $\mathsf{=}$, called the term model $\mathcal{T}(1,\Pi,\Sigma)$, is defined as follows:

• $\blacktriangleright$

The category $\mathcal{T}(1,\Pi,\Sigma)$ consists of contexts and context morphisms of $\mathsf{MLTT(1,\Pi,\Sigma)}$ as defined in Section 2.1 modulo (judgmental) equality $\mathsf{=}$. Let us write $[\mathsf{\Gamma}]$ (resp. $[\mathsf{A}]$, $[\mathsf{a}]$) for the equivalence class of a context $\mathsf{\vdash\Gamma\ ctx}$ (resp. a type $\mathsf{\Gamma\vdash A\ type}$, a term $\mathsf{\Gamma\vdash a:A}$).

• $\blacktriangleright$

Given $[\mathsf{\Gamma}]\in\mathcal{T}(1,\Pi,\Sigma)$, we define $\mathit{Ty}([\mathsf{\Gamma}])\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\{[\mathsf{A}]\ \!|\ \!\mathsf{\Gamma\vdash A\ type}\ \!\}$ and $\mathit{Tm}([\mathsf{\Gamma}],[\mathsf{A}])\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\{[\mathsf{a}]\ \!|\ \!\mathsf{\Gamma\vdash a:A}\ \!\}$. Below, we represent these equivalence classes by their arbitrary representatives.

• $\blacktriangleright$

The functions $\_\{\_\}$ are generalized substitutions $\_[\_]$ on types and terms in Section 2.1.

• $\blacktriangleright$

The terminal object is (the equivalence class of) the empty context $\mathsf{\vdash\diamondsuit\ ctx}$.

• $\blacktriangleright$

Given $\mathsf{\vdash\Gamma\ ctx}\in\mathcal{T}(1,\Pi,\Sigma)$ and $\mathsf{\Gamma\vdash A\ type}\in\mathit{Ty}(\mathsf{\Gamma})$, we define $\mathsf{\Gamma.A}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\mathsf{\vdash\Gamma,x:A\ ctx}$, where $\mathsf{x}\in\mathscr{V}\setminus\mathscr{FV}(\mathsf{\Gamma})$.

• $\blacktriangleright$

Assume $\mathsf{\vdash\Gamma=x_{1}:A_{1},x_{2}:A_{2},\dots,x_{n}:A_{n}\ ctx}$. Then, we define $\mathit{p}(\mathsf{A})\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\langle\mathsf{x_{1},x_{2},\dots,x_{n}}\rangle:\mathsf{\Gamma.A}\to\mathsf{\Gamma}$ and $\mathit{v}_{\mathsf{A}}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\mathsf{\Gamma,x:A\vdash x:A}\in\mathit{Tm}(\mathsf{\Gamma.A},\mathsf{A[\mathit{p}(A)]})$.

• $\blacktriangleright$

Given $\phi:\mathsf{\Delta}\to\mathsf{\Gamma}$ and $\mathsf{\Delta\vdash g:A[\phi]}\in\mathit{Tm}(\mathsf{\Gamma},\mathsf{A[\phi]})$, we define $\langle\phi,\mathsf{g}\rangle_{\mathsf{A}}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}(\phi,\mathsf{g}):\mathsf{\Gamma\to\Delta.A}$.

There are various non-syntactic instances of CwFs, e.g., sets [Hof97], groupoids [HS98] and games [AJV15, Yam17]. We skip describing these CwFs and leave the details to the references.

Nevertheless, CwFs model only the fragment of MLTTs that is common to all types; we need to equip them with semantic $1$-, $\Pi$- and $\Sigma$-type formers [Hof97] in order to model $\mathsf{MLTT(1,\Pi,\Sigma)}$.

$\blacktriangleright$** Definition 2.2.3**** (CwFs with $1$-type [Hof97]).**

A CwF $\mathcal{C}$ supports $\bm{1}$-type if:

• $\blacktriangleright$

(Unit-Form) For any $\Gamma\in\mathcal{C}$, there is a type $1_{\Gamma}\in\mathit{Ty}(\Gamma)$;

• $\blacktriangleright$

(Unit-Intro) For any $\Gamma\in\mathcal{C}$, there is a term $\star_{\Gamma}\in\mathit{Tm}(\Gamma,1_{\Gamma})$;

• $\blacktriangleright$

(Unit-Subst) For any morphism $\phi:\Delta\to\Gamma$ in $\mathcal{C}$, we have $1_{\Gamma}\{\phi\}=1_{\Delta}$; and

• $\blacktriangleright$

($\star$-Subst) For any morphism $\phi:\Delta\to\Gamma$ in $\mathcal{C}$, we have $\star_{\Gamma}\{\phi\}=\star_{\Delta}$.

It supports $1$-type in the strict sense if it additionally satisfies:

• $\blacktriangleright$

(Unit-Uniq) $f=\star_{\Gamma}$ for any $f\in\mathit{Tm}(\Gamma,1_{\Gamma})$.

$\blacktriangleright$** Definition 2.2.4**** (CwFs with $\Pi$-types [Hof97]).**

A CwF $\mathcal{C}$ supports $\bm{\Pi}$-types if:

• $\blacktriangleright$

($\Pi$-Form) For any $\Gamma\in\mathcal{C}$, $A\in\mathit{Ty}(\Gamma)$ and $B\in\mathit{Ty}(\Gamma.A)$, there is a type $\Pi(A,B)\in\mathit{Ty}(\Gamma)$;

• $\blacktriangleright$

($\Pi$-Intro) For any $f\in\mathit{Tm}(\Gamma.A,B)$, there is a term $\lambda_{A,B}(f)\in\mathit{Tm}(\Gamma,\Pi(A,B))$;

• $\blacktriangleright$

($\Pi$-Elim) For any $h\in\mathit{Tm}(\Gamma,\Pi(A,B))$ and $a\in\mathit{Tm}(\Gamma,A)$, there is a term $\mathit{App}_{A,B}(h,a)\in\mathit{Tm}(\Gamma,B\{\overline{a}\})$, where $\overline{a}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\langle\textit{id}_{\Gamma},a\rangle_{A}:\Gamma\to\Gamma.A$;

• $\blacktriangleright$

($\Pi$-Comp) We have $\mathit{App}_{A,B}(\lambda_{A,B}(f),a)=f\{\overline{a}\}$;

• $\blacktriangleright$

($\Pi$-Subst) For any $\Delta\in\mathcal{C}$ and $\phi:\Delta\to\Gamma$ in $\mathcal{C}$, we have $\Pi(A,B)\{\phi\}=\Pi(A\{\phi\},B\{\phi^{+}\}$, where $\phi^{+}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\langle\phi\circ\mathit{p}(A\{\phi\}),\mathit{v}_{A\{\phi\}}\rangle_{A}:\Delta.A\{\phi\}\to\Gamma.A$;

• $\blacktriangleright$

($\lambda$-Subst) For any $g\in\mathit{Tm}(\Gamma.A,B)$, we have $\lambda_{A,B}(g)\{\phi\}=\lambda_{A\{\phi\},B\{\phi^{+}\}}(g\{\phi^{+}\})$; and

• $\blacktriangleright$

(App-Subst) We have $\mathit{App}_{A,B}(h,a)\{\phi\}=\mathit{App}_{A\{\phi\},B\{\phi^{+}\}}(h\{\phi\},a\{\phi\})$.

It supports $\Pi$-types in the strict sense if it additionally satisfies:

• $\blacktriangleright$

($\lambda$-Uniq) $\lambda_{A,B}(\mathit{App}_{A\{\mathit{p}(A)\},B\{\mathit{p}(A)^{+}\}}(k,\mathit{v}_{A}))\{\mathit{p}(A)\}=k$ for any $k\in\mathit{Tm}(\Gamma.A,\Pi(A,B)\{\mathit{p}(A)\})$.

$\blacktriangleright$** Definition 2.2.5**** (CwFs with $\Sigma$-types [Hof97]).**

A CwF $\mathcal{C}$ supports $\bm{\Sigma}$-types if:

• $\blacktriangleright$

($\Sigma$-Form) For any $\Gamma\in\mathcal{C}$, $A\in\mathit{Ty}(\Gamma)$ and $B\in\mathit{Ty}(\Gamma.A)$, there is a type $\Sigma(A,B)\in\mathit{Ty}(\Gamma)$;

• $\blacktriangleright$

($\Sigma$-Intro) There is a morphism $\mathit{Pair}_{A,B}:\Gamma.A.B\to\Gamma.\Sigma(A,B)$ in $\mathcal{C}$;

• $\blacktriangleright$

($\Sigma$-Elim) Given $P\in\mathit{Ty}(\Gamma.\Sigma(A,B))$ and $f\in\mathit{Tm}(\Gamma.A.B,P\{\mathit{Pair}_{A,B}\})$, there is a term $\mathcal{R}^{\Sigma}_{A,B,P}(f)\in\mathit{Tm}(\Gamma.\Sigma(A,B),P)$;

• $\blacktriangleright$

($\Sigma$-Comp) $\mathcal{R}^{\Sigma}_{A,B,P}(f)\{\mathit{Pair}_{A,B}\}=f$;

• $\blacktriangleright$

($\Sigma$-Subst) For any $\Delta\in\mathcal{C}$ and $\phi:\Delta\to\Gamma$ in $\mathcal{C}$, $\Sigma(A,B)\{\phi\}=\Sigma(A\{\phi\},B\{\phi^{+}\})$;

• $\blacktriangleright$

(Pair-Subst) $\mathit{p}(\Sigma(A,B))\circ\mathit{Pair}_{A,B}=\mathit{p}(A)\circ\mathit{p}(B)$, $\phi^{\star}\circ\mathit{Pair}_{A\{\phi\},B\{\phi^{+}\}}=\mathit{Pair}_{A,B}\circ\phi^{++}$, where $\phi^{\star}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\langle\phi\circ\mathit{p}(\Sigma(A,B)\{\phi\}),\mathit{v}_{\Sigma(A,B)\{\phi\}}\rangle_{\Sigma(A,B)}:\Delta.\Sigma(A,B)\{\phi\}\to\Gamma.\Sigma(A,B)$, $\phi^{++}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\langle\phi^{+}\circ\mathit{p}(B\{\phi^{+}\}),\mathit{v}_{B\{\phi^{+}\}}\rangle_{B}:\Delta.A\{\phi\}.B\{\phi^{+}\}\to\Gamma.A.B$; and

• $\blacktriangleright$

($\mathcal{R}^{\Sigma}$-Subst) $\mathcal{R}^{\Sigma}_{A,B,P}(f)\{\phi^{\star}\}=\mathcal{R}^{\Sigma}_{A\{\phi\},B\{\phi^{+}\},P\{\phi^{\star}\}}(f\{\phi^{++}\})$.

It supports $\Sigma$-types in the strict sense if it satisfies:

• $\blacktriangleright$

($\mathcal{R}^{\Sigma}$-Uniq) $g=\mathcal{R}^{\Sigma}_{A,B,P}(f)$ for any $g\in\mathit{Tm}(\Gamma.\Sigma(A,B),P)$ such that $g\{\mathit{Pair}_{A,B}\}=f$.

In light of Definition 2.2.2, it is straightforward to see what these semantic type formers in the term model $\mathcal{T}(1,\Pi,\Sigma)$ are; thus, we leave their details to [Hof97].

$\blacktriangleright$** Proposition 2.2.6**** (Well-defined $\mathcal{T}(1,\Pi,\Sigma)$ [Hof97]).**

The term model $\mathcal{T}(1,\Pi,\Sigma)$ is a well-defined CwF that supports $1$-, $\Pi$- and $\Sigma$-types in the strict sense.

Now, one may see clearly why CwFs equipped with those semantic type formers are not categorical: They are not a strict version of some weak concepts defined by universal properties. The work [Awo16] by Awodey is an attempt to address this point.

2.2.2 Interpretation of MLTTs in CwFs

Now, let us recall the interpretation of $\mathsf{MLTT(1,\Pi,\Sigma)}$ in CwFs that support $1$-, $\Pi$-, $\Sigma$-types in the strict sense [Hof97]. Since a deduction tree of a judgement in $\mathsf{MLTT(1,\Pi,\Sigma)}$ is not necessarily unique in the presence of the rules Ty-Con and Tm-Con, a priori we cannot define an interpretation by induction on deduction trees. For this point, a standard approach is to define an interpretation $\llbracket\_\rrbracket$ on pre-syntax by induction on the lengths of expressions, which is partial, and show that it is total and well-defined on every valid or well-typed syntax (i.e., judgement) and preserves judgmental equality as the corresponding semantic equality [Str12, Hof97, Pit01].

By this soundness result, a posteriori we may describe the interpretation $\llbracket\_\rrbracket$ of the syntax by induction on derivation trees of judgements:

$\blacktriangleright$** Definition 2.2.7**** (Interpretation of $\mathsf{MLTT(1,\Pi,\Sigma)}$ in CwFs [Hof97]).**

The interpretation $\llbracket\_\rrbracket$ of $\mathsf{MLTT(1,\Pi,\Sigma)}$ in a CwF $\mathcal{C}=(\mathcal{C},\mathit{Ty},\mathit{Tm},\_\{\_\},T,\_.\_,\mathit{p},\mathit{v},\langle\_,\_\rangle_{\_})$ that supports semantic type formers $1=(1,\star)$, $\Pi=(\Pi,\lambda,\mathit{App})$, $\Sigma=(\Sigma,\mathit{Pair},R^{\Sigma})$ in the strict sense is defined as follows:

• $\blacktriangleright$

(Ct-Emp) $\llbracket\mathsf{\vdash\diamondsuit\ ctx}\rrbracket\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}T$;

• $\blacktriangleright$

(Ct-Ext) $\llbracket\mathsf{\vdash\Gamma,x:A\ ctx}\rrbracket\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\llbracket\mathsf{\vdash\Gamma\ ctx}\rrbracket.\llbracket\mathsf{\Gamma\vdash A\ type}\rrbracket$;

• $\blacktriangleright$

($\mathsf{1}$-Form) $\llbracket\mathsf{\Gamma\vdash\mathsf{1}\ type}\rrbracket\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}1_{\llbracket\mathsf{\Gamma}\rrbracket}$;

• $\blacktriangleright$

($\Pi$-Form) $\llbracket\mathsf{\Gamma\vdash\Pi_{x:A}B\ type}\rrbracket\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\Pi(\llbracket\mathsf{\Gamma\vdash A\ type}\rrbracket,\llbracket\mathsf{\Gamma,x:A\vdash B\ type}\rrbracket)$;

• $\blacktriangleright$

($\Sigma$-Form) $\llbracket\mathsf{\Gamma\vdash\Sigma_{x:A}B\ type}\rrbracket\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\Sigma(\llbracket\mathsf{\Gamma\vdash A\ type}\rrbracket,\llbracket\mathsf{\Gamma,x:A\vdash B\ type}\rrbracket)$;

• $\blacktriangleright$

(Var) $\llbracket\mathsf{\Gamma,x:A\vdash x:A}\rrbracket\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\mathit{v}_{\llbracket\mathsf{A}\rrbracket}$, $\llbracket\mathsf{\Gamma,x:A,\Delta,y:B\vdash x:A}\rrbracket\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\llbracket\mathsf{\Gamma,x:A,\Delta\vdash x:A}\rrbracket\{\mathit{p}(\llbracket\mathsf{\Gamma,x:A,\Delta\vdash B\ type}\rrbracket)\}$;

• $\blacktriangleright$

(Ty-Con) $\llbracket\mathsf{\Delta\vdash A\ type}\rrbracket\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\llbracket\mathsf{\Gamma\vdash A\ type}\rrbracket$;

• $\blacktriangleright$

(Tm-Con) $\llbracket\mathsf{\Delta\vdash a:B}\rrbracket\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\llbracket\mathsf{\Gamma\vdash a:A}\rrbracket$;

• $\blacktriangleright$

($\mathsf{1}$-Intro) $\llbracket\mathsf{\Gamma\vdash\star:\mathsf{1}}\rrbracket\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\star_{\llbracket\mathsf{\Gamma}\rrbracket}$;

• $\blacktriangleright$

($\Pi$-Intro) $\llbracket\mathsf{\Gamma\vdash\lambda x.\ \!b:\Pi_{x:A}B}\rrbracket\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\lambda_{\llbracket\mathsf{A}\rrbracket,\llbracket\mathsf{B}\rrbracket}(\llbracket\mathsf{\Gamma,x:A\vdash b:B}\rrbracket)$;

• $\blacktriangleright$

($\Sigma$-Intro) $\llbracket\mathsf{\Gamma\vdash(a,b):\Sigma_{x:A}B}\rrbracket\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\mathit{Pair}_{\llbracket\mathsf{A}\rrbracket,\llbracket\mathsf{B}\rrbracket}\circ\langle\overline{\llbracket\mathsf{\Gamma\vdash a:A}\rrbracket},\llbracket\mathsf{\Gamma\vdash b:B[a/x]\rrbracket}\rangle$;

• $\blacktriangleright$

($\Pi$-Elim) $\llbracket\mathsf{\Gamma\vdash f(a):B[a/x]}\rrbracket\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\mathit{App}_{\llbracket\mathsf{A}\rrbracket,\llbracket\mathsf{B}\rrbracket}(\llbracket\mathsf{\Gamma\vdash f:\Pi_{x:A}B}\rrbracket,\llbracket\mathsf{\Gamma\vdash a:A}\rrbracket\rangle)$; and

• $\blacktriangleright$

($\Sigma$-Elim) $\llbracket\mathsf{\Gamma\vdash R^{\Sigma}(C,g,p):C[p/z]}\rrbracket\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}R^{\Sigma}_{\llbracket\mathsf{A}\rrbracket,\llbracket\mathsf{B}\rrbracket,\llbracket\mathsf{C}\rrbracket}(\llbracket\mathsf{\Gamma,x:A,y:B\vdash g:C[(x,y)/z]}\rrbracket)\circ\overline{\llbracket\mathsf{\Gamma\vdash p:\Sigma_{x:A}B}\rrbracket}$

where the hypotheses of the rules are as presented in Section 2.1, $\overline{\llbracket\mathsf{\Gamma\vdash a:A}\rrbracket}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\langle\mathit{id}_{\llbracket\mathsf{\Gamma}\rrbracket},\llbracket\mathsf{a}\rrbracket\rangle:\llbracket\mathsf{\Gamma}\rrbracket\to\llbracket\mathsf{\Gamma}\rrbracket.\llbracket\mathsf{A}\rrbracket$ and $\overline{\llbracket\mathsf{\Gamma\vdash p:\Sigma_{x:A}B}\rrbracket}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\langle\mathit{id}_{\llbracket\mathsf{\Gamma}\rrbracket},\llbracket\mathsf{p}\rrbracket\rangle:\llbracket\mathsf{\Gamma}\rrbracket\to\llbracket\mathsf{\Gamma}\rrbracket.\llbracket\mathsf{\Sigma_{x:A}B}\rrbracket$.

$\blacktriangleright$** Theorem 2.2.8**** (Soundness of CwFs [Hof97]).**

If $\mathsf{\vdash\Gamma=\Gamma^{\prime}\ ctx}$ (resp. $\mathsf{\Gamma\vdash A=A^{\prime}\ type}$, $\mathsf{\Gamma\vdash a=a^{\prime}:A}$) in $\mathsf{MLTT(1,\Pi,\Sigma)}$, then $\llbracket\mathsf{\Gamma}\rrbracket=\llbracket\mathsf{\Gamma^{\prime}}\rrbracket$ (resp. $\llbracket\mathsf{A}\rrbracket=\llbracket\mathsf{A^{\prime}}\rrbracket$, $\llbracket\mathsf{a}\rrbracket=\llbracket\mathsf{a^{\prime}}\rrbracket$) for the interpretation $\llbracket\_\rrbracket$ of $\mathsf{MLTT(1,\Pi,\Sigma)}$ in any CwF that supports $1$-, $\Pi$- and $\Sigma$-types in the strict sense.

By Proposition 2.2.6, this interpretation is also complete:

$\blacktriangleright$** Theorem 2.2.9**** (Completeness of CwFs [Hof97]).**

Given $\mathsf{\vdash\Gamma\ ctx}$ and $\mathsf{\vdash\Delta\ ctx}$ (resp. $\mathsf{\Gamma\vdash A\ type}$ and $\mathsf{\Gamma\vdash B\ type}$, $\mathsf{\Gamma\vdash a:A}$ and $\mathsf{\Gamma\vdash a^{\prime}:A}$) in $\mathsf{MLTT(1,\Pi,\Sigma)}$, if $\llbracket\mathsf{\Gamma}\rrbracket=\llbracket\mathsf{\Delta}\rrbracket$ (resp. $\llbracket\mathsf{A}\rrbracket=\llbracket\mathsf{B}\rrbracket$, $\llbracket\mathsf{a}\rrbracket=\llbracket\mathsf{a^{\prime}}\rrbracket$) for the interpretation $\llbracket\_\rrbracket$ in any CwF that supports $1$-, $\Sigma$- and $\Pi$-types in the strict sense, then there is a judgement $\mathsf{\vdash\Gamma=\Delta\ ctx}$ (resp. $\mathsf{\Gamma\vdash A=B\ type}$, $\mathsf{\Gamma\vdash a=a^{\prime}:A}$) in $\mathsf{MLTT(1,\Pi,\Sigma)}$.

For $\mathsf{\lambda^{=}_{1,\times}}$ is a sub-theory of $\mathsf{MLTT(1,\Pi,\Sigma)}$, any CwF that supports $1$-, $\Pi$- and $\Sigma$-types in the strict sense clearly interprets $\mathsf{\lambda^{=}_{1,\times}}$, and it is not hard to see that the interpretation is sound and complete as well.

2.2.3 Interpretation of STLCs in CCCs

The standard categorical semantics of $\mathsf{\lambda^{=}_{1,\times}}$ is in CCCs, where contexts and types are both interpreted by objects, and terms by morphisms:

$\blacktriangleright$** Definition 2.2.10**** (Interpretation of $\mathsf{\lambda^{=}_{1,\times}}$ in CCCs [LS88, Pit01, Jac99, Cro93]).**

The interpretation $\llbracket\_\rrbracket$ of the equational theory $\mathsf{\lambda^{=}_{1,\times}}$ in a CCC $\mathcal{C}=(\mathcal{C},T,\times,\pi,\Rightarrow,\mathit{ev})$ is given by:

• $\blacktriangleright$

(Ct-Emp) $\llbracket\mathsf{\vdash\diamondsuit\ ctx}\rrbracket\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}T$;

• $\blacktriangleright$

(Ct-Ext) $\llbracket\mathsf{\vdash\Gamma,x:A\ ctx}\rrbracket\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\llbracket\mathsf{\vdash\Gamma\ ctx}\rrbracket\times\llbracket\mathsf{\vdash A\ type}\rrbracket$;

• $\blacktriangleright$

($\mathsf{1}$-Form) $\llbracket\mathsf{\vdash\mathsf{1}\ type}\rrbracket\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}T$;

• $\blacktriangleright$

($\Rightarrow$-Form) $\llbracket\mathsf{\vdash A\Rightarrow B\ type}\rrbracket\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\llbracket\mathsf{\vdash A\ type}\rrbracket\Rightarrow\llbracket\mathsf{\vdash B\ type}\rrbracket$;

• $\blacktriangleright$

($\times$-Form) $\llbracket\mathsf{\vdash A\times B\ type}\rrbracket\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\llbracket\mathsf{\vdash A\ type}\rrbracket\times\llbracket\mathsf{\vdash B\ type}\rrbracket$;

• $\blacktriangleright$

(Var) $\llbracket\mathsf{x_{1}:A_{1},x_{2}:A_{2},\dots,x_{j}:A_{j},\dots,x_{n}:A_{n}\vdash x_{j}:A_{j}}\rrbracket\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\pi_{j}$;

• $\blacktriangleright$

($\mathsf{1}$-Intro) $\llbracket\mathsf{\Gamma\vdash\star:\mathsf{1}}\rrbracket\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\ \!!_{\llbracket\mathsf{\Gamma}\rrbracket}$;

• $\blacktriangleright$

($\Rightarrow$-Intro) $\llbracket\mathsf{\Gamma\vdash\lambda x.\ \!b:A\Rightarrow B}\rrbracket\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\lambda_{\llbracket\mathsf{A}\rrbracket,\llbracket\mathsf{B}\rrbracket}(\llbracket\mathsf{\Gamma,x:A\vdash b:B}\rrbracket)$;

• $\blacktriangleright$

($\times$-Intro) $\llbracket\mathsf{\Gamma\vdash(a,b):A\times B}\rrbracket\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\langle\llbracket\mathsf{\Gamma\vdash a:A}\rrbracket,\llbracket\mathsf{\Gamma\vdash b:B}\rrbracket\rangle$;

• $\blacktriangleright$

($\Rightarrow$-Elim) $\llbracket\mathsf{\Gamma\vdash f(a):B}\rrbracket\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\mathit{ev}_{\llbracket\mathsf{A}\rrbracket,\llbracket\mathsf{B}\rrbracket}\circ\langle\llbracket\mathsf{\Gamma\vdash f:A\Rightarrow B}\rrbracket,\llbracket\mathsf{\Gamma\vdash a:A}\rrbracket\rangle$; and

• $\blacktriangleright$

($\times$-Elim) $\llbracket\mathsf{\Gamma\vdash\pi_{i}(p):A_{i}}\rrbracket\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\pi_{i}\circ\llbracket\mathsf{\Gamma\vdash p:A_{1}\times A_{2}}\rrbracket$

where the hypotheses of the rules are as presented in Section 2.1, and $\pi_{j}$ is constructed from the first and second projections in the obvious manner.

$\blacktriangleright$ Remark.

As each judgement in $\mathsf{\lambda^{=}_{1,\times}}$ has a unique derivation, Definition 2.2.10 has no problem.

In light of the rather simple relation between $\mathsf{MLTT(1,\Pi,\Sigma)}$ and $\mathsf{\lambda^{=}_{1,\times}}$, i.e., the restriction of the former to closed types is the latter, the gap between the interpretations of $\mathsf{\lambda^{=}_{1,\times}}$ in Definitions 2.2.7 and 2.2.10 should not be the case. We shall address this problem in Section 4.

3 Categories with Dependence

We have reviewed all the necessary backgrounds; the main contents of the paper begin from the present section. It is structured roughly as follows. First, Section 3.1 introduces categories with dependence (CwDs) and morphisms between CwDs, called functors with dependence (FwDs). Then, Section 3.2 defines CwDs with generalized finite products, called semi-cartesian CwDs (SCCwDs), and morphisms between them, called semi-cartesian FwDs (SCFwDs). The semi-cartesian structure enables us to define morphisms between SCFwDs, called natural transformations with dependence (NTwDs), and moreover the 2-category of SCCwDs (0-cells), SCFwDs (1-cells) and NTwDs (2-cells). Next, Section 3.3 gives a full generalization of finite products; we call CwDs with them cartesian CwDs (CCwDs). Finally Section 3.4 defines a closed structure on CCwDs; we call CCwDs with the closed structure cartesian closed CwDs (CCCwDs), where morphisms between these concepts, cartesian FwDs (CFwDs) and cartesian closed FwDs (CCFwDs), are also defined. These concepts constitute the 2-category of CCCwDs (0-cells), CCFwDs (1-cells) and NTwDs (2-cells) between them.

Along with these developments, we show that:

• $\blacktriangleright$

Strict SCCwDs coincide with CwFs;

• $\blacktriangleright$

Strict CCwDs induce CwFs that support $1$- and $\Sigma$-types in the strict sense; and

• $\blacktriangleright$

Strict CCCwDs induce CwFs that support $1$-, $\Sigma$- and $\Pi$-types in the strict sense.

Thus, in particular, we establish an interpretation of $\mathsf{MLTT}(1,\Pi,\Sigma)$ in CCCwDs; it is easy to see that this interpretation is sound and complete.

3.1 Categories and Functors with Dependence

Let us begin with a very simple generalization of categories to capture type dependence in DTTs, called categories with dependence (CwDs), and morphisms between them, called functors with dependence (FwDs).

3.1.1 Categories with Dependence

The idea of CwDs comes from CwFs: To take counterparts of types and terms as primitive, rather than to induce or compose them, which stands in sharp contrast to other categorical semantics of DTTs mentioned in the introduction.

$\blacktriangleright$** Definition 3.1.1**** (CwDs).**

A category with dependence (CwD) is a category $\mathcal{C}$ equipped with:

• $\blacktriangleright$

Dependent (D-) objects such that each D-object $A$ is assigned a unique object $\Gamma\in\mathcal{C}$, called the base of $A$, where $A$ is said to be over $\Gamma$, and the class of all D-objects over $\Gamma$ is written $\mathscr{D}_{\mathcal{C}}(\Gamma)$;

• $\blacktriangleright$

Dependent (D-) morphisms such that each D-morphism $f$ is assigned a unique pair of an object $\Gamma\in\mathcal{C}$ and a D-object $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$, called the domain and the codomain of $f$, respectively, where the class of all D-morphisms whose domain and codomain are $\Gamma$ and $A$, respectively, are written $\mathscr{D}_{\mathcal{C}}(\Gamma,A)$;

• $\blacktriangleright$

For each morphism $\phi:\Delta\to\Gamma$ in $\mathcal{C}$ a (class) function $\_\{\phi\}_{\mathcal{C}}:\mathscr{D}_{\mathcal{C}}(\Gamma)\to\mathscr{D}_{\mathcal{C}}(\Delta)$ and a family $(\_\{\phi\}_{\mathcal{C},A})_{A\in\mathscr{D}_{\mathcal{C}}(\Gamma)}$ of (class) functions $\_\{\phi\}_{\mathcal{C},A}:\mathscr{D}_{\mathcal{C}}(\Gamma,A)\to\mathscr{D}_{\mathcal{C}}(\Delta,A\{\phi\}_{\mathcal{C}})$, which are all called dependent (D-) compositions, that satisfy for any $\Theta,\Delta,\Gamma\in\mathcal{C}$, $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$, $\phi\in\mathcal{C}(\Delta,\Gamma),\varphi\in\mathcal{C}(\Theta,\Delta)$ and $a\in\mathscr{D}_{\mathcal{C}}(\Gamma,A)$ the equations $A\{\mathit{id}_{\Gamma}\}_{\mathcal{C}}=A$, $a\{\mathit{id}_{\Gamma}\}_{\mathcal{C},A}=a$, $A\{\phi\circ\varphi\}_{\mathcal{C}}=A\{\phi\}_{\mathcal{C}}\{\varphi\}_{\mathcal{C}}$ and $a\{\phi\circ\varphi\}_{\mathcal{C},A}=a\{\phi\}_{\mathcal{C},A}\{\varphi\}_{\mathcal{C},A\{\phi\}_{\mathcal{C}}}$.

$\blacktriangleright$ Notation.

We often omit the subscript $\mathcal{C}$ on $\mathscr{D}_{\mathcal{C}}$ and $\_\{\_\}_{\mathcal{C}}$ as well as the subscripts $\mathcal{C}$ and/or $A$ on $\_\{\_\}_{\mathcal{C},A}$ if it brings no ambiguity. We write $a:\Gamma\rightarrowtriangle A$ as a notation for $a\in\mathscr{D}(\Gamma,A)$. Given a CwD $\mathcal{C}$, we write $\mathsf{ob}(\mathcal{C})$ or $\mathcal{C}_{0}$ (resp. $\mathsf{ar}(\mathcal{C})$ or $\mathcal{C}_{1}$, $\mathsf{dob}(\mathcal{C})$ or $\mathcal{C}_{2}$, $\mathsf{dar}(\mathcal{C})$ or $\mathcal{C}_{3}$) for the class of all objects in $\mathcal{C}$ (resp. all morphisms in $\mathcal{C}$, all D-objects in $\mathcal{C}$, all D-morphisms in $\mathcal{C}$).

$\blacktriangleright$ Remark.

CwDs are nothing new; a CwD is just a substructure of a CwF (Definition 2.2.1), consisting of the underlying category, types, terms and substitutions of the CwF, where we have assigned new names to the last three components.

$\blacktriangleright$ Notation.

Let us write $\mathscr{U}(\mathcal{C})$ for the underlying category of a given CwD $\mathcal{C}$.

In an MLTT, assuming that each type has at least one non-variable term, a type is constant in the sense that it does not contain any free variable iff it is invariant (except its context) with respect to a generalized substitution. Thus, it seems natural to define:

$\blacktriangleright$** Definition 3.1.2**** (Constant CwDs).**

Let $\mathcal{C}$ be a CwD. A D-object $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ is constant if $A\{\phi_{1}\}_{\mathcal{C}}=A\{\phi_{2}\}_{\mathcal{C}}$ for all $\Delta\in\mathcal{C}$ and $\phi_{1},\phi_{2}:\Delta\to\Gamma$ in $\mathcal{C}$. A CwD is constant if its D-objects are all constant.

$\blacktriangleright$ Example 3.1.3.

Each category $\mathcal{C}$ can be seen as a constant CwD $\mathsf{D}(\mathcal{C})$ as follows. We define $\mathscr{D}_{\mathsf{D}(\mathcal{C})}(\Gamma)\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\mathsf{ob}(\mathcal{C})$ and $\mathscr{D}_{\mathsf{D}(\mathcal{C})}(\Delta,\Gamma)\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\mathcal{C}(\Delta,\Gamma)$ for all $\Delta,\Gamma\in\mathcal{C}$. Given $\phi:\Delta\to\Gamma$ in $\mathcal{C}$, we define the D-composition $\_\{\phi\}:\mathscr{D}_{\mathsf{D}(\mathcal{C})}(\Gamma)\to\mathscr{D}_{\mathsf{D}(\mathcal{C})}(\Delta)$ to be the identity function on $\mathsf{ob}(\mathcal{C})$, and the D-composition $\_\{\phi\}_{\Theta}:\mathscr{D}_{\mathsf{D}(\mathcal{C})}(\Gamma,\Theta)\to\mathscr{D}_{\mathsf{D}(\mathcal{C})}(\Delta,\Theta)$ for any $\Theta\in\mathscr{D}_{\mathsf{D}(\mathcal{C})}(\Gamma)$ to be the pre-composition function with $\phi$, i.e., $f\mapsto f\circ\phi$ for all $f\in\mathscr{D}_{\mathsf{D}(\mathcal{C})}(\Gamma,\Theta)$. We call this kind of CwDs categories seen as CwDs. Moreover, the operation $\mathscr{U}$, restricted to CwDs $\mathcal{D}$ such that $\mathscr{D}_{\mathcal{D}}(\Gamma)=\mathsf{ob}(\mathcal{D})$, $\mathscr{D}_{\mathcal{D}}(\Delta,\Gamma)=\mathcal{D}(\Delta,\Gamma)$, $\_\{\phi\}=\mathit{id}_{\mathsf{ob}(\mathcal{D})}$ and $\_\{\phi\}_{\Theta}=(\_)\circ\phi$ for all $\Delta,\Gamma,\Theta\in\mathcal{D}$ and $\phi:\Delta\to\Gamma$ in $\mathcal{D}$, is clearly the inverse of the operation $\mathsf{D}$. Hence, CwDs are generalized categories.

$\blacktriangleright$ Remark.

It is also possible to regard each category $\mathcal{C}$ as a constant CwD $\mathsf{d}(\mathcal{C})$ by $\mathscr{D}_{\mathsf{d}(\mathcal{C})}(\Gamma)\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\emptyset$, but it does not reflect our view on CwDs as generalized categories. This point will be clearer shortly as we proceed.

Also, it seems natural to lift smallness and local smallness of categories as follows:

$\blacktriangleright$** Definition 3.1.4**** (Small CwDs).**

A CwD $\mathcal{C}$ is small if so is the underlying category $\mathscr{U}(\mathcal{C})$, and the class of all D-objects in $\mathcal{C}$ and the class of all D-morphisms in $\mathcal{C}$ are both sets.

$\blacktriangleright$** Definition 3.1.5**** (Locally small CwDs).**

A CwD $\mathcal{C}$ is locally small if so is the underlying category $\mathscr{U}(\mathcal{C})$, and the class $\mathscr{D}_{\mathcal{C}}(\Gamma,A)$ is a set for any $\Gamma\in\mathcal{C}$ and $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$.

$\blacktriangleright$ Example 3.1.6.

The category $\mathit{Sets}$ of sets and functions gives rise to a non-constant locally small CwD. A D-object over a set $X$ in $\mathit{Sets}$ is an indexed set $A=\{A_{x}\in\mathit{Sets}\mid x\in X\ \!\}$, called a dependent (D-) set over $X$. A D-morphism $X\rightarrowtriangle A$ in $\mathit{Sets}$ is a function $f:X\to\bigcup_{x\in X}A_{x}$ that satisfies $f(x)\in A_{x}$ for all $x\in X$, called a dependent (D-) function from $X$ to $A$. Given a function $\phi:Y\to X$, the D-compositions in $\mathit{Sets}$ are given by $A\{\phi\}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\{A_{\phi(y)}\mid y\in Y\ \!\}$ and $f\{\phi\}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}f\circ\phi:(y\in Y)\mapsto f(\phi(y))\in A_{\phi(y)}=(A\{\phi\})_{y}$.

It is straightforward to define the substructure relation between CwDs:

$\blacktriangleright$** Definition 3.1.7**** (SubCwDs).**

A CwD $\mathcal{C}$ is a subCwD of another $\mathcal{D}$ if $\mathscr{U}(\mathcal{C})$ is a subcategory of $\mathscr{U}(\mathcal{D})$, and the dependence of $\mathcal{C}$ is the corresponding part of the dependence of $\mathcal{D}$, i.e., for all $\Delta,\Gamma\in\mathcal{C}$, $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$, $f\in\mathscr{D}_{\mathcal{C}}(\Gamma,A)$ and $\phi:\Delta\to\Gamma$ in $\mathcal{C}$ we have $A\in\mathscr{D}_{\mathcal{D}}(\Gamma)$, $f\in\mathscr{D}_{\mathcal{D}}(\Gamma,A)$, $A\{\phi\}_{\mathcal{C}}=A\{\phi\}_{\mathcal{D}}$ and $f\{\phi\}_{\mathcal{C}}=f\{\phi\}_{\mathcal{D}}$.

$\blacktriangleright$** Definition 3.1.8**** (Full and wide subCwDs).**

A CwD $\mathcal{C}$ is a full subCwD (resp. wide subCwD) of a CwD $\mathcal{D}$ if $\mathcal{C}$ is a subCwD of $\mathcal{D}$, $\mathscr{U}(\mathcal{C})$ is a full (resp. wide) subcategory of $\mathscr{U}(\mathcal{D})$, and $\mathscr{D}_{\mathcal{C}}(\Gamma,A)=\mathscr{D}_{\mathcal{D}}(\Gamma,A)$ for all $\Gamma\in\mathcal{C}$ and $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ (resp. $\mathscr{D}_{\mathcal{C}}(\Gamma)=\mathscr{D}_{\mathcal{D}}(\Gamma)$ for all $\Gamma\in\mathcal{C}$).

$\blacktriangleright$ Example 3.1.9.

Similarly to the CwD $\mathit{Sets}$, there is a non-constant locally small CwD $\mathit{Rel}$ whose underlying category is the category $\mathit{Rel}$ of sets and relations. D-objects in $\mathit{Rel}$ are D-sets, D-morphisms $X\rightarrowtriangle A$ in $\mathit{Rel}$ are relations $R\subseteq X\times\bigcup_{x\in X}A_{x}$ such that $(x,a)\in R\Rightarrow a\in A_{x}$, D-compositions in $\mathit{Rel}$ are given by $A\{\phi\}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\{\bigcup_{(y,x)\in\phi}A_{x}\mid y\in Y\ \!\}$, i.e., $A\{\phi\}_{y}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\bigcup_{(y,x)\in\phi}A_{x}$ for all $y\in Y$ and $R\{\phi\}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}R\circ\phi=\{(y,a)\mid\exists x\in X.\ \!(y,x)\in\phi\wedge(x,a)\in R\ \!\}$ for any relation $\phi\subseteq Y\times X$. It is straightforward to see that $\mathit{Sets}$ is a wide subCwD of $\mathit{Rel}$, lifting the relation between the categories $\mathit{Sets}$ and $\mathit{Rel}$.

$\blacktriangleright$ Example 3.1.10.

There is a non-constant locally small CwD $\mathit{Mon}$ whose underlying category is the category $\mathit{Mon}$ of monoids and monoid homomorphisms. A D-object over a monoid $M=(|M|,\cdot_{M},e_{M})$ in $\mathit{Mon}$ is a triple $A=(|A|,\cdot_{A},e_{A})$ of an indexed set $|A|=(A_{m})_{m\in|M|}$, a binary operation $\cdot_{A}$ on the union $\bigcup|A|\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\bigcup_{m\in|M|}A_{m}$ satisfying $a\cdot_{A}a^{\prime}\in A_{m\cdot_{M}m^{\prime}}$ for all $m,m^{\prime}\in|M|$, $a\in A_{m}$ and $a\in A_{m^{\prime}}$, and an element $e_{A}\in A_{e_{M}}$ such that the triple $\bigcup A=(\bigcup|A|,\cdot_{A},e_{A})$ forms a monoid, called a dependent (D-) monoid over $M$, and a D-morphism $M\rightarrowtriangle A$ in $\mathit{Mon}$ is a monoid homomorphism $f:M\to\bigcup A$ such that $f(m)\in A_{m}$ for all $m\in|M|$. Given a monoid homomorphism $\phi:N\to M$, the D-composition $A\{\phi\}=(|A\{\phi\}|,\cdot_{A\{\phi\}},e_{A\{\phi\}})$ is given by $A\{\phi\}_{n}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}A_{\phi(n)}$ for each $n\in|N|$, $\cdot_{A\{\phi\}}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\cdot_{A}\upharpoonright\bigcup|A\{\phi\}|$ and $e_{A\{\phi\}}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}e_{A}$, and the D-composition $f\{\phi\}$ is simply given by the function composition $f\circ\phi$.

One may wonder, as in the case of the CwDs $\mathit{Sets}$, $\mathit{Rel}$ and $\mathit{Mon}$, whether D-morphisms are always certain morphisms in the underlying category; however, it is not the case. For instance, in the term model $\mathcal{T}(1,\Pi,\Sigma)$ regarded as a CwD, i.e., its types, terms and substitutions are regarded respectively as D-objects, D-morphisms and D-compositions, note that morphisms (or context morphisms) are certain lists of D-morphisms (or terms).

There are other non-trivial CwDs whose D-morphisms are not certain morphisms:

$\blacktriangleright$ Example 3.1.11.

There is a non-constant locally small CwD $\mathcal{GPD}$ whose underlying category is the category $\mathcal{GPD}$ of groupoids and functors between them [HS98]. A D-object over a groupoid $G$ in $\mathcal{GPD}$ is any functor $A:G\to\mathcal{GPD}$, called a dependent (D-) groupoid. In order to define D-morphisms in $\mathcal{GPD}$, it is convenient (though not strictly necessary) to first employ the Grothendieck construction $G.A\in\mathcal{GPD}$ of $G$ and $A$, which is given by:

• $\blacktriangleright$

An object of $G.A$ is a pair $(g,a)$ of objects $g\in G$ and $a\in A(g)$;

• $\blacktriangleright$

A morphism $(g,a)\to(g^{\prime},a^{\prime})$ in $G.A$ is a pair $(\phi,f)$ of a morphism $\phi:g\to g^{\prime}$ in $G$ and a morphism $f:A(\phi)(a)\to a^{\prime}$ in $A(g^{\prime})$;

• $\blacktriangleright$

The composition $(g,a)\stackrel{{\scriptstyle(\phi,f)}}{{\to}}(g^{\prime},a^{\prime})\stackrel{{\scriptstyle(\phi^{\prime},f^{\prime})}}{{\to}}(g^{\prime\prime},a^{\prime\prime})$ in $G.A$ is the pair $(\phi^{\prime}\circ\phi,f^{\prime}\circ A(\phi^{\prime})(f))$;

• $\blacktriangleright$

The identity $\mathit{id}_{(g,a)}:(g,a)\to(g,a)$ in $G.A$ is the pair $(\mathit{id}_{g},\mathit{id}_{a})$; and

• $\blacktriangleright$

The inverse of $(\phi,f):(g,a)\to(g^{\prime},a^{\prime})$ is the pair $(\phi^{-1},A(\phi^{-1})(f^{-1})):(g^{\prime},a^{\prime})\to(g,a)$.

Then, a D-morphism $G\rightarrowtriangle A$ in $\mathcal{GPD}$ is a pair $\mu=(\mu_{0},\mu_{1})$ of maps $\mu_{0}:\mathsf{ob}(G)\to\bigcup_{g\in G}\mathsf{ob}(A(g))$ and $\mu_{1}:\mathsf{ar}(G)\to\bigcup_{g\in G}\mathsf{ar}(A(g))$ such that

[TABLE]

for all $g,g^{\prime},g^{\prime\prime}\in G$, $\phi:g\to g^{\prime}$ and $\psi:g^{\prime}\to g^{\prime\prime}$ in $G$, i.e., the pairing $\langle\mathit{id}_{G},\mu\rangle$ is a functor $G\to G.A$. Note that it is impossible to turn $\mu$ into a morphism in $\mathcal{GPD}$ for there is no groupoid to serve as the codomain of $\mu$; we have employed $G.A$ to make this point clear. Finally, given a morphism $F:H\to G$ in $\mathcal{GPD}$, the D-composition $A\{F\}:H\to\mathcal{GPD}$ is the composition $A\circ F$ of functors, and the D-composition $\mu\{F\}:H\rightarrowtriangle A\{F\}$ is given by $\mu\{F\}_{i}=\mu_{i}\circ F_{i}$ for $i=1,2$.

$\blacktriangleright$ Example 3.1.12.

Similarly to $\mathcal{GPD}$, the category $\mathit{CAT}$ of small categories and functors between them forms a non-constant locally small CwD. A D-object over a category $\mathcal{C}$ in $\mathit{CAT}$ is a functor $\mathcal{X}:\mathcal{C}\to\mathit{CAT}$, called a dependent (D-) category, and a D-morphism $\mathcal{C}\rightarrowtriangle\mathcal{X}$ in $\mathit{CAT}$ is a pair $F=(F_{0},F_{1})$ of maps $F_{0}:\mathsf{ob}(\mathcal{C})\to\bigcup_{\Gamma\in\mathcal{C}}\mathsf{ob}(\mathcal{X}(\Gamma))$ and $F_{1}:\mathsf{ar}(\mathcal{C})\to\bigcup_{\Gamma\in\mathcal{C}}\mathsf{ar}(\mathcal{X}(\Gamma))$ such that

[TABLE]

for all $\Delta,\Gamma,\Theta\in\mathcal{C}$, $\phi:\Delta\to\Gamma$ and $\psi:\Gamma\to\Theta$ in $\mathcal{C}$, called a dependent (D-) functor, where the category $\mathcal{C}.\mathcal{X}$ is the Grothendieck construction of $\mathcal{C}$ and $\mathcal{X}$ (discarding the structure of inverses). Finally, D-compositions in $\mathit{CAT}$ are defined exactly as in the case of $\mathcal{GPD}$.

Now, one may wonder what is an appropriate notion of isomorphisms between D-objects for it is a fundamental principle in category theory to regard isomorphic objects as essentially the same. Thinking of the CwD $\mathit{Sets}$ as an example, it sounds fair to say that two D-sets $A$ and $A^{\prime}$ are isomorphic if they are over sets $X$ and $X^{\prime}$, respectively, such that there is a bijection $\iota:X\stackrel{{\scriptstyle\sim}}{{\to}}X^{\prime}$, and $A_{x}$ is isomorphic to $A^{\prime}_{\iota(x)}$ for each $x\in X$ because then the structures of $A$ and $A^{\prime}$ as D-sets are essentially the same. However, the second condition does not make sense for an arbitrary CwD (i.e., we cannot always talk about the components $A_{x}$). We need additional conditions on CwDs, which will be introduced in Section 3.2, to talk about isomorphisms between D-objects.

Next, note that the asymmetry of the domain and the codomain of D-morphisms prohibits us from defining the ‘opposite CwDs’ just by ‘flipping’ morphisms and D-morphisms in a given CwD. However, we may ‘flip’ only morphisms, not D-morphisms, taking this operation as the ‘opposite’ construction on CwDs. Thus, we do not need any new concepts for this construction; it suffices to consider CwDs whose underlying categories are opposite categories.

Nevertheless, it is often convenient to give the explicit definition:

$\blacktriangleright$** Definition 3.1.13**** (Contravariant CwDs).**

A contravariant CwD is a category $\mathcal{C}$ equipped with a pair $(\mathscr{D}_{\mathcal{C}},\_\{\_\}_{\mathcal{C}})$, called the dependence of $\mathcal{C}$, where:

• $\blacktriangleright$

$\mathscr{D}_{\mathcal{C}}$ assigns to each object $\Gamma\in\mathcal{C}$ a class $\mathscr{D}_{\mathcal{C}}(\Gamma)$ of dependent (D-) objects over $\Gamma$ and to each pair of $\Gamma\in\mathcal{C}$ and $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ a class $\mathscr{D}_{\mathcal{C}}(\Gamma,A)$ of dependent (D-) morphisms from $\Gamma$ to $A$;

• $\blacktriangleright$

$\_\{\_\}_{\mathcal{C}}$ assigns to each morphism $\phi:\Delta\to\Gamma$ in $\mathcal{C}$ a (class) function $\_\{\phi\}_{\mathcal{C}}:\mathscr{D}_{\mathcal{C}}(\Delta)\to\mathscr{D}_{\mathcal{C}}(\Gamma)$ and a family $(\_\{\phi\}_{\mathcal{C},A})_{A\in\mathscr{D}_{\mathcal{C}}(\Gamma)}$ of (class) functions $\_\{\phi\}_{\mathcal{C},A}:\mathscr{D}_{\mathcal{C}}(\Delta,B)\to\mathscr{D}_{\mathcal{C}}(\Gamma,B\{\phi\}_{\mathcal{C}})$, which are all called contravariant dependent (D-) compositions that satisfy:

[TABLE]

for any $\Theta,\Delta,\Gamma\in\mathcal{C}$, $B\in\mathscr{D}_{\mathcal{C}}(\Delta)$, $\phi\in\mathcal{C}(\Delta,\Gamma),\psi\in\mathcal{C}(\Gamma,\Theta)$ and $b\in\mathscr{D}_{\mathcal{C}}(\Delta,B)$.

$\blacktriangleright$ Notation.

We write $\mathcal{C}^{\mathsf{op}}$ for the opposite category of a given category $\mathcal{C}$, and $\phi^{\mathsf{op}}:\Gamma\to\Delta$ in $\mathcal{C}^{\mathsf{op}}$ for the ‘flipped’ morphism $\phi:\Delta\to\Gamma$ in $\mathcal{C}$.

$\blacktriangleright$ Remark.

A contravariant CwD $\mathcal{C}$ is nothing other than a CwD $\mathcal{C}^{\mathsf{op}}$ described in terms of the category $\mathcal{C}$.

$\blacktriangleright$ Notation.

The notations for CwDs are also applied to contravariant CwDs.

We are now ready to define:

$\blacktriangleright$** Definition 3.1.14**** (Opposites).**

Given a CwD $\mathcal{C}$, its opposite $\mathcal{C}^{\mathsf{op}}$ is the contravariant CwD such that $\mathscr{U}(\mathcal{C}^{\mathsf{op}})\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\mathscr{U}(\mathcal{C})^{\mathsf{op}}$, $\mathscr{D}_{\mathcal{C}^{\mathsf{op}}}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\mathscr{D}_{\mathcal{C}}$ and $\_\{\_\}_{\mathcal{C}^{\mathsf{op}}}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\_\{\_\}_{\mathcal{C}}\circ(\_)^{\mathsf{op}}$. Dually, the opposite $\mathcal{D}^{\mathsf{op}}$ of a contravariant CwD $\mathcal{D}$ is the CwD defined in the same manner.

For a contravariant CwD $\mathcal{C}$ is just a CwD $\mathcal{C}^{\mathsf{op}}$, by the principle of duality [ML13, Awo10], it suffices to focus only on (covariant) CwDs. However, just for convenience, we occasionally describe contravariant ones $\mathcal{C}^{\mathsf{op}}$ explicitly in terms of $\mathcal{C}$ like Definition 3.1.13.

3.1.2 Functors with Dependence

Next, let us generalize functors by taking into account D-objects and D-morphisms:

$\blacktriangleright$** Definition 3.1.15**** (FwDs).**

A functor with dependence (FwD) between CwDs $\mathcal{C}$ and $\mathcal{D}$ is a quadruple $F=(F_{0},F_{1},F_{2},F_{3})$, written $F:\mathcal{C}\to\mathcal{D}$, of maps $F_{i}:\mathcal{C}_{i}\to\mathcal{D}_{i}$ that satisfies:

$\forall\Delta,\Gamma\in\mathcal{C},\phi\in\mathcal{C}(\Delta,\Gamma).\ \!F_{1}(\phi)\in\mathcal{D}(F_{0}(\Delta),F_{0}(\Gamma))$; 2. 2.

$\forall\Gamma\in\mathcal{C},A\in\mathscr{D}_{\mathcal{C}}(\Gamma).\ \!F_{2}(A)\in\mathscr{D}_{\mathcal{D}}(F_{0}(\Gamma))$; 3. 3.

$\forall\Gamma\in\mathcal{C},A\in\mathscr{D}_{\mathcal{C}}(\Gamma),a\in\mathscr{D}_{\mathcal{C}}(\Gamma,A).\ \!F_{3}(a)\in\mathscr{D}_{\mathcal{D}}(F_{0}(\Gamma),F_{2}(A))$; 4. 4.

$\forall\Delta,\Gamma,\Theta\in\mathcal{C},\phi\in\mathcal{C}(\Delta,\Gamma),\psi\in\mathcal{C}(\Gamma,\Theta).\ \!F_{1}(\psi\circ\phi)=F_{1}(\psi)\circ F_{1}(\phi)$; 5. 5.

$\forall\Gamma\in\mathcal{C}.\ \!F_{1}(\mathit{id}_{\Gamma})=\mathit{id}_{F_{0}(\Gamma)}$; 6. 6.

$\forall\Delta,\Gamma\in\mathcal{C},\phi\in\mathcal{C}(\Delta,\Gamma),A\in\mathscr{D}_{\mathcal{C}}(\Gamma).\ \!F_{2}(A\{\phi\}_{\mathcal{C}})=F_{2}(A)\{F_{1}(\phi)\}_{\mathcal{D}}$; and 7. 7.

$\forall\Delta,\Gamma\in\mathcal{C},\phi\in\mathcal{C}(\Delta,\Gamma),A\in\mathscr{D}_{\mathcal{C}}(\Gamma),a\in\mathscr{D}_{\mathcal{C}}(\Gamma,A).\ \!F_{3}(a\{\phi\}_{\mathcal{C}})=F_{3}(a)\{F_{1}(\phi)\}_{\mathcal{D}}$.

$\blacktriangleright$ Convention.

We usually abbreviate each $F_{i}$ ($i=0,1,2,3$) as $F$, which would not bring any confusion in practice.

That is, an FwD $F:\mathcal{C}\to\mathcal{D}$ is just a functor $\mathscr{U}(F)\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}(F_{0},F_{1}):\mathscr{U}(\mathcal{C})\to\mathscr{U}(\mathcal{D})$ equipped with maps $F_{2}$ and $F_{3}$ on D-objects and D-morphisms, respectively, with analogous structure-preserving properties.

$\blacktriangleright$ Example 3.1.16.

Given a functor $F:\mathcal{C}\to\mathcal{D}$, there are the obvious FwDs $\mathsf{D}(F):\mathsf{D}(\mathcal{C})\to\mathsf{D}(\mathcal{D})$. We call this kind of FwDs functors seen as FwDs. Conversely, FwDs between categories seen as CwDs coincide with functors. In this sense, FwDs are a generalization of functors. Note also that there are the trivial FwDs $\mathsf{d}(F):\mathsf{d}(\mathcal{C})\to\mathsf{d}(\mathcal{D})$.

$\blacktriangleright$ Example 3.1.17.

There is an FwD $(\_)^{\ast}:\mathit{Sets}\to\mathit{Mon}$ that maps:

[TABLE]

where $X^{\ast}=(X^{\ast},\ast,\bm{\epsilon})$ is the free monoid over $X$, $\phi^{\ast}$ (resp. $f^{\ast}$) maps each $x_{1}x_{2}\dots x_{k}\in X^{\ast}$ to $\phi(x_{1})\phi(x_{2})\dots\phi(x_{k})\in Y^{\ast}$ (resp. to $f(x_{1})f(x_{2})\dots f(x_{k})\in\prod_{i=1}^{k}A_{x_{i}}$), and $\prod_{i=1}^{k}A_{x_{i}}$ is the product of monoids $A_{x_{i}}$ for $i=1,2,\dots,k$.

$\blacktriangleright$** Definition 3.1.18**** (Fullness and faithfulness of FwDs).**

An FwD $F:\mathcal{C}\to\mathcal{D}$ is full (resp. faithful) if so is the underlying functor $\mathscr{U}(F)$, and the function $F_{\Gamma,A}:\mathscr{D}_{\mathcal{C}}(\Gamma,A)\to\mathscr{D}_{\mathcal{D}}(F(\Gamma),F(A))$ that maps $f\mapsto F(f)$ for all $f\in\mathscr{D}_{\mathcal{C}}(\Gamma,A)$ is surjective (resp. injective) for each pair of an object $\Gamma\in\mathcal{C}$ and a D-object $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ in $\mathcal{C}$.

Just for convenience, let us write down explicitly the contravariant case:

$\blacktriangleright$** Definition 3.1.19**** (Contravariant FwDs).**

A contravariant FwD from a contravariant CwD $\mathcal{C}$ to a CwD $\mathcal{D}$ is an FwD $F:\mathcal{C}^{\mathsf{op}}\to\mathcal{D}$. Dually, a contravariant FwD from $\mathcal{D}$ to $\mathcal{C}$ is a contravariant FwD $\mathcal{D}^{\mathsf{op}}\to\mathcal{C}^{\mathsf{op}}$, i.e., an FwD $\mathcal{D}\to\mathcal{C}^{\mathsf{op}}$.

$\blacktriangleright$ Example 3.1.20.

Given a locally small CwD $\mathcal{C}$ and an object $\Delta\in\mathcal{C}$, we obtain an FwD $\mathcal{C}(\Delta,\_):\mathcal{C}\to\mathit{Sets}$ that maps each object $\Gamma\in\mathcal{C}$ to the set $\mathcal{C}(\Delta,\Gamma)$, each morphism $\alpha\in\mathcal{C}(\Gamma,\Gamma^{\prime})$ to the function $\mathcal{C}(\Delta,\alpha):\mathcal{C}(\Delta,\Gamma)\to\mathcal{C}(\Delta,\Gamma^{\prime})$ that maps $(\phi\in\mathcal{C}(\Delta,\Gamma))\mapsto\alpha\circ\phi\in\mathcal{C}(\Delta,\Gamma^{\prime})$, each D-object $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ to the D-set $\mathcal{C}(\Delta,A)\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}(\mathscr{D}_{\mathcal{C}}(\Delta,A\{\phi\}_{\mathcal{C}}))_{\phi\in\mathcal{C}(\Delta,\Gamma)}$, and each D-morphism $f\in\mathscr{D}_{\mathcal{C}}(\Gamma,A)$ to the D-function $\mathcal{C}(\Delta,f):\mathcal{C}(\Delta,\Gamma)\rightarrowtriangle\mathcal{C}(\Delta,A)$ that maps $(\phi\in\mathcal{C}(\Delta,\Gamma))\mapsto f\{\phi\}_{\mathcal{C}}\in\mathscr{D}_{\mathcal{C}}(\Delta,A\{\phi\}_{\mathcal{C}})=\mathcal{C}(\Delta,A)_{\phi}$.

Dually, given a locally small contravariant CwD $\mathcal{D}$ and an object $\Delta\in\mathcal{D}$, we obtain a contravariant FwD $\mathcal{D}(\_,\Delta):\mathcal{D}\to\mathit{Sets}$ that maps each object $\Gamma\in\mathcal{D}$ to the set $\mathcal{D}(\Gamma,\Delta)$, each morphism $\beta\in\mathcal{D}(\Gamma^{\prime},\Gamma$) to the function $\mathcal{D}(\beta,\Delta):\mathcal{D}(\Gamma,\Delta)\to\mathcal{D}(\Gamma^{\prime},\Delta)$ that maps $(\varphi\in\mathcal{D}(\Gamma,\Delta))\mapsto\varphi\circ\beta\in\mathcal{D}(\Gamma^{\prime},\Delta)$, each D-object $A\in\mathscr{D}_{\mathcal{D}}(\Gamma)$ to the D-set $\mathcal{D}(A,\Delta)\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}(\mathscr{D}_{\mathcal{D}}(\Delta,A\{\varphi\}_{\mathcal{D}}))_{\varphi\in\mathcal{D}(\Gamma,\Delta)}$, and each D-morphism $f\in\mathscr{D}_{\mathcal{D}}(\Gamma,A)$ to the D-function $\mathcal{D}(f,\Delta):\mathcal{D}(\Gamma,\Delta)\rightarrowtriangle\mathcal{D}(A,\Delta)$ that maps $(\varphi\in\mathcal{D}(\Gamma,\Delta))\mapsto f\{\varphi\}_{\mathcal{D}}\in\mathscr{D}_{\mathcal{D}}(\Delta,A\{\varphi\}_{\mathcal{D}})=\mathcal{D}(A,\Delta)_{\varphi}$.

As expected, small CwDs and FwDs between them form a category:

$\blacktriangleright$** Definition 3.1.21**** (The category $\mathbb{C}_{\mathbb{D}}$).**

The category $\mathbb{C}_{\mathbb{D}}$ is given by:

• $\blacktriangleright$

Objects are small CwDs;

• $\blacktriangleright$

Morphism $\mathcal{C}\to\mathcal{D}$ are FwDs $\mathcal{C}\to\mathcal{D}$;

• $\blacktriangleright$

The composition $\mathcal{C}\stackrel{{\scriptstyle F}}{{\to}}\mathcal{D}\stackrel{{\scriptstyle G}}{{\to}}\mathcal{E}$ is the quadruple $(G_{0}\circ F_{0},G_{1}\circ F_{1},G_{2}\circ F_{2},G_{3}\circ F_{3})$; and

• $\blacktriangleright$

The identity $\mathit{id}_{\mathcal{C}}:\mathcal{C}\to\mathcal{C}$ is the quadruple $(\mathit{id}_{\mathcal{C}_{0}},\mathit{id}_{\mathcal{C}_{1}},\mathit{id}_{\mathcal{C}_{2}},\mathit{id}_{\mathcal{C}_{3}})$.

It is easy to check that $\mathbb{C}_{\mathbb{D}}$ is a well-defined locally small category, and there is the obvious forgetful functor $\mathscr{U}:\mathbb{C}_{\mathbb{D}}\to\mathit{CAT}$, which has the functor $\mathsf{d}:\mathit{CAT}\to\mathbb{C}_{\mathbb{D}}$ as the left adjoint.

On the other hand, there seems no sensible way to lift the category $\mathbb{C}_{\mathbb{D}}$ to a CwD. One may define a D-object over a small CwD $\mathcal{C}$ to be an FwD $\mathcal{C}\to\mathit{CAT}$ or a functor $\mathscr{U}(\mathcal{C})\to\mathbb{C_{D}}$, but neither works very well.

3.2 Semi-Cartesian Categories, Functors and Natural Transformations with Dependence

As we have seen above, CwDs and FwDs are natural generalizations of categories and functors, respectively, which subsume several concrete instances. However, we cannot yet have morphisms between parallel FwDs because we cannot define morphisms between D-objects at the moment. Thus, CwDs and FwDs are in some sense incomplete structures.

On the other hand, we need additional structures on CwDs in order to interpret the empty context Ctx-Emp and context extensions Ctx-Ext in MLTTs.

The present section addresses these two problems by introducing CwDs with generalized binary products, called semi-dependent pair (semi-$\Sigma$-) spaces. We call CwDs with a terminal object and semi-$\Sigma$-spaces semi-cartesian CwDs (SCCwDs); their strict version coincides with CwFs, and thus they interpret the empty context and context extensions. We also define FwDs that preserve the semi-cartesian structure of CwDs, called semi-cartesian FwDs (SCFwDs) and morphisms between parallel SCFwDs, called natural transformations with dependence (NTwDs), which constitute 1-cells and 2-cells of the 2-category of SCCwDs (0-cells), respectively. Moreover, as promised before, we lift this 2-category to a 2-CwD, the 2-dimensional generalization of CwDs.

3.2.1 Semi-Cartesian Categories with Dependence

$\blacktriangleright$** Definition 3.2.1**** (Semi-$\Sigma$-spaces).**

Let $\mathcal{C}$ be a CwD. A semi-dependent pair (semi-$\bm{\Sigma}$-) space of an object $\Gamma\in\mathcal{C}$ and a D-object $A\in\mathscr{D}(\Gamma)$ is an object

[TABLE]

together with a morphism

[TABLE]

in $\mathcal{C}$, called the first projection on $\Gamma.A$, and a D-morphism

[TABLE]

in $\mathcal{C}$, called the second projection on $\Gamma.A$, such that for any $\Delta\in\mathcal{C}$, $\phi:\Delta\to\Gamma$ and $g:\Delta\rightarrowtriangle A\{\phi\}$ in $\mathcal{C}$ there exists a unique morphism

[TABLE]

in $\mathcal{C}$, called the semi-dependent pairing of $\phi$ and $g$, that satisfies the equations

[TABLE]

$\blacktriangleright$ Notation.

We often omit the superscript $\Gamma.A$ on $\pi_{i}^{\Gamma.A}$ ($i=1,2$).

$\blacktriangleright$** Definition 3.2.2**** (SCCwDs).**

A semi-cartesian CwD (SCCwD) is a CwD $\mathcal{C}$ that has:

• $\blacktriangleright$

A terminal object $T\in\mathcal{C}$; and

• $\blacktriangleright$

A semi-$\Sigma$-pair space $\Gamma\stackrel{{\scriptstyle\pi_{1}}}{{\leftarrow}}\Gamma.A\stackrel{{\scriptstyle\pi_{2}}}{{\rightarrowtriangle}}A\{\pi_{1}\}$ of any $\Gamma\in\mathcal{C}$ and $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$.

See the following diagram that depicts the universal property of semi-$\Sigma$-spaces: {diagram} where the thick arrow $A\{\pi_{1}\}\Rightarrow A\{\phi\}$ denotes the transformation of the codomain of $\pi_{2}$ when $\langle\phi,g\rangle$ is composed with $\pi_{2}$. Clearly, it generalizes the universal property of binary products in the sense that for a category seen as a CwD the diagram coincides with that of binary products; in other words, for a category seen as a CwD, semi-$\Sigma$-spaces $\Gamma.A$ are just binary products $\Gamma\times A$. In this sense, SCCwDs are a generalization of cartesian categories.

On the other hand, unlike binary products, we do not even have a sensible way to formulate, let alone prove, that a terminal object is unit for semi-$\Sigma$-spaces, or semi-$\Sigma$-spaces are associative, due to the asymmetry of semi-$\Sigma$-spaces. We need unit D-objects and $\Sigma$-spaces in Section 3.3 to address this point.

Similarly to the case of binary products, we may easily establish:

$\blacktriangleright$** Proposition 3.2.3**** (Uniqueness of semi-$\Sigma$-spaces).**

Semi-$\Sigma$-spaces are unique up to isomorphisms.

$\blacktriangleright$** Lemma 3.2.4**** (Semi-dependent pairings as comprehensions).**

Let $\mathcal{C}$ be an SCCwD, and $\Theta,\Delta,\Gamma\in\mathcal{C}$, $A\in\mathscr{D}(\Gamma)$, $\varphi:\Theta\to\Delta$, $\phi:\Delta\to\Gamma$ and $g:\Delta\rightarrowtriangle A\{\phi\}$ in $\mathcal{C}$. Then, we have:

[TABLE]

Note that the equations (5) and (6) correspond respectively to the axioms Cons-Nat and Cons-Id for CwFs, and thus Lemma 3.2.4 particularly implies that an SCCwD is a CwF except that a terminal object, comprehensions, projections and extensions are not parts of the structure, and comprehensions and extensions are called semi-$\Sigma$-spaces and semi-dependent pairings, respectively. Hence, CwFs are the strict version of SCCwDs.

Nevertheless, we require some equation for our notion of strict SCCwDs:

$\blacktriangleright$** Definition 3.2.5**** (Strict SCCwDs).**

A strict SCCwD is an SCCwD $\mathcal{C}$ equipped with a terminal object $T\in\mathcal{C}$ and a semi-$\Sigma$-space $\Gamma\stackrel{{\scriptstyle\pi_{1}}}{{\leftarrow}}\Gamma.A\stackrel{{\scriptstyle\pi_{2}}}{{\rightarrowtriangle}}A\{\pi_{1}\}$ that satisfies:

[TABLE]

for each $\Gamma\in\mathcal{C}$ and $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$.

We shall need this equation for the proof of Theorem 3.4.15.

$\blacktriangleright$ Example 3.2.6.

A category $\mathcal{C}$ seen as a CwD $\mathsf{D}(\mathcal{C})$ is semi-cartesian iff $\mathcal{C}$ is cartesian. We call this kind of SCCwDs cartesian categories seen as SCCwDs.

$\blacktriangleright$ Example 3.2.7.

The CwD $\mathit{Sets}$ is semi-cartesian. Any singleton set $\{\bullet\}$ is a terminal object, and given a set $X$ and an indexed set $A$ over $X$ the set $\{(x,a)\mid x\in X,a\in A_{x}\ \!\}$ of semi-dependent pairs $(x,a)$ is a semi-$\Sigma$-space $X.A$ together with the projection functions as the projections. Semi-dependent pairings are just pairings of functions.

$\blacktriangleright$ Example 3.2.8.

The CwD $\mathit{Rel}$ is semi-cartesian. The empty set $\emptyset$ is a terminal (as well as initial) object, and given a set $X$ and an indexed set $A$ over $X$ the disjoint union $X+\bigcup_{x\in X}A_{x}$ is a semi-$\Sigma$-space $X.A$ together with the first projection $\pi_{1}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\{(\iota_{1}(x),x)\mid x\in X\ \!\}\subseteq X.A\times X$ and the second projection $\pi_{2}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\{(\iota_{2}(a),a)\mid a\in\bigcup_{x\in X}A_{x}\ \!\}\subseteq X.A\times\bigcup_{z\in X.A}A\{\pi_{1}\}_{z}$, where $\iota_{i}$ ($i=1,2$) are the ‘tags’ for the disjoint union $X.A$. Given a set $Y$, a relation $R\subseteq Y\times X$ and a D-relation $S\subseteq Y\times\bigcup_{y\in Y}A\{R\}_{y}$, the semi-dependent pairing of $R$ and $S$ is given by $\langle R,S\rangle\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\{(y,\iota_{1}(x))\mid(y,x)\in R\ \!\}\cup\{(y,\iota_{2}(a))\mid(y,a)\in S\ \!\}$.

$\blacktriangleright$ Example 3.2.9.

The CwD $\mathit{Mon}$ is semi-cartesian. A terminal object in $\mathit{Mon}$ or a terminal monoid is any monoid $T$ whose underlying set is singleton. Given a monoid $M$ and a D-monoid $A$ over $M$, the semi-$\Sigma$-space $M.A$ is given by $|M.A|\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\{(m,a)\mid m\in|M|,a\in A_{m}\ \!\}$, $\cdot_{M.A}:((m,a),(m^{\prime},a^{\prime}))\mapsto(m\cdot_{M}m^{\prime},a\cdot_{A}a^{\prime})$ and $e_{M.A}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}(e_{M},e_{A})$, where projections and semi-dependent pairings are the obvious ones as in $\mathit{Sets}$.

$\blacktriangleright$ Example 3.2.10.

The CwD $\mathcal{GPD}$ is semi-cartesian. A terminal object in $\mathcal{GPD}$ is any groupoid $T$ with just one object $\star$ and the identity $\mathit{id}_{\star}$. Given a groupoid $G$ and a D-groupoid $A:G\to\mathcal{GPD}$, the semi-$\Sigma$-space $G.A$ is the Grothendieck construction of $G$ and $A$, where projections and semi-dependent pairings are the obvious ones.

$\blacktriangleright$ Example 3.2.11.

The CwD $\mathit{CAT}$ is semi-cartesian in the same manner as the case of $\mathcal{GPD}$.

Just for clarity, we explicitly write down the contravariant case because the directions of morphisms in this case are slightly trickier:

$\blacktriangleright$** Definition 3.2.12**** (Contravariant semi-$\Sigma$-spaces).**

Let $\mathcal{C}$ be a contravariant CwD. A contravariant semi-$\bm{\Sigma}$-space of an object $\Gamma\in\mathcal{C}$ and a D-object $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ is an object $\Gamma.A\in\mathcal{C}$ together with a morphism $\pi_{1}:\Gamma\to\Gamma.A$ in $\mathcal{C}$, called the contravariant first projection on $\Gamma.A$, and a D-morphism $\pi_{2}:\Gamma.A\rightarrowtriangle A\{\pi_{1}\}$ in $\mathcal{C}$, called the contravariant second projection on $\Gamma.A$, such that for any $\Delta\in\mathcal{C}$, $\varphi:\Gamma\to\Delta$ and $g:\Delta\rightarrowtriangle A\{\varphi\}$ in $\mathcal{C}$ there exists a unique morphism $\langle\varphi,g\rangle:\Gamma.A\to\Delta$ in $\mathcal{C}$, called the contravariant semi-dependent pairing of $\varphi$ and $g$, that satisfies $\langle\varphi,g\rangle\circ\pi_{1}=\varphi$ and $\pi_{2}\{\langle\varphi,g\rangle\}=g$.

$\blacktriangleright$** Definition 3.2.13**** (Semi-cartesian contravariant CwDs).**

A contravariant CwD $\mathcal{C}$ is semi-cartesian iff it has a terminal object $T\in\mathcal{C}$ and a contravariant semi-$\Sigma$-space $\Gamma\stackrel{{\scriptstyle\pi_{1}}}{{\rightarrow}}\Gamma.A\stackrel{{\scriptstyle\pi_{2}}}{{\rightarrowtriangle}}A\{\pi_{1}\}$ of any pair of an object $\Gamma\in\mathcal{C}$ and a D-object $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$.

Clearly, the opposite of an SCCwD is a semi-cartesian contravariant CwD; the semi-cartesian contravariant CwDs which we shall consider occur mostly in this manner.

3.2.2 Semi-Cartesian Functors with Dependence

Next, following the general principle of category theory that morphisms are structure-preserving, let us define:

$\blacktriangleright$** Definition 3.2.14**** (SCFwDs).**

A semi-cartesian FwD (SCFwD) is an FwD $F:\mathcal{C}\to\mathcal{C^{\prime}}$ between SCCwDs $\mathcal{C}$ and $\mathcal{C^{\prime}}$ such that:

• $\blacktriangleright$

The object $F(T)\in\mathcal{C^{\prime}}$ is terminal in $\mathcal{C^{\prime}}$ for any terminal object $T\in\mathcal{C}$; and

• $\blacktriangleright$

The diagram $F(\Gamma)\stackrel{{\scriptstyle F(\pi_{1}^{\Gamma.A})}}{{\leftarrow}}F(\Gamma.A)\stackrel{{\scriptstyle F(\pi_{2}^{\Gamma.A})}}{{\rightarrowtriangle}}F(A)\{F(\pi_{1}^{\Gamma.A})\}$ in $\mathcal{C^{\prime}}$ is a semi-$\Sigma$-space in $\mathcal{C^{\prime}}$ for any semi-$\Sigma$-space $\Gamma\stackrel{{\scriptstyle\pi_{1}^{\Gamma.A}}}{{\leftarrow}}\Gamma.A\stackrel{{\scriptstyle\pi_{2}^{\Gamma.A}}}{{\rightarrowtriangle}}A\{\pi_{1}^{\Gamma.A}\}$ in $\mathcal{C}$.

If $\mathcal{C}$ and $\mathcal{C^{\prime}}$ are both strict, written $\mathcal{C}=(\mathcal{C},T,\_.\_,\pi)$ and $\mathcal{C^{\prime}}=(\mathcal{C^{\prime}},T^{\prime},\_.^{\prime}\_,\pi^{\prime})$, then $F$ is strict iff

[TABLE]

for any semi-$\Sigma$-space $\Gamma\stackrel{{\scriptstyle\pi_{1}^{\Gamma.A}}}{{\leftarrow}}\Gamma.A\stackrel{{\scriptstyle\pi_{2}^{\Gamma.A}}}{{\rightarrowtriangle}}A\{\pi_{1}^{\Gamma.A}\}$ in $\mathcal{C}$.

$\blacktriangleright$ Remark.

Note that the first projection $\pi_{1}$ is ‘fliped’ under semi-cartesian contravariant FwDs.

Let $F:\mathcal{C}\to\mathcal{C^{\prime}}$ be an SCFwD. It is easy to see that there is a unique isomorphism $\iota_{T^{\prime}}^{F(T)}:T^{\prime}\stackrel{{\scriptstyle\sim}}{{\to}}F(T)$ in $\mathcal{C^{\prime}}$ for any terminal objects $T\in\mathcal{C}$ and $T^{\prime}\in\mathcal{C^{\prime}}$, and similarly given semi-$\Sigma$-spaces $\Gamma\stackrel{{\scriptstyle\pi_{1}}}{{\leftarrow}}\Gamma.A\stackrel{{\scriptstyle\pi_{2}}}{{\rightarrowtriangle}}A\{\pi_{1}\}$ in $\mathcal{C}$ and $F(\Gamma)\stackrel{{\scriptstyle\pi_{1}^{\prime}}}{{\leftarrow}}F(\Gamma).^{\prime}F(A)\stackrel{{\scriptstyle\pi_{2}^{\prime}}}{{\rightarrowtriangle}}F(A)\{\pi_{1}^{\prime}\}$ in $\mathcal{C^{\prime}}$ there is a unique isomorphism $\iota^{F(\Gamma.A)}_{F(\Gamma).^{\prime}F(A)}:F(\Gamma).^{\prime}F(A)\stackrel{{\scriptstyle\sim}}{{\to}}F(\Gamma.A)$ in $\mathcal{C^{\prime}}$. Moreover, given that $\mathcal{C}$ and $\mathcal{C^{\prime}}$ are both strict, $F$ is strict iff these isomorphisms are all identities.

$\blacktriangleright$ Notation.

We often abbreviate the isomorphism $\iota_{T^{\prime}}^{F(T)}$ (resp. $\iota^{F(\Gamma.A)}_{F(\Gamma).^{\prime}F(A)}$) as $\iota$.

$\blacktriangleright$ Example 3.2.15.

Clearly, (resp. strict) finite-product-preserving (or cartesian) functors $\mathcal{C}\to\mathcal{D}$ coincide with (resp. strict) SCFwDs $\mathsf{D}(\mathcal{C})\to\mathsf{D}(\mathcal{D})$ for any (resp. strict) cartesian categories $\mathcal{C}$ and $\mathcal{D}$. We call this kind of (resp. strict) SCFwDs (resp. strict) cartesian functors seen as (resp. strict) SCFwDs. Thus, (resp. strict) SCFwDs are generalized (resp. strict) cartesian functors.

$\blacktriangleright$ Example 3.2.16.

Given a locally small SCCwD $\mathcal{C}$ and an object $\Delta\in\mathcal{C}$, the FwD $\mathcal{C}(\Delta,\_):\mathcal{C}\to\mathit{Sets}$ is semi-cartesian: For any semi-$\Sigma$-space $\Gamma\stackrel{{\scriptstyle\pi_{1}}}{{\leftarrow}}\Gamma.A\stackrel{{\scriptstyle\pi_{2}}}{{\rightarrowtriangle}}A\{\pi_{1}\}$ in $\mathcal{C}$, we have the semi-$\Sigma$-space

[TABLE]

in $\mathit{Sets}$, i.e., $\mathcal{C}(\Delta,\Gamma).\mathcal{C}(\Delta,A)\cong\mathcal{C}(\Delta,\Gamma.A)$, where semi-dependent pairings of $\mathcal{C}(\Delta,\Gamma.A)$ are the obvious ‘point-wise’ semi-dependent pairings in $\mathcal{C}$.

Dually, given a locally small semi-cartesian contravariant CwD $\mathcal{D}$ and $\Delta\in\mathcal{D}$, the contravariant FwD $\mathcal{D}(\_,\Delta):\mathcal{D}\to\mathit{Sets}$ is semi-cartesian: Given a contravariant semi-$\Sigma$-space $\Gamma\stackrel{{\scriptstyle\pi_{1}}}{{\rightarrow}}\Gamma.A\stackrel{{\scriptstyle\pi_{2}}}{{\rightarrowtriangle}}A\{\pi_{1}\}$ in $\mathcal{D}$, we have the semi-$\Sigma$-space

[TABLE]

in $\mathit{Sets}$, i.e., $\mathcal{D}(\Gamma,\Delta).\mathcal{C}(A,\Delta)\cong\mathcal{C}(\Gamma.A,\Delta)$, where semi-dependent pairings of $\mathcal{C}(\Gamma.A,\Delta)$ are again the ‘point-wise’ contravariant semi-dependent pairings in $\mathcal{D}$.

The following lemma generalizes well-known properties of cartesian functors:

$\blacktriangleright$** Lemma 3.2.17**** (SCFwD-lemma).**

Let $F:\mathcal{C}\to\mathcal{D}$ be an SCFwD, and $\Gamma,\Delta\in\mathcal{C}$, $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$, $B\in\mathscr{D}_{\mathcal{C}}(\Delta)$, $\phi:\Delta\to\Gamma$, $g:\Delta\rightarrowtriangle A\{\phi\}$ and $h:\Delta.B\rightarrowtriangle A\{\phi\circ\pi_{1}^{\Delta.B}\}$ in $\mathcal{C}$. Then, we have:

$F(\pi_{1}^{\Gamma.A})\circ\iota^{F(\Gamma.A)}_{F(\Gamma).F(A)}=\pi_{1}^{F(\Gamma).F(A)}:F(\Gamma).F(A)\to F(\Gamma)$; 2. 2.

$F(\pi_{2}^{\Gamma.A})\{\iota^{F(\Gamma.A)}_{F(\Gamma).F(A)}\}=\pi_{2}^{F(\Gamma).F(A)}:F(\Gamma).F(A)\rightarrowtriangle F(A)\{\pi_{1}^{F(\Gamma).F(A)}\}$; 3. 3.

$F(\langle\phi,g\rangle)=\iota^{F(\Gamma.A)}_{F(\Gamma).F(A)}\circ\langle F(\phi),F(g)\rangle:F(\Delta)\to F(\Gamma.A)$; and 4. 4.

$(\iota^{F(\Gamma.A)}_{F(\Gamma).F(A)})^{-1}\circ F(\langle\phi\circ\pi_{1}^{\Delta.B},h\rangle)\circ\iota^{F(\Delta.B)}_{F(\Delta).F(B)}=\langle F(\phi)\circ\pi_{1}^{F(\Delta).F(B)},F(h)\{\iota^{F(\Delta.B)}_{F(\Delta).F(B)}\}\rangle:F(\Delta).F(B)\to F(\Gamma).F(A)$.

Proof.

The equations 1 and 2 follow from the definition of the canonical isomorphism $\iota^{F(\Gamma.A)}_{F(\Gamma).F(A)}:F(\Gamma).F(A)\stackrel{{\scriptstyle\sim}}{{\to}}F(\Gamma.A)$, i.e., $\iota^{F(\Gamma.A)}_{F(\Gamma).F(A)}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\langle F(\pi_{1}^{\Gamma.A}),F(\pi_{2}^{\Gamma.A})\rangle^{-1}$, and for the equation 3 we have:

[TABLE]

as well as:

[TABLE]

Hence, by the universal property of semi-dependent pairings, we may conclude that

[TABLE]

whence $F(\langle\phi,g\rangle)=\iota^{F(\Gamma.A)}_{F(\Gamma).F(A)}\circ\langle F(\phi),F(g)\rangle:F(\Delta)\to F(\Gamma.A)$, establishing the equation 3.

Finally, the equation 4 is an immediate corollary of the equations 1 and 3. ∎

3.2.3 Natural Transformations with Dependence

Note that the additional semi-cartesian structure on SCCwDs $\mathcal{C}$ enables us to define a morphism between D-objects $D\in\mathscr{D}_{\mathcal{C}}(\Delta)$ and $C\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ to be a pair $(\phi,f)$ of a morphism $\phi:\Delta\to\Gamma$ and a D-morphism $f:\Delta.D\rightarrowtriangle C\{\phi\circ\pi_{1}\}$ in $\mathcal{C}$. Based on this idea, it seems a reasonable idea to define a morphism between SCFwDs $F,G:\mathcal{C}\to\mathcal{D}$ to be a pair $(\eta,t)$ of a family $\eta=(\eta_{\Gamma})_{\Gamma\in\mathcal{C}}$ of morphisms $\eta_{\Gamma}:F(\Gamma)\to G(\Gamma)$ in $\mathcal{D}$ and a family $t=(t_{\Gamma,A})_{\Gamma\in\mathcal{C},A\in\mathscr{D}_{\mathcal{C}}(\Gamma)}$ of D-morphisms $t_{\Gamma,A}:F(\Gamma).F(A)\rightarrowtriangle G(A)\{\eta_{\Gamma}\circ\pi_{1}\}$ in $\mathcal{D}$ such that the diagrams {diagram} commute for any $\Gamma,\Delta\in\mathcal{C}$, $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$, $B\in\mathscr{D}_{\mathcal{C}}(\Delta)$, $\varphi:\Gamma\to\Delta$ and $g:\Gamma.A\rightarrowtriangle B\{\varphi\circ\pi_{1}\}$ in $\mathcal{C}$.

Nevertheless, this concept turns out to be too general as morphisms between SCFwDs. For instance, such morphisms between cartesian functors seen as SCFwDs do not coincide with natural transformations, and Theorem 4.3.7 would not hold if we adopted them as morphisms between SCFwDs.

Fortunately, however, the right one is simpler:

$\blacktriangleright$** Definition 3.2.18**** (NTwDs).**

A natural transformation with dependence (NTwD) between SCFwDs $F,G:\mathcal{C}\to\mathcal{D}$ is a pair $(\eta,t)$ of a family $\eta=(\eta_{\Gamma})_{\Gamma\in\mathcal{C}}$ of morphisms $\eta_{\Gamma}:F(\Gamma)\to G(\Gamma)$ in $\mathcal{D}$ and a family $t=(t_{\Gamma,A})_{\Gamma\in\mathcal{C},A\in\mathscr{D}_{\mathcal{C}}(\Gamma)}$ of D-morphisms $t_{\Gamma,A}:F(\Gamma).F(A)\rightarrowtriangle G(A)\{\eta_{\Gamma}\circ\pi_{1}\}$ in $\mathcal{D}$ such that $\eta$ forms a natural transformation (NT) $\mathscr{U}(F)\Rightarrow\mathscr{U}(G):\mathscr{U}(\mathcal{C})\to\mathscr{U}(\mathcal{D})$, and the pair is coherent in the sense that for any $\Gamma,\Delta\in\mathcal{C}$, $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$, $B\in\mathscr{D}_{\mathcal{C}}(\Delta)$, $\varphi:\Gamma\to\Delta$ and $g:\Gamma.A\rightarrowtriangle B\{\varphi\circ\pi_{1}\}$ in $\mathcal{C}$ it satisfies the equation

[TABLE]

where the semi-$\Sigma$-spaces $\Gamma.A\in\mathcal{C}$ and $G(\Gamma).G(A)\in\mathcal{D}$ are arbitrary.

Let us see that the coherence axiom (8) makes the diagram {diagram} commutes for any $\Gamma,\Delta\in\mathcal{C}$, $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$, $B\in\mathscr{D}_{\mathcal{C}}(\Delta)$, $\varphi:\Gamma\to\Delta$ and $g:\Gamma.A\rightarrowtriangle B\{\varphi\circ\pi_{1}\}$ in $\mathcal{C}$. First, by the coherence of $(\eta,t)$ and the naturality of $\eta$, we have:

[TABLE]

as well as:

[TABLE]

whence it suffices to show:

[TABLE]

Then, by the naturality of $\eta$, we have:

[TABLE]

and thus, it is immediate that:

[TABLE]

Next, note that NTwDs $(\eta,t)$ between strict SCFwDs $F,G:\mathcal{C}\to\mathcal{D}$ are essentially NTs $\eta:\mathscr{U}(F)\Rightarrow\mathscr{U}(G):\mathscr{U}(\mathcal{C})\to\mathscr{U}(\mathcal{D})$ because $t$ may be completely recovered from $\eta$ by the equation $t_{\Gamma,A}=\pi_{2}\{\eta_{\Gamma.A}\}$ for any $\Gamma\in\mathcal{C}$ and $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$. This point plays an essential role for the commutative diagram in the proof of Theorem 4.3.7.

$\blacktriangleright$ Notation.

We write $(\eta,t):F\Rightarrow G$ to mean that the pair $(\eta,t)$ is an NTwD from an SCCwD $F$ to another $G$, or even $(\eta,t):F\Rightarrow G:\mathcal{C}\to\mathcal{D}$ if we would like to indicate $F,G:\mathcal{C}\to\mathcal{D}$.

We skip describing contravariant NTwDs explicitly because now it should be clear for the reader what they are. More generally, we shall focus on covariant cases in the rest of the paper.

$\blacktriangleright$ Example 3.2.19.

An NT $\eta:F\Rightarrow G:\mathcal{C}\to\mathcal{D}$ gives rise to an NTwD $\mathsf{D}(\eta)\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}(\eta,t(\eta)):\mathsf{D}(F)\Rightarrow\mathsf{D}(G):\mathsf{D}(\mathcal{C})\to\mathsf{D}(\mathcal{D})$ by $t(\eta)_{\Gamma,A}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\eta_{A}\circ\pi_{2}^{F(\Gamma).F(A)}$ for all $\Gamma\in\mathcal{C}$ and $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$, as well as another $\mathsf{d}(\eta)\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}(\eta,\emptyset):\mathsf{d}(F)\Rightarrow\mathsf{d}(G):\mathsf{d}(\mathcal{C})\to\mathsf{d}(\mathcal{D})$. We call the first kind NTs seen as NTwDs. Conversely, an NTwD $(\epsilon,s):J\Rightarrow K:\mathcal{L}\to\mathcal{R}$ such that $J$ and $K$ are cartesian functors seen as SCFwDs and $s_{\Gamma,A}=\epsilon_{A}\circ\pi_{2}^{F(\Gamma).F(A)}$ for all $\Gamma\in\mathcal{L}$ and $A\in\mathscr{D}_{\mathcal{L}}(\Gamma)$ coincides with an NT. Hence, NTwDs are a generalization of NTs.

$\blacktriangleright$ Example 3.2.20.

Given a locally small SCCwD $\mathcal{C}$ and a morphism $\phi:\Delta\to\Gamma$ in $\mathcal{C}$, we may give an NTwD $(\eta(\phi),t(\phi)):\mathcal{C}(\Gamma,\_)\Rightarrow\mathcal{C}(\Delta,\_):\mathcal{C}\to\mathit{Sets}$ by defining for any $\Theta\in\mathcal{C}$ and $C\in\mathscr{D}_{\mathcal{C}}(\Theta)$

[TABLE]

Note that $\eta(\phi)_{\Theta}$ maps each morphism $\varphi:\Gamma\to\Theta$ in $\mathcal{C}$ to the morphism $\varphi\circ\phi:\Delta\to\Theta$ in $\mathcal{C}$, and $t(\phi)_{\Theta,C}$ maps each pair $(\varphi,g)\in\mathcal{C}(\Gamma,\Theta).\mathcal{C}(\Gamma,C)$ to the D-morphism $g\{\phi\}\in\mathscr{D}_{\mathcal{C}}(\Delta,C\{\varphi\}\{\phi\})$ in $\mathcal{C}$. It is easy to see that the pair $(\eta(\phi),t(\phi))$ satisfies the required naturality condition.

Similarly to the case of NTs, it is straightforward to define vertical composition of NTwDs:

$\blacktriangleright$** Definition 3.2.21**** (Vertical composition of NTwDs).**

The vertical composition $(\epsilon,s)\circ(\eta,t):F\Rightarrow H:\mathcal{C}\to\mathcal{D}$ of NTwDs $(\eta,t):F\Rightarrow G:\mathcal{C}\to\mathcal{D}$ and $(\epsilon,s):G\Rightarrow H:\mathcal{C}\to\mathcal{D}$ is given by:

[TABLE]

Note that the vertical composition on the first components is just the conventional vertical composition on NTs. It is easy to see that vertical composition of NTwDs is well-defined:

$\blacktriangleright$** Proposition 3.2.22**** (Well-defined VC of NTwDs).**

NTwDs are closed under vertical composition.

Proof.

It suffices to show that the coherence 8 is preserved under vertical composition. Let $(\eta,t):F\Rightarrow G:\mathcal{C}\to\mathcal{D}$ and $(\epsilon,s):G\Rightarrow H:\mathcal{C}\to\mathcal{D}$ be NTwDs. Then, we have:

[TABLE]

for any $\Gamma\in\mathcal{C}$ and $A\in\mathscr{D}_{\mathcal{C}}(\gamma)$, which establishes the coherence 8 on the vertical composition $(\epsilon,s)\circ(\eta,t)=(\epsilon\circ\eta,s\circ t)$. ∎

As one may have already expected, we also have horizontal composition of NTwDs:

$\blacktriangleright$** Definition 3.2.23**** (Horizontal composition of NTwDs).**

The horizontal composition $(\eta^{\prime},t^{\prime})\odot(\eta,t):F^{\prime}\circ F\Rightarrow G^{\prime}\circ G:\mathcal{C}\to\mathcal{E}$ of NTwDs $(\eta,t):F\Rightarrow G:\mathcal{C}\to\mathcal{D}$ and $(\eta^{\prime},t^{\prime}):F^{\prime}\Rightarrow G^{\prime}:\mathcal{D}\to\mathcal{E}$ is given by:

[TABLE]

Again, note that the horizontal composition on the first components is just the horizontal composition on NTs. It is not hard to see that horizontal composition on NTwDs is well-defined:

$\blacktriangleright$** Proposition 3.2.24**** (Well-defined HC of NTwDs).**

NTwDs are closed under horizontal composition.

Proof.

Let $(\eta,t):F\Rightarrow G:\mathcal{C}\to\mathcal{D}$ and $(\eta^{\prime},t^{\prime}):F^{\prime}\Rightarrow G^{\prime}:\mathcal{D}\to\mathcal{E}$ be NTwDs. We show that horizontal composition $(\eta^{\prime},t^{\prime})\odot(\eta,t):F^{\prime}\circ F\Rightarrow G^{\prime}\circ G:\mathcal{C}\to\mathcal{E}$ satisfies the coherence (8):

[TABLE]

for any $\Gamma\in\mathcal{C}$ and $A\in\mathscr{D}_{\mathcal{C}}(\gamma)$, completing the proof. ∎

3.2.4 The 2-Category of Semi-Cartesian Categories with Dependence

We are now ready to define the 2-category of small SCCwDs, SCFwDs and NTwDs. Let us first define the following preliminary concept:

$\blacktriangleright$** Definition 3.2.25**** (SCFwD-categories).**

Given SCCwDs $\mathcal{C}$ and $\mathcal{D}$, the category $[\mathcal{C},\mathcal{D}]$, called the SCFwD-category from $\mathcal{C}$ to $\mathcal{D}$ is given by:

• $\blacktriangleright$

Objects are SCFwDs $\mathcal{C}\to\mathcal{D}$;

• $\blacktriangleright$

Morphisms $F\to G$ are NTwDs $F\Rightarrow G$;

• $\blacktriangleright$

The composition $F\stackrel{{\scriptstyle(\eta,t)}}{{\to}}G\stackrel{{\scriptstyle(\epsilon,s)}}{{\to}}H$ is the vertical composition $(\epsilon,s)\circ(\eta,t)$; and

• $\blacktriangleright$

The identity $\mathit{id}_{F}$ is the pair $((\mathit{id}_{F(\Gamma)})_{\Gamma\in\mathcal{C}},(\pi_{2}^{F(\Gamma).F(A)})_{\Gamma\in\mathcal{C},A\in\mathscr{D}_{\mathcal{C}}(\Gamma)})$.

It is easy to see that SCFwD-categories are well-defined. We are now ready to define:

$\blacktriangleright$** Definition 3.2.26**** (The 2-category $\mathbb{SCC_{D}}$).**

The 2-category $\mathbb{SCC_{D}}$ is defined by:

• $\blacktriangleright$

0-cells (or objects) are small SCCwDs;

• $\blacktriangleright$

Given 0-cells $\mathcal{C}$ and $\mathcal{D}$, the hom-category $\mathbb{SCC_{D}}(\mathcal{C},\mathcal{D})$ is the SCFwD-category $[\mathcal{C},\mathcal{D}]$;

• $\blacktriangleright$

Given 0-cells $\mathcal{C}$, $\mathcal{D}$ and $\mathcal{E}$, the composition functor $[\mathcal{C},\mathcal{D}]\times[\mathcal{D},\mathcal{E}]\to[\mathcal{C},\mathcal{E}]$ maps

[TABLE]

for all $F,G\in[\mathcal{C},\mathcal{D}]$, $F^{\prime},G^{\prime}\in[\mathcal{D},\mathcal{E}]$, $(\eta,t)\in[\mathcal{C},\mathcal{D}](F,G)$ and $(\eta^{\prime},t^{\prime})\in[\mathcal{D},\mathcal{E}](F^{\prime},G^{\prime})$; and

• $\blacktriangleright$

Given a 0-cell $\mathcal{C}$, the functor $1\to[\mathcal{C},\mathcal{C}]$ maps

[TABLE]

where $\star$ is the unique object of the terminal category $1$.

$\blacktriangleright$** Theorem 3.2.27**** (Well-defined $\mathbb{SCC_{D}}$).**

The structure $\mathbb{SCC_{D}}$ in fact forms a 2-category.

Proof.

Let us just show that $\mathbb{SCC_{D}}$ satisfies the interchange law since the other axioms are easier to verify. Let $\mathcal{C}$, $\mathcal{D}$ and $\mathcal{E}$ be SCCwDs, $F,G,H:\mathcal{C}\to\mathcal{D}$ and $F^{\prime},G^{\prime},H^{\prime}:\mathcal{D}\to\mathcal{E}$ SCFwDs, and $(\eta,t):F\Rightarrow G$, $(\epsilon,s):G\Rightarrow H$, $(\eta^{\prime},t^{\prime}):F^{\prime}\Rightarrow G^{\prime}$ and $(\epsilon^{\prime},s^{\prime}):G^{\prime}\Rightarrow H^{\prime}$ NTwDs. We have to establish the equation:

[TABLE]

which is equivalent to:

[TABLE]

which is reduced to:

[TABLE]

because the equation of the first components is just the well-known interchange law for the 2-category $\mathit{CAT}$ of small categories, functors and NTs.

Then, observe that:

[TABLE]

for all $\Gamma\in\mathcal{C}$ and $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$, which establishes the equation (9). ∎

By this 2-categorical structure of small SCCwDs, we may employ the notions of adjunctions and equivalences between 0-cells in an arbitrary 2-category to define adjunctions and equivalences between small SCCwDs. Clearly, we may unpack these definitions and define adjunctions and equivalences between large SCCwDs as well.

3.2.5 Categories of Dependent Objects

This section introduces a 2-functor $(\_)_{\mathscr{D}}:\mathbb{SCC_{D}}\to\mathit{CAT}$, which will turn out to be very useful for the rest of the paper.

Let us begin with the operation on 0-cells:

$\blacktriangleright$** Definition 3.2.28**** (Categories of D-objects).**

Given an SCCwD $\mathcal{C}$, the category of D-objects in $\mathcal{C}$ is the category $\mathcal{C}_{\mathscr{D}}$ given by:

• $\blacktriangleright$

$\mathsf{ob}(\mathcal{C}_{\mathscr{D}})\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\{(\Gamma,C)\mid\Gamma\in\mathcal{C},C\in\mathscr{D}_{\mathcal{C}}(\Gamma)\ \!\}$;

• $\blacktriangleright$

$\mathcal{C}_{\mathscr{D}}((\Delta,D),(\Gamma,C))\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\{(\phi,f)\mid\phi\in\mathcal{C}(\Delta,\Gamma),f\in\mathscr{D}_{\mathcal{C}}(\Delta.D,C\{\phi\circ\pi_{1}\})\ \!\}$;

• $\blacktriangleright$

$(\Delta,D)\stackrel{{\scriptstyle(\phi,f)}}{{\to}}(\Gamma,C)\stackrel{{\scriptstyle(\psi,g)}}{{\to}}(\Theta,E)\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}(\psi\circ\phi,g\{\langle\phi\circ\pi_{1},f\rangle\}_{\mathcal{C}})$;

• $\blacktriangleright$

$\mathit{id}_{(\Gamma,C)}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}(\mathit{id}_{\Gamma},\pi_{2})$.

It is straightforward to check that $\mathcal{C}_{\mathscr{D}}$ is a well-defined category for any SCCwD $\mathcal{C}$, and there is the obvious forgetful functor $p_{\mathcal{C}}:\mathcal{C}_{\mathscr{D}}\to\mathcal{C}$. This construction may be seen as a categorical abstraction of the syntactic comprehension category of a DTT [Jac99].

Note that each morphism $(\phi,f):(\Delta,D)\to(\Gamma,C)$ in $\mathcal{C}_{\mathscr{D}}$ induces a morphism $\langle\phi\circ\pi_{1},f\rangle:\Delta.D\to\Gamma.C$ in $\mathcal{C}$; however, we have not taken $\langle\phi\circ\pi_{1},f\rangle$ as a morphism $(\Delta,D)\to(\Gamma,C)$ in $\mathcal{C}_{\mathscr{D}}$ since otherwise we cannot define the composition of these morphisms as given above (as semi-$\Sigma$-spaces are unique only up to isomorphisms).

Next, let us lift this construction to SCFwDs as follows:

$\blacktriangleright$** Definition 3.2.29**** (Functors between categories of D-objects).**

Each SCFwD $F:\mathcal{C}\to\mathcal{D}$ induces the functor $F_{\mathscr{D}}:\mathcal{C}_{\mathscr{D}}\to\mathcal{D}_{\mathscr{D}}$ that maps each object $(\Delta,D)\in\mathcal{C}_{\mathscr{D}}$ to the object $(F(\Delta),F(D))\in\mathcal{D}_{\mathscr{D}}$ and each morphism $(\phi,f)$ in $\mathcal{C}_{\mathscr{D}}$ to the morphism $(F(\phi),F(f)\{\iota^{F(\Delta.D)}_{F(\Delta).F(D)}\})$ in $\mathcal{D}_{\mathscr{D}}$.

By the equation 4 in Lemma 3.2.17 (for the preservation of composition), it is easy to see that the functor $F_{\mathscr{D}}:\mathcal{C}_{\mathscr{D}}\to\mathcal{D}_{\mathscr{D}}$ is well-defined for any SCFwD $F:\mathcal{C}\to\mathcal{D}$.

It is even simpler for the case of NTwDs:

$\blacktriangleright$** Definition 3.2.30**** (NTwDs as NTs).**

An NTwD $(\eta,t):F\Rightarrow G:\mathcal{C}\to\mathcal{D}$ gives rise to an NT $(\eta,t)_{\mathscr{D}}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}(\eta_{\Gamma},t_{\Gamma,A})_{(\Gamma,A)\in\mathcal{C}_{\mathscr{D}}}:F_{\mathscr{D}}\Rightarrow G_{\mathscr{D}}:\mathcal{C}_{\mathscr{D}}\to\mathcal{D}_{\mathscr{D}}$.

It is easy to see that this construction $(\_)_{\mathscr{D}}$ on NTwDs is well-defined. It in essence implies that an NTwD $(\eta,t):F\Rightarrow G:\mathcal{C}\to\mathcal{D}$ can be seen as an NT $(\eta,t)_{\mathscr{D}}:F_{\mathscr{D}}\Rightarrow G_{\mathscr{D}}:\mathcal{C}_{\mathscr{D}}\to\mathcal{D}_{\mathscr{D}}$ such that components of $\eta$ do not depend on D-objects of $\mathcal{C}$, where the two commutative diagrams {diagram} for $(\eta,t)$ in $\mathcal{D}$ is unified into the following commutative diagram {diagram} in $\mathcal{D}_{\mathscr{D}}$ for any $\Gamma,\Delta\in\mathcal{C}$, $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$, $B\in\mathscr{D}_{\mathcal{C}}(\Delta)$, $\varphi:\Gamma\to\Delta$ and $g:\Gamma.A\rightarrowtriangle B\{\varphi\circ\pi_{1}\}$ in $\mathcal{C}$.

Thus, we may just apply known results on NTs to NTwDs; for instance:

$\blacktriangleright$** Lemma 3.2.31**** (Naturality of vertical inverses of NTwDs).**

Given an NTwD $(\eta,t):F\Rightarrow G:\mathcal{C}\to\mathcal{D}$, if a pair $(\epsilon,s)$ of a family $\epsilon=(\epsilon_{\Gamma})_{\Gamma\in\mathcal{C}}$ of morphisms $\epsilon_{\Gamma}:G(\Gamma)\to F(\Gamma)$ in $\mathcal{D}$ and a family $s=(s_{\Gamma,A})_{\Gamma\in\mathcal{C},A\in\mathscr{D}_{\mathcal{C}}(\Gamma)}$ of D-morphisms $s_{\Gamma,A}:G(\Gamma).G(A)\rightarrowtriangle F(A)\{\epsilon_{\Gamma}\circ\pi_{1}\}$ in $\mathcal{D}$ satisfies the equations

[TABLE]

for all $\Gamma\in\mathcal{C}$ and $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$, then the pair $(\epsilon,s)$ is an NTwD $G\Rightarrow F$.

Now, let us summarize the constructions $(\_)_{\mathscr{D}}$ given so far as follows:

$\blacktriangleright$** Definition 3.2.32**** (The 2-functor $(\_)_{\mathscr{D}}$).**

The 2-functor $(\_)_{\mathscr{D}}:\mathbb{SCC_{D}}\to\mathit{CAT}$ is given by $\mathcal{C}\mapsto\mathcal{C}_{\mathscr{D}}$ for small SCCwDs $\mathcal{C}$, $F\mapsto F_{\mathscr{D}}$ for SCFwDs $F$ and $(\eta,t)\mapsto(\eta,t)_{\mathscr{D}}$ for NTwDs $(\eta,t)$.

$\blacktriangleright$** Proposition 3.2.33**** (Well-defined $(\_)_{\mathscr{D}}$).**

The map $(\_)_{\mathscr{D}}$ is in fact a 2-functor $\mathbb{SCC_{D}}\to\mathit{CAT}$.

Proof.

It suffices to show that $(\_)_{\mathscr{D}}$ preserves composition and identities. We first show the preservation of composition of 1-cells. Let $\mathcal{C}$, $\mathcal{D}$ and $\mathcal{E}$ be SCCwDs. Given SCFwDs $F:\mathcal{C}\to\mathcal{D}$ and $G:\mathcal{D}\to\mathcal{E}$, the object-maps of $(G\circ F)_{\mathscr{D}}$ and $G_{\mathscr{D}}\circ F_{\mathscr{D}}$ clearly coincide. For their arrow-maps, consider any morphism $(\phi,f):(\Delta,D)\to(\Gamma,C)$ in $\mathcal{C}$; then, we have:

[TABLE]

where it is easy to show $\iota^{G\circ F(\Delta.D)}_{G\circ F(\Delta).G\circ F(D)}=G(\iota^{F(\Delta.D)}_{F(\Delta).F(D)})\circ\iota^{G(F(\Delta).F(D))}_{G(F(\Delta)).G(F(D))}$ by the equations 1, 2 and 3 of Lemma 3.2.17. Hence, we have shown that $(G\circ F)_{\mathscr{D}}=G_{\mathscr{D}}\circ F_{\mathscr{D}}$. Finally, the preservation of 1-cell identities is immediate, and the preservations of vertical and horizontal compositions of 2-cells, and of vertical and horizontal 2-cell identities are rather trivial. ∎

Given an SCCwD $\mathcal{C}$ and an object $\Gamma\in\mathcal{C}$, we have the subcategory of $\mathcal{C}_{\mathscr{D}}$ whose objects are pairs $(\Gamma,C)$ and morphisms are pairs $(\mathit{id}_{\Gamma},f)$, where $C$ and $f$ vary, but $\Gamma$ is fixed. Then, we may focus on the second components of such pairs, which is equivalent to the following category:

$\blacktriangleright$** Definition 3.2.34**** (Categories of fixed objects).**

Given an SCCwD $\mathcal{C}$ and an object $\Gamma\in\mathcal{C}$, the category of a fixed object $\Gamma$ on $\mathcal{C}$ is the category $\mathcal{C}_{\Gamma}$ given by:

• $\blacktriangleright$

$\mathsf{ob}(\mathcal{C}_{\Gamma})\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\mathscr{D}_{\mathcal{C}}(\Gamma)$;

• $\blacktriangleright$

$\mathcal{C}_{\Gamma}(A,B)\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\mathscr{D}_{\mathcal{C}}(\Gamma.A,B\{\pi_{1}\})$;

• $\blacktriangleright$

$A\stackrel{{\scriptstyle f}}{{\to}}B\stackrel{{\scriptstyle g}}{{\to}}C\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}g\{\langle\pi_{1},f\rangle\}$; and

• $\blacktriangleright$

$\mathit{id}_{(\Gamma,A)}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\pi_{2}$.

This structure will be essential when we prove that our generalizations of binary products and exponentials are certain adjoints, and thus they are unique up to isomorphisms.

3.2.6 Isomorphisms between Dependent Objects

Next, we define isomorphisms between D-objects as promised before:

$\blacktriangleright$** Definition 3.2.35**** (Isomorphisms between D-objects).**

Let $\mathcal{C}$ be an SCCwD. Given $\Gamma,\Delta\in\mathcal{C}$, $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ and $B\in\mathscr{D}_{\mathcal{C}}(\Delta)$, an isomorphism between $A$ and $B$ is an isomorphism $(\Gamma,A)\stackrel{{\scriptstyle\sim}}{{\to}}(\Delta,B)$ in $\mathcal{C}_{\mathscr{D}}$. We call $A$ and $B$ isomorphic and write $A\cong B$ iff there is an isomorphism between them.

It is easy to see that an inverse of an isomorphism between D-objects is unique.

$\blacktriangleright$ Example 3.2.36.

In the SCCwD $\mathit{Sets}$, D-sets $A\in\mathscr{D}_{\mathit{Sets}}(X)$ and $B\in\mathscr{D}_{\mathit{Sets}}(Y)$ are isomorphic iff there is a bijection $\varphi:X\stackrel{{\scriptstyle\sim}}{{\to}}Y$, and the sets $A_{x}$ and $B_{\varphi(x)}$ are bijective for each $x\in X$.

Note that it is a fundamental property of functors to preserve isomorphisms between objects. Similarly, SCFwDs preserve isomorphisms between D-objects as well:

$\blacktriangleright$** Proposition 3.2.37**** (Preservation of isomorphisms between D-objects under SCFwDs).**

SCFwDs preserve isomorphisms between D-objects.

Proof.

Let $F:\mathcal{C}\to\mathcal{D}$ be an SCFwD, and $(\phi,f):(\Delta,D)\stackrel{{\scriptstyle\sim}}{{\to}}(\Gamma,C)$ in $\mathcal{C}_{\mathscr{D}}$. Let $(\psi,g)$ be the inverse of $(\phi,f)$, i.e., $\psi\circ\phi=\mathit{id}_{\Delta}$, $\phi\circ\psi=\mathit{id}_{\Gamma}$, $g\{\langle\phi\circ\pi_{1},f\rangle\}=\pi_{2}$ and $f\{\langle\psi\circ\pi_{1},g\rangle\}=\pi_{2}$. It suffices to establishes the isomorphisms $(F(\phi),F(f)\{\iota\}):(F(\Delta),F(B))\cong(F(\Gamma),F(A)):(F(\psi),F(g)\{\iota\})$ in $\mathcal{D}_{\mathscr{D}}$. Clearly, $F(\psi)\circ F(\phi)=F(\psi\circ\phi)=F(\mathit{id}_{\Delta})=\mathit{id}_{F(\Delta)}$; and we have:

[TABLE]

Similarly, we have $F(\phi)\circ F(\psi)=\mathit{id}_{F(\Gamma)}$ and $F(f)\{\iota\}\{\langle F(\psi)\circ\pi_{1},F(g)\{\iota\}\rangle\}=\pi_{2}$, which completes the proof. ∎

3.3 Cartesian Categories and Functors with Dependence

We have seen in the last section that strict SCCwDs are CwFs, and thus they give a semantics of MLTTs yet without any specific type constructions. In this section, we give a generalization of terminal objects and semi-$\Sigma$-spaces, called unit D-objects and $\Sigma$-spaces, which respectively interpret $\mathsf{1}$- and $\mathsf{\Sigma}$-types in MLTTs. We also introduce SCFwDs that preserve these structures.

3.3.1 Cartesian Categories with Dependence

A naive idea to interpret $\mathsf{1}$-types is to employ D-objects that are to be called terminal. Note that we may define limits for D-objects and D-morphisms in any SCCwD $\mathcal{C}$ to be just limits in the category $\mathcal{C}_{\mathscr{D}}$. Therefore, we may define:

$\blacktriangleright$** Definition 3.3.1**** (Terminal and initial D-objects).**

A D-object $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ in an SCCwD $\mathcal{C}$ is terminal (resp. initial) iff so is the pair $(\Gamma,A)$ in the category $\mathcal{C}_{\mathscr{D}}$.

Since a terminal (resp. initial) D-object in an SCCwD is unique up to isomorphisms, we may call it the terminal (resp. initial) D-object.

Notice, however, that terminal D-objects cannot interpret $\mathsf{1}$-type because their universal property does not exactly match the uniqueness rule $1$-Uniq. Thus, we introduce:

$\blacktriangleright$** Definition 3.3.2**** (Unit D-objects).**

A D-object $1\in\mathscr{D}_{\mathcal{C}}(T)$ in an SCCwD $\mathcal{C}$ is unit iff $T\in\mathcal{C}$ is a terminal object in $\mathcal{C}$, and there is a unique D-morphism $\bm{!}_{\Gamma}:\Gamma\rightarrowtriangle 1\{!_{\Gamma}\}$222Note the notational difference between $!_{\Gamma}$ and $\bm{!}_{\Gamma}$. for each object $\Gamma\in\mathcal{C}$.

$\blacktriangleright$ Example 3.3.3.

In a cartesian category $\mathcal{C}$ seen as an SCCwD $\mathsf{D}(\mathcal{C})$, a terminal object $T$ over itself is also a unit D-object.

$\blacktriangleright$** Proposition 3.3.4**** (Uniqueness of unit D-objects).**

Unit D-objects are unique up to isomorphisms.

Proof.

Let $1\in\mathscr{D}_{\mathcal{C}}(T)$ and $1^{\prime}\in\mathscr{D}_{\mathcal{C}}(T^{\prime})$ be both unit D-objects in an SCCwD $\mathcal{C}$. Then, we have $(!_{T^{\prime}},\bm{!}_{1^{\prime}}):(T,1)\cong(T^{\prime},1^{\prime}):(!_{T},\bm{!}_{1})$ in the category $\mathcal{C}_{\mathscr{D}}$, i.e., $1\cong 1^{\prime}$ in $\mathcal{C}$. ∎

It is almost immediate by the definition that unit D-objects capture $\mathsf{1}$-type in MLTTs:

$\blacktriangleright$** Theorem 3.3.5**** (Unit D-objects interpret the $\mathsf{1}$-type).**

A strict SCCwD equipped with a unit D-object gives rise to a CwF that supports $\mathsf{1}$-type in the strict sense.

Proof.

Let $\mathcal{C}$ be a strict SCCwD equipped with a unit D-object $1\in\mathscr{D}_{\mathcal{C}}(T)$. For each object $\Gamma\in\mathcal{C}$, we define $1_{\Gamma}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}1\{!_{\Gamma}\}\in\mathscr{D}_{\mathcal{C}}(\Gamma)$, which interprets the rule Unit-Intro. Then, it is clear how the remaining axioms for a CwF $\mathcal{C}$ that supports $1$-type in the strict sense are satisfied. ∎

Note that unit D-objects are terminal, but not necessarily vice versa. In fact, this pattern will occur repeatedly: Limits in the category of D-objects $\mathcal{C}_{\mathscr{D}}$ on an SCCwD $\mathcal{C}$ in general do not give interpretations of type constructions of MLTTs in $\mathcal{C}$, but their stronger version does.

Next, let us consider (binary) products of D-objects. However, if we define the binary product of D-objects $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ and $B\in\mathscr{D}_{\mathcal{C}}(\Gamma.A)$ in an SCCwD $\mathcal{C}$ as the binary product $(\Gamma,A)\times(\Gamma.A,B)$ in the category $\mathcal{C}_{\mathscr{D}}$, then it would be a D-object $A\times B\in\mathscr{D}_{\mathcal{C}}(\Gamma\times\Gamma.A)$ in $\mathcal{C}$, which does not match the rule $\mathsf{\Sigma}$-Form. Instead, what we need to interpret $\mathsf{\Sigma}$-types is the following:

$\blacktriangleright$** Definition 3.3.6**** ($\Sigma$-spaces).**

Let $\mathcal{C}$ be an SCCwD. Given $\Gamma\in\mathcal{C}$, $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ and $B\in\mathscr{D}_{\mathcal{C}}(\Gamma.A)$, a dependent pair ($\bm{\Sigma}$-) space of $A$ and $B$ in $\mathcal{C}$ is a D-object $\Sigma(A,B)\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ together with D-morphisms

[TABLE]

in $\mathcal{C}$, called the first and second projections of $\Sigma(A,B)$, respectively, such that for any $\phi:\Delta\to\Gamma$, $g:\Delta\rightarrowtriangle A\{\phi\}$ and $h:\Delta\rightarrowtriangle B\{\langle\phi,g\rangle\}$ in $\mathcal{C}$ there exists a unique D-morphism

[TABLE]

in $\mathcal{C}$, called the dependent pairing of $g$ and $h$, that satisfies

[TABLE]

$\blacktriangleright$ Notation.

We often omit the superscript $\Sigma(A,B)$ on $\varpi_{i}^{\Sigma(A,B)}$ ($i=1,2$).

The universal property of a dependent pairing $\Lbag g,h\Rbag:\Delta\rightarrowtriangle\Sigma(A,B)\{\phi\}$ may be described as the following commutative diagram: {diagram}

$\blacktriangleright$** Proposition 3.3.7**** (Uniqueness of $\Sigma$-spaces).**

$\Sigma$-spaces are unique up to isomorphisms.

Proof.

Similar to the proof of the uniqueness of semi-$\Sigma$-spaces. ∎

$\blacktriangleright$** Definition 3.3.8**** (CCwDs).**

A cartesian CwD (CCwD) is an SCCwD $\mathcal{C}$ that has:

• $\blacktriangleright$

A unit D-object $1\in\mathscr{D}_{\mathcal{C}}(T)$;

• $\blacktriangleright$

A $\Sigma$-space $A\{\pi_{1}\}\stackrel{{\scriptstyle\varpi_{1}}}{{\leftarrowtriangle}}\Gamma.\Sigma(A,B)\stackrel{{\scriptstyle\varpi_{2}}}{{\rightarrowtriangle}}B\{\langle\pi_{1},\varpi_{1}\rangle\}$ for any triple of $\Gamma\in\mathcal{C}$, $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ and $B\in\mathscr{D}_{\mathcal{C}}(\Gamma.A)$.

A strict CCwD is a strict SCCwD $\mathcal{C}=(\mathcal{C},T,\_.\_,\pi)$ equipped with a unit D-object $1\in\mathscr{D}_{\mathcal{C}}(T)$ and a family $\Sigma=(\Sigma(A,B))_{\Gamma\in\mathcal{C},A\in\mathscr{D}_{\mathcal{C}}(\Gamma),B\in\mathscr{D}_{\mathcal{C}}(\Gamma.A)}$ of $\Sigma$-spaces $\Sigma(A,B)\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ that is coherent in the sense that for any $\Delta,\Gamma\in\mathcal{C}$, $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$, $B\in\mathscr{D}_{\mathcal{C}}(\Gamma.A)$ and $\phi:\Delta\to\Gamma$ in $\mathcal{C}$ it satisfies

[TABLE]

where $\phi^{+}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\langle\phi\circ\pi_{1},\pi_{2}\rangle:\Delta.A\{\phi\}\to\Gamma.A$ and $\phi^{\star}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\langle\phi\circ\pi_{1},\pi_{2}\rangle:\Delta.\Sigma(A,B)\{\phi\}\to\Gamma.\Sigma(A,B)$.

$\blacktriangleright$ Example 3.3.9.

A cartesian category $\mathcal{C}$ seen as an SCCwD $\mathsf{D}(\mathcal{C})$ is a CCwD as we may define $\Sigma(A,B)\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}A\times B$, $\varpi_{1}^{\Sigma(A,B)}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\pi_{1}^{A\times B}\circ\pi_{2}^{\Gamma\times(A\times B)}$ and $\varpi_{2}^{A\times B}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\pi_{2}^{A\times B}\circ\pi_{2}^{\Gamma\times(A\times B)}$ for any $\Gamma\in\mathcal{C}$, $A\in\mathscr{D}_{\mathsf{D}(\mathcal{C})}(\Gamma)$ and $B\in\mathscr{D}_{\mathsf{D}(\mathcal{C})}(\Gamma.A)$. We call it a cartesian category seen as a CCwD.

$\blacktriangleright$** Proposition 3.3.10**** (Associativity of $\Sigma$-spaces).**

Let $\mathcal{C}$ be an SCCwD, and $\Gamma\in\mathcal{C}$, $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$, $B\in\mathscr{D}_{\mathcal{C}}(\Gamma.A)$ and $C\in\mathscr{D}_{\mathcal{C}}(\Gamma.\Sigma(A,B))$. Then, we have isomorphisms

[TABLE]

Proof.

For brevity, let us omit the subscripts and superscripts, and write $\mathit{Pair}$ and $\mathit{Triple}$ for the isomorphisms to establish. Let us define:

[TABLE]

which has $\langle\langle\pi_{1},\varpi_{1}\rangle,\varpi_{2}\rangle:\Gamma.\Sigma(A,B)\to\Gamma.A.B$ as the inverse $\mathit{Pair}^{-1}$.

Similarly, we define:

[TABLE]

which has the inverse $\mathit{Triple}^{-1}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}(\mathit{id}_{\Gamma},\Lbag\Lbag\varpi_{1},\varpi_{1}\{\langle\langle\pi_{1},\varpi_{1}\rangle,\varpi_{2}\rangle\}\Rbag,\varpi_{2}\{\langle\langle\pi_{1},\varpi_{1}\rangle,\varpi_{2}\rangle\}\Rbag)$. ∎

$\blacktriangleright$ Notation.

For strict SCCwDs, we rather write $\mathit{Pair}_{A,B}$ and $\mathit{Triple}_{A,B,C}$ for $\mathit{Pair}_{\Gamma.\Sigma(A,B)}^{\Sigma(\Gamma.A,B)}$ and $\mathit{Triple}_{\Sigma(\Sigma(A,B),C)}^{\Sigma(A,\Sigma(B,C\{\mathit{Pair}_{\Gamma.\Sigma(A,B)}^{\Sigma(\Gamma.A,B)}\}))}$, respectively. Even for non-strict SCCwDs, however, we often abuse the notation and employ $\mathit{Pair}_{A,B}$ and $\mathit{Triple}_{A,B,C}$ for brevity.

$\blacktriangleright$** Proposition 3.3.11**** (Unit law of $\Sigma$-spaces).**

Let $\mathcal{C}$ be an SCCwD, and $\Gamma\in\mathcal{C}$ and $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$. If $1\in\mathscr{D}_{\mathcal{C}}(T)$ is a unit D-object, then we have $\Sigma(1\{!_{\Gamma}\},A\{\pi_{1}\})\cong A\cong\Sigma(A,1\{!_{\Gamma}\})$.

Proof.

Immediate from Proposition 3.3.7. ∎

Thus, as promised before, we have shown that $\Sigma$-spaces have a unit D-object $1$ and satisfy associativity, generalizing the corresponding properties of binary products.

Now, let us show that coherent $\Sigma$-spaces capture strict $\mathsf{\Sigma}$-types in MLTTs:

$\blacktriangleright$** Theorem 3.3.12**** (Coherent $\Sigma$-spaces interpret $\mathsf{\Sigma}$-types).**

A strict SCCwD equipped with coherent $\Sigma$-spaces induces a CwF that supports $\mathsf{\Sigma}$-types in the strict sense.

Proof.

Let $\mathcal{C}=(\mathcal{C},T,\_.\_,\pi)$ be a strict SCCwD equipped with a coherent family of $\Sigma$-spaces $\Sigma=(\Sigma,\varpi,\Lbag,\_\Rbag)$. We equip the corresponding CwF $\mathcal{C}$ with $\Sigma$-types in the strict sense as follows:

• $\blacktriangleright$

($\Sigma$-Form) Given $\Gamma\in\mathcal{C}$, $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ and $B\in\mathscr{D}_{\mathcal{C}}(\Gamma.A)$, we have:

[TABLE]

• $\blacktriangleright$

($\Sigma$-Intro) As in the proof of Proposition 3.3.10, we define:

[TABLE]

with the inverse given by:

[TABLE]

• $\blacktriangleright$

($\Sigma$-Elim) Given $P\in\mathscr{D}_{\mathcal{C}}(\Sigma(\Gamma,\Sigma(A,B)))$ and $f\in\mathscr{D}_{\mathcal{C}}(\Sigma(\Sigma(\Gamma,A),B),P\{\mathit{Pair}_{A,B}\})$, let us define:

[TABLE]

• $\blacktriangleright$

($\Sigma$-Comp) We clearly have:

[TABLE]

• $\blacktriangleright$

($\Sigma$-Subst) By the axiom (12).

• $\blacktriangleright$

(Pair-Subst) We clearly have:

[TABLE]

as well as:

[TABLE]

where

[TABLE]

• $\blacktriangleright$

($\mathcal{R}^{\Sigma}$-Subst) We have:

[TABLE]

• $\blacktriangleright$

($\Sigma$-Uniq) Finally, given $g\in\mathscr{D}_{\mathcal{C}}(\Gamma.\Sigma(A,B),P)$ such that $g\{\mathit{Pair}_{A,B}\}=f$, we have:

[TABLE]

which completes the proof. ∎

Note that strict $\Sigma$-types in CwFs are reformulated more concisely as strict $\Sigma$-spaces in SCCwDs. In particular, we have rather induced the morphism $\mathit{Pair}_{A,B}:\Gamma.A.B\to\Gamma.\Sigma(A,B)$ from projections, which seems rather canonical, while it is taken as primitive in NMs [Awo16].

On the other hand, strict $\Sigma$-types in CwFs do not always induce $\Sigma$-spaces in the corresponding strict SCCwDs as, e.g., there are no obvious projections $\varpi_{i}$. However, we claim that strict CCwDs are a refinement of CwFs that support $1$- and $\Sigma$-types in the strict sense, rather than a restriction, as the following instances, including the term models, are formed via CCwDs:

$\blacktriangleright$ Example 3.3.13.

The SCCwD $\mathit{Sets}$ is cartesian. A unit D-object in $\mathit{Sets}$ is any singleton D-set $1=(1_{\bullet})_{\bullet\in T}$ such that $1_{\bullet}=T$. Given a set $X$ and D-sets $A$ over $X$ and $B$ over $X.A$, the $\Sigma$-space $\Sigma(A,B)$ in $\mathit{Sets}$ is the D-set $(\{(a,b)\mid a\in A_{x},b\in B_{(x,a)}\ \!\})_{x\in X}$ over $X$ equipped with the obvious projections and dependent pairings. The SCCwD $\mathit{Rel}$ is also cartesian in a similar manner.

$\blacktriangleright$ Example 3.3.14.

The SCCwD $\mathcal{GPD}$ is cartesian. A unit D-object in $\mathcal{GPD}$ is a D-groupoid $1:T\to\mathcal{GPD}$ that maps $\star\mapsto T$ and $\mathit{id}_{\star}\mapsto\mathit{id}_{T}$. Given D-groupoids $A:\Gamma\to\mathcal{GPD}$ and $B:\Gamma.A\to\mathcal{GPD}$, the $\Sigma$-space $\Sigma(A,B):\Gamma\to\mathcal{GPD}$ in $\mathcal{GPD}$ maps each object $\gamma\in\Gamma$ to the groupoid $A(\gamma).B_{\gamma}$, where the D-groupoid $B_{\gamma}:A(\gamma)\to\mathcal{GPD}$ maps each object $a\in A(\gamma)$ to the groupoid $B(\gamma,a)$ and each isomorphism $\alpha:a\stackrel{{\scriptstyle\sim}}{{\to}}a^{\prime}$ in $A(\gamma)$ to the functor $B(\mathit{id}_{\gamma},\alpha):B(\gamma,a)\to B(\gamma,a^{\prime})$, and each isomorphism $\phi:\gamma\stackrel{{\scriptstyle\sim}}{{\to}}\gamma^{\prime}$ in $\Gamma$ to the functor $A(\phi).B(\phi,A(\phi)):A(\gamma).B_{\gamma}\to A(\gamma^{\prime}).B_{\gamma^{\prime}}$ that maps each object $(a,b)\in A(\gamma).B_{\gamma}$ to the groupoid $(A(\phi)(a),B(\phi,A(\phi))(b))$ and each isomorphism $(\alpha,\beta):(a,b)\to(a^{\prime},b^{\prime})$ in $A(\gamma).B_{\gamma}$ to the functor $(A(\phi)(\alpha),B(\phi,A(\phi))(\beta)):(A(\phi)(a),B(\phi,A(\phi))(b))\to(A(\phi)(a^{\prime}),B(\phi,A(\phi))(b^{\prime}))$. The projections and dependent pairings of $\Sigma(A,B)$ are the obvious ones.

$\blacktriangleright$ Example 3.3.15.

In a similar manner, we may show that the SCCwD $\mathit{CAT}$ is also cartesian.

$\blacktriangleright$ Example 3.3.16.

The term model $\mathcal{T}(1,\Pi,\Sigma)$ is a strict CCwD. The unit D-object is $\mathsf{\diamondsuit\vdash 1\ type}$, and the $\Sigma$-space of $\mathsf{\Gamma\vdash A\ type}$ and $\mathsf{\Gamma,x:A\vdash B\ type}$ is $\mathsf{\Gamma\vdash\Sigma(A,B)\ type}$ equipped with projections

[TABLE]

and the dependent pairing of $\mathsf{\Delta\vdash g:A[\bm{\mathsf{d}}]}$ and $\mathsf{\Delta\vdash h:B[\langle\bm{\mathsf{d}},g\rangle]}$, where $\bm{\mathsf{d}}:\mathsf{\Delta}\to\mathsf{\Gamma}$, is the term

[TABLE]

3.3.2 Dependent Limits

We have seen that a unit D-object and $\Sigma$-spaces model $\mathsf{1}$- and $\mathsf{\Sigma}$-types in MLTTs. However, one may wonder if there is any systematic way to understand these constructions, which would be similar to limits that subsume finite products. This section briefly addresses this point by introducing the notion of dependent limits (D-limits), which is a natural generalization of limits. As such, the present section is a detour, and thus the reader may skip it without any problem.

$\blacktriangleright$** Definition 3.3.17**** (D-cones).**

Given an FwD $F:\mathcal{I}\to\mathcal{C}$, a dependent (D-) cone to $F$ is a triple $(\Theta,\phi,f)$ of an object $\Theta\in\mathcal{C}$, a family $\phi=(\phi_{i})_{i\in\mathcal{I}}$ of morphisms $\phi_{i}:\Theta\to F(i)$ in $\mathcal{C}$ and a family $f=(f_{i,X})_{i\in\mathcal{I},X\in\mathscr{D}_{\mathcal{I}}(i)}$ of D-morphisms $f_{i,X}:\Theta\rightarrowtriangle F(X)\{\phi_{i}\}$ such that for any morphism $\mu:i\to j$ in $\mathcal{I}$ the diagram {diagram} in $\mathcal{C}$ commutes, and for any D-morphism $x:i\rightarrowtriangle X$ in $\mathcal{I}$ the diagram {diagram} in $\mathcal{C}$ commutes.

$\blacktriangleright$** Definition 3.3.18**** (Categories of D-cones).**

Given an FwD $F:\mathcal{I}\to\mathcal{C}$, the category $\mathsf{DCones}(F)$ is defined by:

• $\blacktriangleright$

Objects are D-cones to $F$;

• $\blacktriangleright$

A morphism $(\Theta,\phi,f)\to(\Xi,\psi,g)$ is a morphism $\sigma:\Theta\to\Xi$ in $\mathcal{C}$ such that the diagrams {diagram} in $\mathcal{C}$ commute for all $i\in\mathcal{I}$ and $X\in\mathscr{D}_{\mathcal{I}}(i)$;

• $\blacktriangleright$

Composition in $\mathsf{DCones}(F)$ is the composition in $\mathcal{C}$;

• $\blacktriangleright$

Identities in $\mathsf{DCones}(F)$ are the identities in $\mathcal{C}$.

It is easy to see that $\mathsf{DCones}(F)$ is a well-defined category for any FwD $F:\mathcal{I}\to\mathcal{C}$. We are now ready to define:

$\blacktriangleright$** Definition 3.3.19**** (D-limits).**

Let $\mathcal{C}$ be a CwD and $\mathcal{I}$ a small CwD. A dependent (D-) limit of shape $\mathcal{I}$ in $\mathcal{C}$ is the terminal object in the category $\mathsf{DCones}(F)$ for any FwD $F:\mathcal{I}\to\mathcal{C}$.

Clearly, D-limits in a category $\mathcal{C}$ seen as a CwD $\mathsf{D}(\mathcal{C})$ coincide with limits in $\mathcal{C}$; in this sense, D-limits generalize limits. On the other hand, by the asymmetry of the domain and codomain of D-morphisms, what should be called dependent (D-) colimits would be more complicated than D-limits. For the lack of space, we leave the concept of D-limits as future work.

$\blacktriangleright$ Example 3.3.20.

Let $\emptyset$ denote the trivial CwD which has no objects. The D-limit of shape $\emptyset$ in a CwD $\mathcal{C}$ is just a terminal object of $\mathcal{C}$. If we focus on a terminal object of the form $T.A\in\mathcal{C}$, where $T\in\mathcal{C}$ is terminal and $A\in\mathscr{D}_{\mathcal{C}}(T)$, then such D-objects $A$ coincides with unit D-objects:

Given an object $\Gamma\in\mathcal{C}$, there is a D-morphism $\Gamma\stackrel{{\scriptstyle!_{\Gamma}}}{{\to}}T.A\stackrel{{\scriptstyle\pi_{2}}}{{\rightarrowtriangle}}A\{\pi_{1}\}\Rightarrow A\{!_{\Gamma}\}$; 2. 2.

Any D-morphism $f:\Gamma\rightarrowtriangle A\{!_{\Gamma}\}$ coincides with $\pi_{2}\{!_{\Gamma}\}$ because

[TABLE]

This pattern applies to $\Sigma$-spaces as well:

$\blacktriangleright$ Example 3.3.21.

Let $\mathcal{I}$ be an SCCwD with three objects $i,i.X,i.X.Y\in\mathcal{I}$ and two D-objects $X\in\mathscr{D}_{\mathcal{I}}(i)$ and $Y\in\mathscr{D}_{\mathcal{I}}(i.X)$. The D-limit of shape $\mathcal{I}$ in a SCCwD $\mathcal{C}$ is any diagram {diagram} in $\mathcal{C}$ such that for any diagram {diagram} in $\mathcal{C}$ there exists a unique morphism $\Upsilon(\phi,g,h):\Delta\to\Theta$ such that the diagram {diagram} commutes. Note that we have omitted semi-$\Sigma$-spaces and semi-dependent pairings in the above diagrams because they are redundant. If $\Theta$ is of the form $\Gamma.C$ for some $C\in\mathscr{D}_{\mathcal{C}}(\Gamma)$, then $\psi=\pi_{1}$, and thus the D-object $C$ coincides with the $\Sigma$-space $\Sigma(A,B)$ up to isomorphisms.

We may further study the concept of D-limits in its own right; for instance, similarly to finite limits, how can we characterize finite D-limits in terms of just a few instances of finite D-limits? Nevertheless, for the lack of space, we leave it as future work.

3.3.3 Cartesian Functors with Dependence

It is now clear what would be morphisms between CCwDs:

$\blacktriangleright$** Definition 3.3.22**** (CFwDs).**

A cartesian FwD (CFwD) is an SCFwD $F:\mathcal{C}\to\mathcal{C^{\prime}}$ between CCwDs $\mathcal{C}$ and $\mathcal{C^{\prime}}$ such that:

• $\blacktriangleright$

The D-object $F(1)\in\mathscr{D}_{\mathcal{C^{\prime}}}(F(T))$ is unit in $\mathcal{C^{\prime}}$ for each unit D-object $1\in\mathscr{D}_{\mathcal{C}}(T)$;

• $\blacktriangleright$

The diagram $F(A)\{F(\pi_{1})\}\stackrel{{\scriptstyle F(\varpi_{1})}}{{\leftarrowtriangle}}F(\Gamma.\Sigma(A,B))\stackrel{{\scriptstyle F(\varpi_{2})}}{{\rightarrowtriangle}}F(B)\{\iota^{F(\Gamma.A)}_{F(\Gamma).F(A)}\}\{\langle F(\pi_{1}),F(\varpi_{1})\rangle\}$ in $\mathcal{C^{\prime}}$ is a $\Sigma$-space of $F(A)\in\mathscr{D}_{\mathcal{C^{\prime}}}(F(\Gamma))$ and $F(B)\{\iota^{F(\Gamma.A)}_{F(\Gamma).F(A)}\}\in\mathscr{D}_{\mathcal{C^{\prime}}}(F(\Gamma).F(A))$ in $\mathcal{C^{\prime}}$ for a $\Sigma$-space $A\{\pi_{1}\}\stackrel{{\scriptstyle\varpi_{1}}}{{\leftarrowtriangle}}\Gamma.\Sigma(A,B)\stackrel{{\scriptstyle\varpi_{2}}}{{\rightarrowtriangle}}B\{\langle\pi_{1},\varpi_{1}\rangle\}$ of any $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ and $B\in\mathscr{D}_{\mathcal{C}}(\Gamma.A)$ in $\mathcal{C}$.

Moreover, given that $\mathcal{C}$ and $\mathcal{C^{\prime}}$ are both strict, written $\mathcal{C}=(\mathcal{C},T,\_.\_,\pi,1,\Sigma,\varpi)$ and $\mathcal{C^{\prime}}=(\mathcal{C^{\prime}},T^{\prime},\_.^{\prime}\_,\pi^{\prime},1^{\prime},\Sigma^{\prime},\varpi^{\prime})$, $F$ is strict iff it is a strict SCFwD, $F(1)=1^{\prime}$, and the diagram

[TABLE]

in $\mathcal{C^{\prime}}$ coincides with the $\Sigma$-space

[TABLE]

in $\mathcal{C^{\prime}}$ for any $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ and $B\in\mathscr{D}_{\mathcal{C}}(\Gamma.A)$ in $\mathcal{C}$.

Given a CFwD $F:\mathcal{C}\to\mathcal{D}$, there is an isomorphism

[TABLE]

between D-objects in $\mathcal{D}$ for any $\Sigma$-space $\Sigma(A,B)\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ in $\mathcal{C}$. It is easy to see that $F$ is strict iff $(\mathit{id}_{F(\Gamma)},\iota^{F}_{A,B})$ is the identity for any $\Sigma$-space $\Sigma(A,B)\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ in $\mathcal{C}$.

$\blacktriangleright$ Example 3.3.23.

A cartesian functor $F:\mathcal{C}\to\mathcal{D}$ seen as an SCFwD $\mathsf{D}(F):\mathsf{D}(\mathcal{C})\to\mathsf{D}(\mathcal{D})$ is a CFwD because unit D-objects and $\Sigma$-spaces are just finite products. Let us call this kind of CFwDs cartesian functors seen as CFwDs. Thus, CFwDs are generalized cartesian functors.

$\blacktriangleright$ Example 3.3.24.

Given a locally small CCwD $\mathcal{C}$ and an object $\Delta\in\mathcal{C}$, the SCFwD $\mathcal{C}(\Delta,\_):\mathcal{C}\to\mathit{Sets}$ is cartesian. Given a unit D-object $1\in\mathscr{D}_{\mathcal{C}}(T)$, the D-set $\mathcal{C}(\Delta,1)$ is unit in $\mathit{Sets}$ because it is a singleton D-set $\mathcal{C}(\Delta,1)=(\mathcal{C}(\Delta,1\{!_{\Delta}\}))_{!_{\Delta}\in\mathcal{C}(\Delta,T)}$, and the set $\mathcal{C}(\Delta,1\{!_{\Delta}\})$ is a singleton set. Moreover, given a $\Sigma$-space $A\{\pi_{1}\}\stackrel{{\scriptstyle\varpi_{1}}}{{\leftarrowtriangle}}\Gamma.\Sigma(A,B)\stackrel{{\scriptstyle\varpi_{2}}}{{\rightarrowtriangle}}B\{\langle\pi_{1},\varpi_{1}\rangle\}$ of any D-objects $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ and $B\in\mathscr{D}_{\mathcal{C}}(\Gamma.A)$ in $\mathcal{C}$, it is not hard to see that the diagram

[TABLE]

is a $\Sigma$-space of D-sets $\mathcal{C}(\Delta,A)\in\mathscr{D}_{\mathit{Sets}}(\mathcal{C}(\Delta,\Gamma))$ and $\mathcal{C}(\Delta,B)\in\mathscr{D}_{\mathit{Sets}}(\mathcal{C}(\Delta,\Gamma.A))$ in $\mathit{Sets}$.

3.3.4 The 2-Category of Cartesian Categories with Dependence

It is now clear there is the following 2-category:

$\blacktriangleright$** Definition 3.3.25**** (The 2-category $\mathbb{CC_{D}}$).**

The 2-category $\mathbb{CC_{D}}$ is a sub-2-category of $\mathbb{SCC_{D}}$ whose 0-cells are small CCwDs and 1-cells are CFwDs.

$\blacktriangleright$** Theorem 3.3.26**** (Well-defined $\mathbb{CC_{D}}$).**

The structure $\mathbb{CC_{D}}$ is a well-defined sub-2-category of $\mathbb{SCC_{D}}$.

3.4 Cartesian Closed Categories and Functors with Dependence

This is the last section on the basic theory of CwDs, in which we introduce a closed structure on SCCwDs. On the one hand it gives a categorical semantics of strict $\mathsf{\Pi}$-types in MLTTs, and on the other hand it provides a categorical generalization of the 2-category $\mathbb{CCC}$ of small CCCs.

3.4.1 Cartesian Closed Categories with Dependence

We would like to equip CCwDs with a closed structure to form a generalization of CCCs. Then, as a generalization of exponentials, the following construction seems appropriate:

$\blacktriangleright$** Definition 3.4.1**** (Pseudo-$\Pi$-spaces).**

Let $\mathcal{C}$ be an SCCwD, $\Gamma\in\mathcal{C}$, $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ and $B\in\mathscr{D}_{\mathcal{C}}(\Gamma.A)$. A pseudo-dependent map (pseudo-$\Pi$-) space from $A$ to $B$ in $\mathcal{C}$ is a D-object

[TABLE]

equipped with a D-morphism

[TABLE]

in $\mathcal{C}$, called the dependent (D-) evaluation of $\Pi(A,B)$, where

[TABLE]

such that for any D-morphism in $\mathcal{C}$ of the form $f:\Gamma.A\rightarrowtriangle B$ there exists a unique D-morphism

[TABLE]

in $\mathcal{C}$, called the dependent (D-) currying of $f$, that satisfies the equation

[TABLE]

where

[TABLE]

Pseudo-$\Pi$-spaces, D-evaluations and D-currying are, as their names suggest, intended to be generalizations of exponentials, evaluations and currying, respectively. To make this point explicit, let us draw the following commutative diagram that depicts the universal property of a pseudo-$\Pi$-space $\Pi(A,B)\in\mathscr{D}_{\mathcal{C}}(\Gamma)$: {diagram} which can be given in a CCC $\mathcal{C}=(\mathcal{C},T,\times,p,\Rightarrow,\mathit{ev})$ by: {diagram}

Unfortunately, however, pseudo-$\Pi$-spaces are not unique up to isomorphisms because the canonical morphisms between pseudo-$\Pi$-spaces from the same D-object $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ to the same D-object $B\in\mathscr{D}_{\mathcal{C}}(\Gamma.A)$ (specifically, they are $\imath_{A,B}$ and $\jmath_{A,B}$ in the proof of Proposition 3.4.8 below) are not inverses to each other. By a similar mechanism, they do not give rise to functors. In other words, pseudo-$\Pi$-spaces are a categorically incomplete structure.

To overcome this point, let us define:

$\blacktriangleright$** Definition 3.4.2**** ($\Pi$-spaces).**

A pseudo-$\Pi$-space $\Pi(A,B)$ from $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ to $B\in\mathscr{D}_{\mathcal{C}}(\Gamma.A)$ in an SCCwD $\mathcal{C}$ is a dependent map ($\Pi$-) space from $A$ to $B$ in $\mathcal{C}$ iff for any D-object $C\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ the pair $\Pi(A,B)\{\pi_{1}\}=(\Pi(A,B)\{\pi_{1}\},\mathit{dev}_{\Pi(A,B)\{\pi_{1}\}})$ such that

[TABLE]

is a pseudo-$\Pi$-space from $A\{\pi_{1}\}\in\mathscr{D}_{\mathcal{C}}(\Gamma.C)$ to $B\{\pi_{1}^{\star A}\}\in\mathscr{D}_{\mathcal{C}}(\Gamma.C.A\{\pi_{1}\})$ in $\mathcal{C}$ that satisfies

[TABLE]

for any $D\in\mathscr{D}_{\mathcal{C}}(\Gamma)$, $h:\Gamma.C.A\{\pi_{1}\}\rightarrowtriangle B\{\pi_{1}^{\star A}\}$ and $g:\Gamma.D\rightarrowtriangle C\{\pi_{1}\}$ in $\mathcal{C}$, where

[TABLE]

The additional universal properties (15) and (16) of a $\Pi$-space $\Pi(A,B)\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ may be depicted as the following commutative diagrams: {diagram} where $\Lambda(h\{\langle\pi_{1},g\rangle^{+}\})\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\Lambda_{\Pi(A,B)\{\pi\}}(h\{\langle\pi_{1},g\rangle^{+A\{\pi_{1}\}}\})$.

Proposition 3.4.8 below verifies the uniqueness of $\Pi$-spaces up to isomorphisms, where the additional axioms (15) and (16) play essential roles. Also, it is straightforward to see that $\Pi$-spaces (and pseudo-$\Pi$-spaces) in a cartesian category seen as a CCwD coincide with exponentials, where note that D-evaluations do not depend on objects, and thus they are essentially the same as evaluations.

We then define the promised generalization of CCCs as follows:

$\blacktriangleright$** Definition 3.4.3**** (SCCCwDs).**

A semi-cartesian closed CwD (SCCCwD) is an SCCwD $\mathcal{C}$ that has for any triple of $\Gamma\in\mathcal{C}$, $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ and $B\in\mathscr{D}_{\mathcal{C}}(\Gamma.A)$ a $\Pi$-space from $A$ to $B$ in $\mathcal{C}$. A strict SCCCwD is a strict SCCwD $\mathcal{C}$ equipped with a family $\Pi=(\Pi(A,B))_{\Gamma\in\mathcal{C},A\in\mathscr{D}_{\mathcal{C}}(\Gamma),B\in\mathscr{D}_{\mathcal{C}}(\Gamma.A)}$ of $\Pi$-spaces $\Pi(A,B)\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ in $\mathcal{C}$ that is coherent in the sense that it satisfies the equations

[TABLE]

for any $\Delta,\Gamma\in\mathcal{C}$, $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$, $B\in\mathscr{D}_{\mathcal{C}}(\Gamma.A)$ and $\phi:\Delta\to\Gamma$ in $\mathcal{C}$, where

[TABLE]

$\blacktriangleright$** Definition 3.4.4**** (CCCwDs).**

A cartesian closed CwD (CCCwD) is a CCwD that is semi-cartesian closed. A strict CCCwD is a strict CCwD that is strictly semi-cartesian closed.

Note that the coherence axioms (17) and (18) on strict SCCCwDs are necessary to interpret strict $\mathsf{\Pi}$-types in MLTTs; see the proof of Theorem 3.4.15 below.

Now, let us prove some of the expected properties of $\Pi$-spaces, including their uniqueness up to isomorphisms (Proposition 3.4.8), as a generalization of exponentials.

$\blacktriangleright$** Lemma 3.4.5**** (Transpositions in pseudo-$\Pi$-spaces).**

Let $\mathcal{C}$ be an SCCwD, $\Gamma\in\mathcal{C}$, $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ and $B\in\mathscr{D}_{\mathcal{C}}(\Gamma.A)$. If $\Pi(A,B)\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ is a pseudo-$\Pi$-space from $A$ to $B$ in $\mathcal{C}$, then there is a bijection

[TABLE]

Proof.

There is the function $\mathscr{D}_{\mathcal{C}}(\Gamma.A,B)\to\mathscr{D}_{\mathcal{C}}(\Gamma,\Pi(A,B))$ that maps $f\mapsto\Lambda_{\Pi(A,B)}(f)$, and also there is the inverse $\mathscr{D}_{\mathcal{C}}(\Gamma,\Pi(A,B))\to\mathscr{D}_{\mathcal{C}}(\Gamma.A,B)$ that maps $g\mapsto\mathit{dev}_{\Pi(A,B)}\{(\overline{g})^{+A\{\pi_{1}\}}\}$, where it is easy to verify that these maps are inverses to each other and thus left to the reader. ∎

$\blacktriangleright$ Notation.

By Lemma 3.4.5, it is legitimate to write $\Lambda_{\Pi(A,B)}^{-1}:\mathscr{D}_{\mathcal{C}}(\Gamma,\Pi(A,B))\to\mathscr{D}_{\mathcal{C}}(\Gamma.A,B)$ for the map

[TABLE]

$\blacktriangleright$** Lemma 3.4.6**** (First $\Pi$-lemma).**

Let $\mathcal{C}$ be an SCCwD, $\Gamma\in\mathcal{C}$, $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ and $B\in\mathscr{D}_{\mathcal{C}}(\Gamma.A)$. If $\Pi(A,B)\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ is a $\Pi$-space from $A$ to $B$ in $\mathcal{C}$, then we have:

[TABLE]

Proof.

By the universal property of the pseudo-$\Pi$-space $\Pi(A,B)\{\pi_{1}\}\in\mathscr{D}_{\mathcal{C}}(\Gamma.\Pi(A,B))$ in $\mathcal{C}$, it suffices to establish the equation

[TABLE]

Then, observe that:

[TABLE]

which completes the proof. ∎

$\blacktriangleright$** Lemma 3.4.7**** (Second $\Pi$-lemma).**

Let $\mathcal{C}=(\mathcal{C},T,\_.\_,\pi,\Pi,\mathit{dev})$ be a strict SCCCwD. Given $\Delta,\Gamma\in\mathcal{C}$, $\phi:\Delta\to\Gamma$, $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$, $B\in\mathscr{D}_{\mathcal{C}}(\Gamma.A)$ and $f:\Gamma.A\rightarrowtriangle B$ in $\mathcal{C}$, we have:

[TABLE]

Proof.

By the universal property of the coherent family $\Pi$ of the $\Pi$-spaces in $\mathcal{C}$, it suffices to show the equation

[TABLE]

Then, we have:

[TABLE]

which completes the proof. ∎

$\blacktriangleright$** Proposition 3.4.8**** (Uniqueness of $\Pi$-spaces).**

In any SCCwD $\mathcal{C}$, every $\Pi$-space in $\mathcal{C}$ is unique up to isomorphisms. More precisely, if $\Gamma\in\mathcal{C}$, $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ and $B\in\mathscr{D}_{\mathcal{C}}(\Gamma.A)$, and $\Pi(A,B),\Pi^{\prime}(A,B)\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ are both $\Pi$-spaces from $A$ to $B$ in $\mathcal{C}$, then $\Pi(A,B)\cong\Pi^{\prime}(A,B)$.

Proof.

First, we have the following two D-morphisms in $\mathcal{C}$:

[TABLE]

It suffices to show that these D-morphisms are inverses to each other.

Then, observe that:

[TABLE]

By symmetry, we also have $\jmath_{A,B}\{\langle\pi_{1},\imath_{A,B}\rangle\}=\pi_{2}$.

Moreover, the D-morphism

[TABLE]

where

[TABLE]

satisfies

[TABLE]

And again by symmetry, $\mathit{dev}_{\Pi^{\prime}(A,B)}\{\langle\pi_{1},\imath_{A,B}\rangle^{+A\{\pi_{1}\}}\}=\mathit{dev}_{\Pi(A,B)}$, completing the proof. ∎

At this point, we hope that the reader has been convinced that $\Pi$-spaces are a reasonable generalization of exponentials. Then, let us define a generalization of CCCs:

$\blacktriangleright$** Definition 3.4.9**** (SCCCwDs).**

A semi-cartesian closed CwD (SCCCwD) is an SCCwD $\mathcal{C}$ that has $\Pi$-spaces, i.e., a $\Pi$-space $\Pi(A,B)\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ for any $\Gamma\in\mathcal{C}$, $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ and $B\in\mathscr{D}_{\mathcal{C}}(\Gamma.A)$. An SCCCwD is strict if it is a strict SCCwD equipped with specified $\Pi$-spaces.

$\blacktriangleright$** Definition 3.4.10**** (CCCwDs).**

A cartesian closed CwD (CCCwD) is a CCwD that is semi-cartesian closed. A CCCwD is strict if it is a strict CCwD equipped with specified $\Pi$-spaces.

$\blacktriangleright$ Example 3.4.11.

As observed above, a (resp. strict) cartesian category $\mathcal{C}$ seen as a (resp. strict) CCwD $\mathsf{D}(\mathcal{C})$ is closed iff so is $\mathcal{C}$. Hence, (resp. strict) CCCwDs are a generalization of (resp. strict) CCCs. Let us call this kind of CCCwDs CCCs seen as CCCwDs.

$\blacktriangleright$ Example 3.4.12.

The CCwD $\mathit{Sets}$ is cartesian closed. Given $X\in\mathit{Sets}$, $A\in\mathscr{D}_{\mathit{Sets}}(X)$ and $B\in\mathscr{D}_{\mathit{Sets}}(X.A)$, we define $\Pi(A,B)$ to be the D-set

[TABLE]

Given a D-function $f:X.A\rightarrowtriangle B$, its D-currying $\Lambda_{A,B}(f):X\to\Pi(A,B)$ maps

[TABLE]

and the D-evaluation $\mathit{dev}_{A,B}:X.\Pi(A,B).A\{\pi_{1}\}\rightarrowtriangle B\{\pi_{1}^{+A}\}$ maps

[TABLE]

It is easy to see that these $\Pi$-spaces in $\mathit{Sets}$ satisfy the required axioms.

$\blacktriangleright$ Example 3.4.13.

The CCwD $\mathcal{GPD}$ is cartesian closed. Given a groupoid $\Gamma$, and D-groupoids $A:\Gamma\to\mathcal{GPD}$ and $B:\Gamma.A\to\mathcal{GPD}$, there is the D-groupoid $\Pi(A,B):\Gamma\to\mathcal{GPD}$ defined by:

• $\blacktriangleright$

First, as shown in [HS98], the set $\mathscr{D}_{\mathcal{GPD}}(\Gamma,A)$ may be seen as the groupoid whose objects are D-groupoid morphisms $f:\Gamma\rightarrowtriangle A$, where note that $\overline{f}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\langle\mathit{id}_{\Gamma},f\rangle:\Gamma\to\Gamma.A$ is a functor, and isomorphisms $f\to g$ are families $\eta=(\eta_{\gamma})_{\gamma\in\Gamma}$ of isomorphisms $\eta_{\gamma}:f(\gamma)\to g(\gamma)$ in $A(\gamma)$ such that $\overline{\eta}=(\overline{\eta}_{\gamma})_{\gamma\in\Gamma}$, where $\overline{\eta}_{\gamma}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}(\mathit{id}_{\gamma},\eta_{\gamma}):\overline{f}(\gamma)\to\overline{g}(\gamma)$, forms an NT $\overline{f}\to\overline{g}$.

• $\blacktriangleright$

Then, again as shown in [HS98], the D-groupoid $\Pi(A,B):\Gamma\to\mathcal{GPD}$ maps each object $\gamma\in\Gamma$ to the groupoid

[TABLE]

and each isomorphism $\phi:\gamma\stackrel{{\scriptstyle\sim}}{{\to}}\gamma^{\prime}$ in $\Gamma$ to the functor

[TABLE]

that maps each D-groupoid homomorphism $f\in\mathscr{D}_{\mathcal{GPD}}(A(\gamma),B_{\gamma})$ to another

[TABLE]

and each isomorphism $\eta:f\stackrel{{\scriptstyle\sim}}{{\to}}g$ in $\mathscr{D}_{\mathcal{GPD}}(A(\gamma),B_{\gamma})$ to the natural isomorphism

[TABLE]

whose component on each $a^{\prime}\in A(\gamma^{\prime})$ is given by:

[TABLE]

The D-evaluation $\mathit{dev}_{A,B}:\Gamma.\Pi(A,B).A\{\pi_{1}\}\rightarrowtriangle B\{\pi_{1}^{+A}\}$ in $\mathcal{GPD}$ is the D-groupoid homomorphism that maps

[TABLE]

and the D-currying $\Lambda(h):\Gamma\rightarrowtriangle\Pi(A,B)$ of a D-groupoid homomorphism $h:\Gamma.A\rightarrowtriangle B$ maps

[TABLE]

It is not hard to see that these $\Pi$-spaces in $\mathcal{GPD}$ satisfy the required axioms.

$\blacktriangleright$ Example 3.4.14.

The term model $\mathcal{T}(1,\Pi,\Sigma)$ is a CCCwD. $\Pi$-spaces are given by $\Pi$-Form, $\mathit{dev}_{A,B}$ by $\Pi$-Elim for terms $\mathsf{\Gamma,f:\Pi(A,B),x:A\vdash f(x):B[f(x)]}$ and D-currying by $\Pi$-Intro.

Now, let us prove that a coherent family of $\Pi$-spaces interprets strict $\mathsf{\Pi}$-types in MLTTs:

$\blacktriangleright$** Theorem 3.4.15**** (Coherent $\Pi$-spaces interpret $\mathsf{\Pi}$-types).**

A strict SCCCwD induces a CwF that supports $\Pi$-types in the strict sense.

Proof.

Let $\mathcal{C}=(\mathcal{C},T,\_.\_,\pi,\Pi,\mathit{dev})$ be a strict SCCCwD. We equip the corresponding CwF $\mathcal{C}$ with $\Pi$-types in the strict sense as follows:

• $\blacktriangleright$

($\Pi$-Form) Given $\Gamma\in\mathcal{C}$, $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ and $B\in\mathscr{D}_{\mathcal{C}}(\Sigma(\Gamma,A))$, we have:

[TABLE]

• $\blacktriangleright$

($\Pi$-Intro) Given $f\in\mathscr{D}_{\mathcal{C}}(\Gamma.A,B)$, we define:

[TABLE]

• $\blacktriangleright$

($\Pi$-Elim) Recall that there is the inverse $\Lambda_{\Pi(A,B)}^{-1}$ of the D-currying map $\Lambda_{\Pi(A,B)}$ as shown in the proof of Lemma 3.4.5. Given $g\in\mathscr{D}_{\mathcal{C}}(\Gamma,\Pi(A,B))$ and $a\in\mathscr{D}_{\mathcal{C}}(\Gamma,A)$, we define:

[TABLE]

where $\overline{a}=\langle\mathit{id}_{\Gamma},a\rangle:\Gamma\to\Sigma(\Gamma,A)$.

• $\blacktriangleright$

($\Pi$-Comp) It is easy to see that:

[TABLE]

• $\blacktriangleright$

($\Pi$-Subst) By the axiom (17).

• $\blacktriangleright$

($\lambda$-Subst) By Lemma 3.4.7.

• $\blacktriangleright$

(App-Subst) It is easy to see that:

[TABLE]

where $\overline{a\{\phi\}}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\langle\mathit{id}_{\Delta},a\{\phi\}\rangle:\Delta\to\Sigma(\Delta,A\{\phi\})$.

• $\blacktriangleright$

($\Pi$-Uniq) Given $k\in\mathit{Tm}(\Gamma.A,\Pi(A,B)\{\pi_{1}\})$, observe that:

[TABLE]

which completes the proof. ∎

Hence, Theorems 2.2.8, 3.3.5, 3.3.12 and 3.4.15 implies:

$\blacktriangleright$** Corollary 3.4.16**** (CCCwDs and CwFs).**

A strict CCCwD induces a CwF that supports $1$-, $\Sigma$- and $\Pi$-types in the strict sense, and thus it gives a sound interpretation of $\mathsf{MLTT(1,\Pi,\Sigma)}$.

Also, since the term model $\mathcal{T}(1,\Pi,\Sigma)$ forms a strict CCCwD, we have:

$\blacktriangleright$** Theorem 3.4.17**** (Completeness theorem).**

The interpretation of $\mathsf{MLTT(1,\Pi,\Sigma)}$ in CCCwDs is complete in the sense of Theorem 2.2.9.

Since $\Sigma$- and $\Pi$-spaces in CCCwDs are respectively generalizations of binary products and of exponentials in CCCs, respectively, it is expected that the former is left adjoint to the latter. Let us see that it is in fact the case (up to the first projections) as follows.

First, let us consider $\Sigma$-spaces. Clearly, we have the correspondence {diagram} where $\Gamma\in\mathcal{C}$, $B,D\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ and $C\in\mathscr{D}_{\mathcal{C}}(\Gamma.B)$, which induces an adjunction {diagram} where the functor $\_\{\pi_{1}^{\Gamma.B}\}:\mathcal{C}_{\Gamma}\to\mathcal{C}_{\Gamma.B}$ maps

[TABLE]

and the functor $\Sigma(B,\_):\mathcal{C}_{\Gamma.B}\to\mathcal{C}_{\Gamma}$ maps

[TABLE]

whose functorialities are both easy to verify.

Next, let us think of $\Pi$-spaces. Note that Lemma 3.4.5 gives the bijective correspondence {diagram} for any $\Gamma\in\mathcal{C}$, $B\in\mathcal{C}_{\Gamma}$ and $C\in\mathcal{C}_{\Gamma.B}$, but it is not an adjunction. Then, following the term model construction of DTTs in [Jac99], we slightly modify this correspondence into {diagram} for each $A\in\mathcal{C}_{\Gamma}$, which gives an adjunction {diagram} where $\Pi(B,\_):\mathcal{C}_{\Gamma.B}\to\mathcal{C}_{\Gamma}$ maps

[TABLE]

whose functoriality (specifically the preservation of composition) is by the axioms (15) and (16).

Therefore, we may compose the two adjunctions to obtain the adjunction: {diagram} which particularly implies the correspondence {diagram} between $\Sigma$ and $\Pi$ up to the first projections.

3.4.2 Cartesian Closed Functors with Dependence

Again, following the general recipe that morphisms are structure-preserving, let us define:

$\blacktriangleright$** Definition 3.4.18**** (CCFwDs).**

A cartesian closed FwD (CCFwD) is a CFwD $F:\mathcal{C}\to\mathcal{D}$ between CCCwDs $\mathcal{C}$ and $\mathcal{D}$ such that the diagram

[TABLE]

forms a $\Pi$-space from $F(A)\in\mathscr{D}_{\mathcal{D}}(F(\Gamma))$ to $F(B)\{\iota^{F(\Gamma.A)}_{F(\Gamma).F(A)}\}\in\mathscr{D}_{\mathcal{D}}(F(\Gamma).F(A))$ in $\mathcal{D}$ for any $\Gamma\in\mathcal{C}$, $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ and $B\in\mathscr{D}_{\mathcal{C}}(\Gamma.A)$ in $\mathcal{C}$. If $\mathcal{C}$ and $\mathcal{D}$ are both strict, $F$ is strict iff it is a strict CFwD, and the diagram

[TABLE]

coincides with the $\Pi$-space

[TABLE]

for any $\Gamma\in\mathcal{C}$, $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ and $B\in\mathscr{D}_{\mathcal{C}}(\Gamma.A)$ in $\mathcal{C}$.

$\blacktriangleright$ Example 3.4.19.

A (resp. strict) cartesian closed functor $F:\mathcal{C}\to\mathcal{D}$ seen as a CFwD $\mathsf{D}(F):\mathsf{D}(\mathcal{C})\to\mathsf{D}(\mathcal{D})$ is clearly (resp. strictly) closed.

$\blacktriangleright$ Example 3.4.20.

Given a locally small CCCwD $\mathcal{C}$ and an object $\Delta\in\mathcal{C}$, the CFwD $\mathcal{C}(\Delta,\_):\mathcal{C}\to\mathit{Sets}$ is closed. In fact, given a $\Pi$-space $\Gamma.\Pi(A,B).A\{\pi_{1}\}\stackrel{{\scriptstyle\mathit{dev}_{\Pi(A,B)}}}{{\rightarrowtriangle}}B\{\pi_{1}^{+A}\}$ in $\mathcal{C}$, the diagram

[TABLE]

in $\mathit{Sets}$ forms a $\Pi$-space from the D-set $\mathcal{C}(\Delta,A)\in\mathscr{D}_{\mathit{Sets}}(\mathcal{C}(\Delta,\Gamma))$ to another $\mathcal{C}(\Delta,B)\in\mathscr{D}_{\mathit{Sets}}(\mathcal{C}(\Delta,\Gamma.A))$.

3.4.3 The 2-Category of Cartesian Closed Categories with Dependence

Finally, let us summarize what we have established in this section as the following 2-category:

$\blacktriangleright$** Definition 3.4.21**** (The 2-category $\mathbb{CCC_{D}}$).**

The 2-category $\mathbb{CCC_{D}}$ is the sub-2-category of $\mathbb{CC_{D}}$ whose 0-cells are small CCCwDs and 1-cells are CCFwDs.

$\blacktriangleright$** Theorem 3.4.22**** (Well-defined $\mathbb{CCC_{D}}$).**

$\mathbb{CCC_{D}}$* is a well-defined sub-2-category of $\mathbb{CC_{D}}$.*

Proof.

It suffices to show that the composition $G\circ F:\mathcal{C}\to\mathcal{E}$ of any CCFwDs $F:\mathcal{C}\to\mathcal{D}$ and $G:\mathcal{D}\to\mathcal{E}$ is again a CCFwD. But then, it is immediate because the equation

[TABLE]

holds for any $\Gamma\in\mathcal{C}$ and $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ in $\mathcal{C}$ by the universal property of semi-$\Sigma$-spaces. ∎

We have established a generalization of CCCs, whose strict version gives a categorical yet direct semantics of MLTTs. In the rest of the paper, we shall make these relations with CCCs and with MLTTs more precise by establishing certain 2-equivalences.

4 Equivalence between CtxCCCs and ConCtxCCCwDs

This section is devoted to establish a 2-equivalence between the 2-category of contextual CCCs and the 2-category of constant contextual CCCwDs, where contextuality refers to strictness plus reachability [Pit01] of any object from a terminal object via binary products or semi-$\Sigma$-spaces.

The rest of the section proceeds roughly as follows. We first define contextual CCCs and contextual CCCwDs in Section 4.1 and Section 4.2, respectively. And then, we establish the promised 2-equivalence (Theorem 4.3.7) in Section 4.3.

4.1 Contextual Cartesian Closed Categories

Let us begin with introducing contextual CCCs, which are similar to contextual categories given by Cartmell [Car86]:

$\blacktriangleright$** Definition 4.1.1**** (CtxCCCs).**

A contextual CCC (CtxCCC) is a strict CCC, i.e., a CCC $\mathcal{C}$ equipped with specified finite products $(T,\times,p)$ and exponentials $(\Rightarrow,\mathit{ev})$, together with a class $\mathscr{A}_{\mathcal{C}}\subseteq\mathsf{ob}(\mathcal{C})$ of objects in $\mathcal{C}$, whose elements are called atomic objects in $\mathcal{C}$, such that $T\in\mathscr{A}_{\mathcal{C}}$, and each object $\Delta\in\mathcal{C}$ has a unique finite sequence $\Delta_{1},\Delta_{2},\dots,\Delta_{\#(\Delta)}\in\mathscr{A}_{\mathcal{C}}^{\ast}$ of atomic objects in $\mathcal{C}$ that satisfies

[TABLE]

where $\times$ is left associative. We call the natural number $\#(\Delta)$ the length of $\Delta$.

Note that in STTs each context is of the form $\mathsf{\diamondsuit,x_{1}:A_{1},x_{2}:A_{2},\dots,x_{k}:A_{k}}$. Atomic objects in contextual CCCs are a categorical abstraction of such atomic constituents $\mathsf{x_{i}:A_{i}}$ of contexts.

$\blacktriangleright$** Definition 4.1.2**** (CtxCCFs).**

A contextual cartesian closed functor (CtxCCF) is a strict cartesian closed functor $F:\mathcal{C}\to\mathcal{D}$ between CtxCCCs $\mathcal{C}$ and $\mathcal{D}$ that preserves atomic objects, i.e.,

[TABLE]

$\blacktriangleright$** Definition 4.1.3**** (The 2-category $\mathsf{Ctx}\mathbb{CCC}$).**

The 2-category $\mathsf{Ctx}\mathbb{CCC}$ is the sub-2-category of the 2-category $\mathbb{CCC}$ of small CCCs whose 0-cells are small CtxCCCs, 1-cells are CtxCCFs, and 2-cells are NTs.

Clearly, $\mathsf{Ctx}\mathbb{CCC}$ is a well-defined 2-category.

4.2 Contextual Cartesian Closed Categories with Dependence

Next, let us define the contextual analogue of SCCwDs:

$\blacktriangleright$** Definition 4.2.1**** (CtxSCCwDs).**

A contextual SCCwD (CtxSCCwD) is a strict SCCwD $\mathcal{C}=(\mathcal{C},T,\_.\_,\pi)$ such that:

• $\blacktriangleright$

Each constant D-object $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$ satisfies

[TABLE]

for a unique D-object $\underline{A}\in\mathscr{D}_{\mathcal{C}}(T)$, called the core of $A$; and

• $\blacktriangleright$

Each object $\Delta\in\mathcal{C}$ has a unique finite sequence $D_{1}\in\mathscr{D}_{\mathcal{C}}(T),D_{2}\in\mathscr{D}_{\mathcal{C}}(T.D_{1}),\dots,D_{\sharp(\Delta)}\in\mathscr{D}_{\mathcal{C}}(T.D_{1}.D_{2}\dots D_{\sharp(\Delta)-1})$ of D-objects that satisfies

[TABLE]

where we call the natural number $\#(\Delta)$ the length of $\Delta$.

$\blacktriangleright$** Lemma 4.2.2**** (CtxSCCwD-lemma).**

Let $F:\mathcal{C}\to\mathcal{C^{\prime}}$ be a strict SCFwD between CtxSCCwDs $\mathcal{C}$ and $\mathcal{C^{\prime}}$. Then, we have:

$A\{\phi\}=\underline{A}\{!_{\Delta}\}$; 2. 2.

$F(!_{\Gamma})=\ !_{F(\Gamma)}$; and 3. 3.

$F(\underline{A})=\underline{F(A)}$**

for any objects $\Delta,\Gamma\in\mathcal{C}$, morphism $\phi:\Delta\to\Gamma$ in $\mathcal{C}$ and constant D-object $A\in\mathscr{D}_{\mathcal{C}}(\Gamma)$.

Proof.

The first and the second equations are immediate, and the third equation follows from the second. ∎

$\blacktriangleright$** Definition 4.2.3**** (CtxCCCwDs).**

A contextual CCCwD (CtxCCCwD) is a strict CCCwD such that the underlying strict SCCwD is contextual.

$\blacktriangleright$** Definition 4.2.4**** (The 2-category $\mathsf{Ctx}\mathbb{CCC_{D}}$).**

The 2-category $\mathsf{Ctx}\mathbb{CCC_{D}}$ is the sub-2-category of $\mathbb{CCC_{D}}$ whose 0-cells are small CtxCCCwDs, 1-cells are strict CCFwDs, and 2-cells are NTwDs.

$\blacktriangleright$** Definition 4.2.5**** (The 2-category $\mathsf{ConCtx}\mathbb{CCC_{D}}$).**

The 2-category $\mathsf{ConCtx}\mathbb{CCC_{D}}$ is the full sub-2-category of $\mathsf{Ctx}\mathbb{CCC_{D}}$ whose 0-cells are all constant.

4.3 Equivalence between CtxCCCs and ConCtxCCCwDs

Finally, we define 2-functors $\mathsf{D}:\mathsf{Ctx}\mathbb{CCC}\rightleftarrows\mathsf{ConCtx}\mathbb{CCC_{D}}:\mathsf{S}$, and show that they constitute a 2-equivalence between the 2-categories.

Let us begin with defining the functor $\mathsf{D}:\mathsf{Ctx}\mathbb{CCC}\to\mathsf{ConCtx}\mathbb{CCC_{D}}$, which just summarizes the operation $\mathsf{D}$ described so far:

$\blacktriangleright$** Definition 4.3.1**** (The 2-functor $\mathsf{D}$).**

The 2-functor $\mathsf{D}:\mathsf{Ctx}\mathbb{CCC}\to\mathsf{ConCtx}\mathbb{CCC_{D}}$ maps:

• $\blacktriangleright$

Each CtxCCC $\mathcal{C}=(\mathcal{C},\mathscr{A}_{\mathcal{C}},T,\times,p,\Rightarrow,\mathit{ev})$ to the constant CtxCCCwD $\mathsf{D}(\mathcal{C})$ such that:

[TABLE]

for all $\Delta,\Gamma\in\mathsf{D}(\mathcal{C})$, $\Theta\in\mathscr{D}_{\mathsf{D}(\mathcal{C})}(\Gamma)$, $\Xi\in\mathscr{D}_{\mathsf{D}(\mathcal{C})}(\Gamma.\Theta)$, $\psi\in\mathscr{D}_{\mathsf{D}(\mathcal{C})}(\Gamma,\Theta)$ and $\phi:\Delta\to\Gamma$ in $\mathsf{D}(\mathcal{C})$;

• $\blacktriangleright$

Each CtxCCF $F:\mathcal{C}\to\mathcal{D}$ to the strict CCFwD $\mathsf{D}(F):\mathsf{D}(\mathcal{C})\to\mathsf{D}(\mathcal{D})$ given by:

[TABLE]

• $\blacktriangleright$

Each NT $\eta:F\Rightarrow G:\mathcal{C}\to\mathcal{D}$ to the NTwD $\mathsf{D}(\eta)\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}(\eta,t^{\mathsf{D}(\eta)}):\mathsf{D}(F)\Rightarrow\mathsf{D}(G):\mathsf{D}(\mathcal{C})\to\mathsf{D}(\mathcal{D})$, where $t^{\mathsf{D}(\eta)}$ is given by:

[TABLE]

for all $\Gamma\in\mathsf{D}(\mathcal{C})$ and $\Theta\in\mathscr{D}_{\mathsf{D}(\mathcal{C})}(\Gamma)$.

$\blacktriangleright$ Remark.

The domain of $\mathsf{D}$ must be $\mathsf{Ctx}\mathbb{CCC}$, not $\mathbb{CCC}$, since the domain of the functor $\mathsf{S}$ given below must be $\mathsf{ConCtx}\mathbb{CCC_{D}}$.

$\blacktriangleright$** Lemma 4.3.2**** (Well-defined $\mathsf{D}$).**

The 2-functor $\mathsf{D}$ is well-defined.

Proof.

Straightforward. ∎

Next, we need a preliminary operation before defining the 2-functor $\mathsf{S}$:

$\blacktriangleright$** Definition 4.3.3**** (Right-shifting).**

Let $\mathcal{C}$ be a constant CtxCCCwD, where $T\in\mathcal{C}$ is the specified terminal object. Given an object $\Delta\in\mathcal{C}$ such that $\Delta\neq T$, we define a D-object $\mathscr{R}_{\mathcal{C}}(\Delta)\in\mathscr{D}_{\mathcal{C}}(T)$, called the right-shifting of $\Delta$, by induction on the length of $\Delta$:

[TABLE]

together with a morphism $r_{\mathcal{C}}(\Delta):T.\mathscr{R}_{\mathcal{C}}(\Delta)\to\Delta$ and a D-morphism $\ell_{\mathcal{C}}(\Delta):\Delta\rightarrowtriangle\mathscr{R}_{\mathcal{C}}(\Delta)\{!_{\Delta}\}$ given by:

[TABLE]

$\blacktriangleright$ Notation.

We often omit the subscript $\mathcal{C}$ on $\mathscr{R}_{\mathcal{C}}$, $r_{\mathcal{C}}$ and $\ell_{\mathcal{C}}$ if it does not bring any confusion.

$\blacktriangleright$** Lemma 4.3.4**** (Right-shifting-lemma).**

Given a constant CtxCCCwD $\mathcal{C}$, where $T\in\mathcal{C}$ is the specified terminal object, the operations $\mathscr{R}_{\mathcal{C}}$, $r_{\mathcal{C}}$ and $\ell_{\mathcal{C}}$ are all well-defined, and we have:

[TABLE]

for all $\Delta\in\mathcal{C}$ such that $\Delta\neq T$.

Proof.

By induction on the length of $\Delta$. ∎

Now, we are ready to define:

$\blacktriangleright$** Definition 4.3.5**** (The 2-functor $\mathsf{S}$).**

The 2-functor $\mathsf{S}:\mathsf{ConCtx}\mathbb{CCC_{D}}\to\mathsf{Ctx}\mathbb{CCC}$ maps each constant CtxCCCwD $\mathcal{D}=(\mathcal{D},T,\_.\_,\pi,1,\Sigma,\varpi,\Pi,\mathit{dev})$ to the CtxCCC $\mathsf{S}(\mathcal{D})$ given by:

• $\blacktriangleright$

The underlying category is $\mathcal{D}$ equipped with the terminal object $T\in\mathcal{D}$;

• $\blacktriangleright$

$\mathscr{A}_{\mathsf{S}(\mathcal{D})}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\{T\}\cup\{T.\underline{A}\mid A\in\mathsf{dob}(\mathcal{D})\}$;

• $\blacktriangleright$

Given $\Delta,\Gamma\in\mathsf{S}(\mathcal{D})$, we define the product of $\Delta$ and $\Gamma$ by:

[TABLE]

• $\blacktriangleright$

Given $\Gamma,\Delta\in\mathsf{S}(\mathcal{D})$, we define the exponential $\Gamma^{\Delta}\times\Delta\stackrel{{\scriptstyle\mathit{ev}_{\Delta,\Gamma}}}{{\rightarrow}}\Gamma$, where $\Gamma^{\Delta}\stackrel{{\scriptstyle\mathrm{df.}}}{{=}}\Delta\Rightarrow\Gamma$, by induction on the length of $\Gamma$:

[TABLE]

and maps each CtxCCF $F$ and NTwD $(\eta,t)$ to their respective restrictions

[TABLE]

to 0-cells and 1-cells.

$\blacktriangleright$** Lemma 4.3.6**** (Well-defined $\mathsf{S}$).**

The 2-functors $\mathsf{S}$ is well-defined.

Proof.

Let $\mathcal{D}=(\mathcal{D},T,\_.\_,\pi,1,\Sigma,\varpi,\Pi,\mathit{dev})$ be a constant CtxCCCwD. It suffices to show that the binary products and the exponentials in $\mathsf{S}(\mathcal{D})$ are well-defined since then it is clearly contextual.

Let us first consider binary products. Given $\Theta,\Delta,\Gamma\in\mathsf{S}(\mathcal{D})$, $\phi:\Theta\to\Delta$ and $\psi:\Theta\to\Gamma$ in $\mathsf{S}(\mathcal{D})$, we define the pairing $(\phi,\psi):\Theta\to\Delta\times\Gamma$ of $\phi$ and $\psi$ to be

[TABLE]

Then, we have:

[TABLE]

and

[TABLE]

Moreover, given $\varphi:\Theta\to\Delta.\mathscr{R}_{\mathcal{C}}(\Gamma)\{!\}$ in $\mathsf{S}(\mathcal{D})$, we have:

[TABLE]

Hence, the diagram $\Delta\stackrel{{\scriptstyle p_{1}}}{{\leftarrow}}\Delta\times\Gamma\stackrel{{\scriptstyle p_{2}}}{{\rightarrow}}\Gamma$ is a well-defined product of $\Delta$ and $\Gamma$.

Next, let us consider the exponential $\Delta\Rightarrow\Gamma$ from $\Delta$ to $\Gamma$. Since the base case $\Gamma=T$ is trivial, assume $\Gamma=\Gamma^{\prime}.A$ for some $\Gamma^{\prime}\in\mathcal{D}$ and $A\in\mathscr{D}_{\mathcal{D}}(\Gamma^{\prime})$. Given $\vartheta:\Theta\times\Delta\to\Gamma^{\prime}.A$ in $\mathsf{S}(\mathcal{D})$, we define:

[TABLE]

such that:

[TABLE]

and for any $\kappa:\Theta\rightarrow(\Delta\Rightarrow\Gamma)$ in $\mathsf{S}(\mathcal{D})$ we have:

[TABLE]

which establishes that the exponential $\Delta\Rightarrow\Gamma$ in $\mathsf{S}(\mathcal{D})$ is well-defined. ∎

$\blacktriangleright$** Theorem 4.3.7**** (DS-theorem).**

There is the 2-equivalence:

[TABLE]

Proof.

First, the 2-natural isomorphism $\eta:\mathit{id}_{\mathsf{Ctx}\mathbb{CCC}}\stackrel{{\scriptstyle\sim}}{{\to}}\mathsf{S}\circ\mathsf{D}$ has the identity CtxCCF $\mathit{id}_{\mathcal{C}}:\mathcal{C}\stackrel{{\scriptstyle\sim}}{{\rightarrow}}\mathcal{C}$ as the component $\eta_{\mathcal{C}}:\mathcal{C}\stackrel{{\scriptstyle\sim}}{{\to}}\mathsf{S}\circ\mathsf{D}(\mathcal{C})$ for each CtxCCC $\mathcal{C}$, whose naturality is obvious.

Next, the 2-natural isomorphism $\epsilon:\mathsf{D}\circ\mathsf{S}\stackrel{{\scriptstyle\sim}}{{\rightarrow}}\mathit{id}_{\mathsf{ConCtx}\mathbb{CCC_{D}}}$ has for each constant CtxCCCwD $\mathcal{D}$ as the component $\epsilon_{\mathcal{D}}:\mathsf{D}\circ\mathsf{S}(\mathcal{D})\to\mathcal{D}$ the strict CCFwD $\mathsf{D}\circ\mathsf{S}(\mathcal{D})\to\mathcal{D}$ that maps objects and morphisms in $\mathsf{D}\circ\mathsf{S}(\mathcal{D})$ to themselves, D-objects $T.\underline{A}\in\mathscr{D}_{\mathsf{D}\circ\mathsf{S}(\mathcal{D})}(\Gamma)$ (resp. $T\in\mathscr{D}_{\mathsf{D}\circ\mathsf{S}(\mathcal{D})}(\Gamma)$) to $\underline{A}\{!_{\Gamma}\}\in\mathscr{D}_{\mathcal{D}}(\Gamma)$ (resp. $1\{!_{\Gamma}\}\in\mathscr{D}_{\mathcal{D}}(\Gamma)$), and D-morphisms $f\in\mathscr{D}_{\mathsf{D}\circ\mathsf{S}(\mathcal{D})}(\Gamma,T.\underline{A})$ (resp. $!_{\Gamma}\in\mathscr{D}_{\mathsf{D}\circ\mathsf{S}(\mathcal{D})}(\Gamma,T)$) to $\pi_{2}\{f\}\in\mathscr{D}_{\mathcal{D}}(\Gamma,\underline{A}\{!_{\Gamma}\})$ (resp. $\bm{!}_{\Gamma}\in\mathscr{D}_{\mathcal{D}}(\Gamma,1\{!_{\Gamma}\})$), which has the obvious inverse. For naturality of $\epsilon$, let $\mathcal{D},\mathcal{D^{\prime}}\in\mathsf{ConCtx}\mathbb{CCC_{D}}$; then, it is easy to see that the diagram {diagram} commutes by Lemma 4.2.2, which completes the proof. ∎

In particular, the 2-natural isomorphism $\epsilon:\mathsf{D}\circ\mathsf{S}\stackrel{{\scriptstyle\sim}}{{\rightarrow}}\mathit{id}_{\mathsf{ConCtx}\mathbb{CCC_{D}}}$ in the proof of Theorem 4.3.7 induces for each constant CtxCCCwD $\mathcal{D}$, an object $\Gamma\in\mathcal{D}$ and a D-object $A\in\mathscr{D}_{\mathcal{D}}(\Gamma)$ the bijective correspondence

[TABLE]

between D-morphisms $\Gamma\rightarrowtriangle A$ and morphisms $\Gamma\rightarrow T.\underline{A}$ in $\mathcal{D}$. In the term models of STLCs, this explains why we may identify terms and singleton context morphisms.

Combined with the main result in the next section, we may recover the conventional interpretation of STLCs in CCCs from our interpretation of them in CtxCCCwDs.

5 Correspondence between MLTTs and CCCwDs

In this final section, analogous to the 2-categorical correspondence between CCCs and STLCs, we establish a 2-categorical correspondence between CCCwDs and MLTTs.

5.1 Algebras for MLTTs

$\blacktriangleright$** Definition 5.1.1**** (Structures for MLTTs).**

Let $\mathcal{T}$ be an MLTT and $\mathcal{C}=(\mathcal{C},T,\_.\_,\pi,1,\Sigma,\varpi,\Pi,\mathit{dev})$ a strict CCCwD. A structure for $\mathcal{T}$ in $\mathcal{C}$ is an assignment $S$ of:

• $\blacktriangleright$

A pair of an object $S(\mathscr{F}_{\mathcal{T}}(\mathsf{C}))\in\mathcal{C}$ and a D-object $S(\mathsf{C})\in\mathscr{D}_{\mathcal{C}}(S(\mathscr{F}_{\mathcal{T}}(\mathsf{C})))$ to each type-constant $\mathsf{C}\in C_{\mathcal{T}}$;

• $\blacktriangleright$

A triple of an object $S(\mathscr{F}^{\mathit{dom}}_{\mathcal{T}}(\mathsf{F}))\in\mathcal{C}$, a D-object $S(\mathscr{F}^{\mathit{cod}}_{\mathcal{T}}(\mathsf{F}))\in\mathscr{D}_{\mathcal{C}}(S(\mathscr{F}^{\mathit{dom}}_{\mathcal{T}}(\mathsf{F})))$ and a D-morphism $S(\mathsf{F})\in\mathscr{D}_{\mathcal{C}}(S(\mathscr{F}^{\mathit{dom}}_{\mathcal{T}}(\mathsf{F})),S(\mathscr{F}^{\mathit{cod}}_{\mathcal{T}}(\mathsf{F})))$ to each term-constant $\mathsf{F}\in C_{\mathcal{T}}$.

$\blacktriangleright$** Definition 5.1.2**** (The partial interpretation of MLTTs by structures).**

Let $\mathcal{T}$ be an MLTT and $\mathcal{C}=(\mathcal{C},T,\_.\_,\pi,1,\Sigma,\varpi,\Pi,\mathit{dev})$ a strict CCCwD. Any structure $S$ for $\mathcal{T}$ in $\mathcal{C}$ induces the partial interpretation $\llbracket\_\rrbracket_{S}$ of $\mathsf{MLTT(1,\Pi,\Sigma)}$ in the induced CwF $\mathcal{C}$ that supports $1$-, $\Pi$- and $\Sigma$-types in the strict sense that extends Definition 2.2.7 to $\mathcal{T}$ by:

[TABLE]

for all type-constants $\mathsf{C}\in C_{\mathcal{T}}(\mathsf{A_{1}},\mathsf{A_{2}},\dots,\mathsf{A_{k}})$, term-constants $\mathsf{F}\in C_{\mathcal{T}}(\mathsf{A_{1}},\mathsf{A_{2}},\dots,\mathsf{A_{k}};\mathsf{B})$ and pre-context morphisms $\bm{\mathsf{f}}$.

$\blacktriangleright$ Remark.

It is partially defined because $\bm{\mathsf{f}}$ may not be a well-defined context morphism with the appropriate domain and codomain.

$\blacktriangleright$** Definition 5.1.3**** (Algebras for MLTTs).**

An algebra for an MLTT $\mathcal{T}$ (or a $\bm{\mathcal{T}}$-algebra) in a strict CCCwD $\mathcal{C}$ is a structure $S$ for $\mathcal{T}$ in $\mathcal{C}$ such that the induced partial interpretation $\llbracket\_\rrbracket_{S}$ satisfies:

• $\blacktriangleright$

If $\mathsf{C}\in C_{\mathcal{T}}(\mathsf{A_{1}},\mathsf{A_{2}},\dots,\mathsf{A_{k}})$ is a type-constant, and $\mathsf{\vdash_{\mathcal{T}}x_{1}:A_{1},x_{2}:A_{2},\dots,x_{k}:A_{k}\ ctx}$, then $\llbracket\mathsf{x_{1}:A_{1},x_{2}:A_{2},\dots,x_{k}:A_{k}}\rrbracket_{S}\simeq S(\mathscr{F}_{\mathcal{T}}(\mathsf{C}))$333It of course means that both sides are defined because so is the right-hand side. The same remark is applied to similar cases below.;

• $\blacktriangleright$

If $\mathsf{F}\in C_{\mathcal{T}}(\mathsf{A_{1}},\mathsf{A_{2}},\dots,\mathsf{A_{k}};\mathsf{B})$ is a term-constant, and $\mathsf{x_{1}:A_{1},x_{2}:A_{2},\dots,x_{k}:A_{k}\vdash_{\mathcal{T}}B\ type}$, then $\llbracket\mathsf{x_{1}:A_{1},x_{2}:A_{2},\dots,x_{k}:A_{k}}\rrbracket_{S}\simeq S(\mathscr{F}^{\mathit{dom}}_{\mathcal{T}}(\mathsf{F}))$ and $\llbracket\mathsf{B}\rrbracket_{S}\simeq S(\mathscr{F}^{\mathit{cod}}_{\mathcal{T}}(\mathsf{F}))$;

• $\blacktriangleright$

If $\mathsf{A=A^{\prime}:Ty}\in A_{\mathcal{T}}$, then $\llbracket\mathsf{A}\rrbracket_{S}\simeq\llbracket\mathsf{A^{\prime}}\rrbracket_{S}$;

• $\blacktriangleright$

If $\mathsf{a=a^{\prime}:A}\in A_{\mathcal{T}}$, then $\llbracket\mathsf{a}\rrbracket_{S}\simeq\llbracket\mathsf{a^{\prime}}\rrbracket_{S}$.

$\blacktriangleright$** Lemma 5.1.4**** (Substitution lemma).**

Let $\mathcal{T}$ be an MLTT. Given an algebra $S$ for $\mathcal{T}$ in a strict CCCwD $\mathcal{C}$, the induced interpretation $\llbracket\_\rrbracket_{S}$ of $\mathcal{T}$ in $\mathcal{C}$ satisfies:

[TABLE]

for all pre-types $\mathsf{A}$, pre-terms $\mathsf{a}$ and pre-context morphisms $\bm{\mathsf{f}}$ and $\bm{\mathsf{f}}$ in $\mathcal{T}$.

Proof.

Since the lemma has been established for $\mathsf{MLTT(1,\Pi,\Sigma)}$ by induction on the lengths of the pre-syntax $\mathsf{A}$, $\mathsf{a}$ and $\bm{\mathsf{g}}$ in [Hof97], it suffices to consider the case $\mathsf{A}\equiv\mathsf{C}(\bm{\mathsf{h}})$ and $\mathsf{a}\equiv\mathsf{F}(\bm{\mathsf{h}})$ for some $\mathsf{C}\in C_{\mathcal{T}}^{\mathsf{Ty}}$ and $\mathsf{F}\in C_{\mathcal{T}}^{\mathsf{Tm}}$. Then, observe that:

[TABLE]

for any pre-context morphism $\bm{\mathsf{f}}$ in $\mathcal{T}$. In the same manner, we may show that $\llbracket\mathsf{F}(\bm{\mathsf{h}})\rrbracket_{S}\{\llbracket\bm{\mathsf{f}}\rrbracket_{S}\}\simeq\llbracket\mathsf{F(\bm{\mathsf{h}})[\bm{\mathsf{f}}]}\rrbracket_{S}$ for any pre-context morphism $\bm{\mathsf{f}}$ in $\mathcal{T}$.

Finally, $\llbracket\bm{\mathsf{g}}\rrbracket_{S}\{\llbracket\bm{\mathsf{f}}\rrbracket_{S}\}\simeq\llbracket\bm{\mathsf{g}}\circ\bm{\mathsf{f}}\rrbracket_{S}$ for any pre-context morphisms $\bm{\mathsf{f}}$ and $\bm{\mathsf{g}}$ in $\mathcal{T}$ may be shown by induction on the length of $\bm{\mathsf{g}}$, completing the proof. ∎

$\blacktriangleright$** Theorem 5.1.5**** (Soundness of algebras for MLTTs).**

The interpretation $\llbracket\_\rrbracket_{S}$ of an MLTT $\mathcal{T}$ in a strict CCCwD $\mathcal{C}$ induced by an algebra $S$ for $\mathcal{T}$ in $\mathcal{C}$ is sound.

Proof.

It suffices to consider the additional four rules: Type-Const, Term-Const, Type-Eq and Term-Eq. Let us first consider a type $\mathsf{\Gamma\vdash C(\bm{\mathsf{f}})\ type}$ generated by the rule Type-Const, where $\mathsf{C}\in C_{\mathcal{T}}(\mathsf{A_{1}},\mathsf{A_{2}},\dots,\mathsf{A_{k}})$. Since $\mathcal{T}$ is well-formed, $\bm{\mathsf{f}}$ is a context morphism $\mathsf{\Gamma}\to\mathsf{\Delta}$ in $\mathcal{T}$, where $\mathsf{\Delta\stackrel{{\scriptstyle\mathrm{df.}}}{{\equiv}}x_{1}:A_{1},x_{2}:A_{2},\dots,x_{k}:A_{k}}$. By the induction hypothesis, $\llbracket\bm{\mathsf{f}}\rrbracket_{S}$ is a morphism $\llbracket\mathsf{\Gamma}\rrbracket_{S}\to\llbracket\mathsf{\Delta}\rrbracket_{S}$ in $\mathcal{C}$. Also, $S(\mathscr{F}_{\mathcal{T}}(\mathsf{C}))=\llbracket\mathsf{\Delta}\rrbracket_{S}$ for $S$ is a $\mathcal{T}$-algebra. Therefore, we have:

[TABLE]

Similarly, with the help of Lemma 5.1.4, we may handle the rule Term-Const. Finally, the remaining two rules Type-Eq and Term-Eq are even simpler to deal with. ∎

$\blacktriangleright$** Definition 5.1.6**** (Generic models of MLTTs).**

Let $\mathcal{T}$ be an MLTT. The generic model of $\mathcal{T}$ is a structure $G$ for $\mathcal{T}$ in the classifying CCCwD $\mathit{Cl}(\mathcal{T})$ defined by:

[TABLE]

for all type-constants $\mathsf{C}\in C_{\mathcal{T}}(\mathsf{A_{1}},\mathsf{A_{2}},\dots,\mathsf{A_{k}})$ and term-constants $\mathsf{F}\in C_{\mathcal{T}}(\mathsf{A_{1}},\mathsf{A_{2}},\dots,\mathsf{A_{k}};\mathsf{B})$.

$\blacktriangleright$** Lemma 5.1.7**** (G-lemma).**

The generic model $G$ of any MLTT $\mathcal{T}$ is an algebra for $\mathcal{T}$ in the classifying CCCwD $\mathit{Cl}(\mathcal{T})$. Moreover, the induced interpretation $\llbracket\_\rrbracket_{G}$ of $\mathcal{T}$ in $\mathit{Cl}(\mathcal{T})$ by $G$ satisfies:

$\llbracket\mathsf{\vdash\Gamma\ ctx}\rrbracket_{G}=[\mathsf{\vdash\Gamma\ ctx}]$* for any context $\mathsf{\vdash\Gamma\ ctx}$ in $\mathcal{T}$;* 2. 2.

$\llbracket\mathsf{\Gamma\vdash A\ type}\rrbracket_{G}=[\mathsf{\Gamma\vdash A\ type}]$* for any type $\mathsf{\Gamma\vdash A\ type}$ in $\mathcal{T}$;* 3. 3.

$\llbracket\mathsf{\Gamma\vdash a:A}\rrbracket_{G}=[\mathsf{\Gamma\vdash a:A}]$* for any term $\mathsf{\Gamma\vdash a:A}$ in $\mathcal{T}$;* 4. 4.

$\llbracket\mathsf{\Gamma\vdash A\ type}\rrbracket_{G}=\llbracket\mathsf{\Gamma\vdash A^{\prime}\ type}\rrbracket_{G}$* iff $\mathsf{\Gamma\vdash A=A^{\prime}\ type}$ is a theorem of $\mathcal{T}$ for any types $\mathsf{\Gamma\vdash A\ type}$ and $\mathsf{\Gamma\vdash A^{\prime}\ type}$ in $\mathcal{T}$; and* 5. 5.

$\llbracket\mathsf{\Gamma\vdash a:A}\rrbracket_{G}=\llbracket\mathsf{\Gamma\vdash a^{\prime}:A}\rrbracket_{G}$* iff $\mathsf{\Gamma\vdash a=a^{\prime}:A}$ is a theorem of $\mathcal{T}$ for any terms $\mathsf{\Gamma\vdash a:A}$ and $\mathsf{\Gamma\vdash a^{\prime}:A}$ in $\mathcal{T}$.*

Proof.

Again, it suffices to consider the four rules, but it is just straightforward. ∎

$\blacktriangleright$** Lemma 5.1.8**** (Universal property of generic models).**

Let $S$ be an algebra for an MLTT $\mathcal{T}$ in a CCCwD $\mathcal{C}$. Then, there exists a strict CCFwD $U_{S}:\mathit{Cl}(\mathcal{T})\to\mathcal{C}$ such that $U_{S}\circ\llbracket\_\rrbracket_{G}=\llbracket\_\rrbracket_{S}$, and such a CCFwD $U_{S}$ is unique up to NIwDs.

Proof.

Since the proof just follows the proof of the corresponding statement in [Pit01], here we just give a proof sketch. Let us define the CCFwD $U_{S}:\mathit{Cl}(\mathcal{T})\to\mathcal{C}$ by:

[TABLE]

It is easy to verify that $U_{S}$ is cartesian closed. Also, we may show that $U_{S}\circ\llbracket\_\rrbracket_{G}=\llbracket\_\rrbracket_{S}$ by induction on derivations of judgements. Finally, uniqueness of $U_{S}$ is straightforward to establish. ∎

$\blacktriangleright$** Definition 5.1.9**** (Morphisms between algebras for MLTTs).**

Let $\mathcal{T}$ be an MLTT, and $S$ and $R$ $\mathcal{T}$-algebras in a strict CCCwD $\mathcal{C}$. A $\bm{\mathcal{T}}$-morphisms from $S$ to $R$ is an NTwD $U_{S}\to U_{R}$.

$\blacktriangleright$** Definition 5.1.10**** (Categories of algebras for MLTTs).**

Given an MLTT $\mathcal{T}$ and a strict CCCwD $\mathcal{C}$, the category $\mathcal{T}\text{-}\mathcal{ALG}(\mathcal{C})$ is given by:

• $\blacktriangleright$

Objects are $\mathcal{T}$-algebras in $\mathcal{C}$;

• $\blacktriangleright$

Morphisms $S\to R$ are $\mathcal{T}$-morphisms from $S$ to $R$;

• $\blacktriangleright$

Composition is the vertical composition of NTwDs; and

• $\blacktriangleright$

Identities are identity NTwDs.

Given an MLTT $\mathcal{T}$, if we regard $\mathcal{T}$-algebras $S$ in a strict CCCwD $\mathcal{C}$ as the strict CCFwDs $U_{S}:\mathit{Cl}(\mathcal{T})\to\mathcal{C}$, then the category $\mathcal{T}\text{-}\mathcal{ALG}(\mathcal{C})$ is clearly a subcategory of $\mathbb{CCC_{D}}(\mathit{Cl}(\mathcal{T}),\mathcal{C})$. It then turns out that this construction constitutes the following equivalence of categories:

$\blacktriangleright$** Corollary 5.1.11**** (Equivalence between algebras and interpretations).**

Given an MLTT $\mathcal{T}$ and a strict CCCwD $\mathcal{C}$, we have $\mathcal{T}\text{-}\mathcal{ALG}(\mathcal{C})\simeq\mathbb{CCC_{D}}(\mathit{Cl}(\mathcal{T}),\mathcal{C})$.

Proof.

Let us define the functor $U^{\mathcal{T},\mathcal{C}}_{(\_)}:\mathcal{T}\text{-}\mathcal{ALG}(\mathcal{C})\to\mathbb{CCC_{D}}(\mathit{Cl}(\mathcal{T}),\mathcal{C})$ that maps $\mathcal{T}$-algebras $S$ in $\mathcal{C}$ to the induced CCFwDs $U_{S}:\mathit{Cl}(\mathcal{T})\to\mathcal{C}$, and 1- and 2-cells in $\mathcal{T}\text{-}\mathcal{ALG}(\mathcal{C})$ to themselves. Then, it suffices to show that this functor $U^{\mathcal{T},\mathcal{C}}_{(\_)}$ is essentially surjective on objects.

Let $F:\mathit{Cl}(\mathcal{T})\to\mathcal{C}$ be any CCFwD. Note that $F$ is completely determined up to NIwDs by its restriction to types of the form $\mathsf{\Gamma\vdash_{\mathcal{T}}C(\bm{\mathsf{f}})\ type}$, where $\mathsf{C}\in C_{\mathcal{T}}^{\mathsf{Ty}}$, and terms of the form $\mathsf{\Gamma\vdash_{\mathcal{T}}F(\bm{\mathsf{f}}):B(\bm{\mathsf{f}})}$, where $\mathsf{F}\in C_{\mathcal{T}}^{\mathsf{Tm}}$. But then, this restriction of $F$ clearly defines a $\mathcal{T}$-algebra $S$ in $\mathcal{C}$ such that $U_{S}\cong F$, which completes the proof. ∎

5.2 Theory-Category Correspondence between MLTTs and CCCwDs

$\blacktriangleright$** Definition 5.2.1**** (The 2-category $\mathbb{MLTT}$).**

The 2-category $\mathbb{MLTT}$ is given by:

• $\blacktriangleright$

0-cells are MLTTs;

• $\blacktriangleright$

The hom-category $\mathbb{MLTT}(\mathcal{T},\mathcal{T^{\prime}})$ for each pair $\mathcal{T},\mathcal{T^{\prime}}\in\mathbb{MLTT}$ is $\mathcal{T}\text{-}\mathcal{ALG}(\mathit{Cl}(\mathcal{T^{\prime}}))$;

• $\blacktriangleright$

The composition functor $\mathbb{MLTT}(\mathcal{T},\mathcal{T^{\prime}})\times\mathbb{MLTT}(\mathcal{T^{\prime}},\mathcal{T^{\prime\prime}})\to\mathbb{MLTT}(\mathcal{T},\mathcal{T^{\prime\prime}})$ for each triple $\mathcal{T},\mathcal{T^{\prime}},\mathcal{T^{\prime\prime}}\in\mathbb{MLTT}$ is given by the composition of CCFwDs and the horizontal composition of NTwDs; and

• $\blacktriangleright$

The functor $1\to\mathbb{MLTT}(\mathcal{T},\mathcal{T})$ for each $\mathcal{T}\in\mathbb{MLTT}$ maps the unique object $\star\in 1$ to the generic model $G$ of $\mathcal{T}$ and the unique morphism $\mathit{id}_{\star}$ to the identity NTwD $\mathit{id}_{U_{G}}$.

Note that the 2-category $\mathbb{MLTT}$ is essentially the sub-2-category of $\mathbb{CCC_{D}}$ whose 0-cells are the classifying CCCwDs of MLTTs, and 1-cells are the CCFwDs $U_{S}$ induced by algebras $S$ for MLTTs. Thus, it is easy to see that $\mathbb{MLTT}$ is a well-defined 2-category. Moreover, we have:

$\blacktriangleright$** Theorem 5.2.2**** (Theory-category correspondence between MLTTs and CCCwDs).**

The 2-categories $\mathbb{MLTT}$ and $\mathbb{CCC_{D}}$ are 2-equivalent. More precisely, the 2-functor $\mathit{Cl}:\mathbb{MLTT}\to\mathbb{CCC_{D}}$ is essentially surjective on objects, and the functor $\mathit{Cl}_{\mathcal{T},\mathcal{T^{\prime}}}:\mathbb{MLTT}(\mathcal{T},\mathcal{T^{\prime}})\to\mathbb{CCC_{D}}(\mathit{Cl}(\mathcal{T}),\mathit{Cl}(\mathcal{T^{\prime}}))$ constitues an equivalence $\mathbb{MLTT}(\mathcal{T},\mathcal{T^{\prime}})\simeq\mathbb{CCC_{D}}(\mathit{Cl}(\mathcal{T}),\mathit{Cl}(\mathcal{T^{\prime}}))$ for all $\mathcal{T},\mathcal{T^{\prime}}\in\mathbb{MLTT}$.

Proof.

By Corollary 5.1.11, it suffices to show that the 2-functor $\mathit{Cl}$ is essentially surjective on objects. Then, given a CCCwD $\mathcal{C}$, the standard ‘theory-construction’ $\mathit{Th}$ induces an MLTT $\mathit{Th}(\mathcal{C})$ such that $\mathit{Cl}(\mathit{Th}(\mathcal{C}))\cong\mathcal{C}$, which completes the proof. ∎

6 Conclusion and Future Work

We have generalized CCCs, viz., CCCwDs, and proved that they give a categorical semantics of MLTTs in a true-to-syntax fashion. We have also analyzed the relation between the standard interpretation of STLCs in CCCs and ours in CCCwDs by establishing a 2-equivalence between CtxCCCs and constant CtxCCCwDs. For these results, it would be fair to say that we have discovered the categorical counterpart of the path from STTs to DTTs.

As immediate future work, we would like to consider additional structures on CCCwDs to interpret other type constructions in MLTTs, e.g., identity types, well-founded tree types and universes. Moreover, it may be possible to extend the present framework as a semantics of homotopy type theory (HoTT) [Uni13]. Finally, it would be interesting to develop a general theory of categories with dependence in its own right, generalizing major theorems in category theory.

Acknowledgements.

The author was supported by Funai Overseas Scholarship. Also, he is grateful to Samson Abramsky for fruitful discussions.