\(\newcommand{\ottnt}[1]{\mathit{#1}}\newcommand{\ottmv}[1]{\mathit{#1}}\newcommand{\ottkw}[1]{\mathbf{#1}}\newcommand{\ottsym}[1]{#1}\newcommand{\ottcom}[1]{\text{#1}}\newcommand{\ottcomplu}[5]{\overline{#1}^{\,#2\in #3 #4 #5}}\newcommand{\ottcompu}[3]{\overline{#1}^{\,#2<#3}}\newcommand{\ottcomp}[2]{\overline{#1}^{\,#2}}\)

In the last post I talked about the need for a categorical proof theory of BINT. In this post I would like to start laying out an idea for how we can obtain one for Dualized Type Theory (DTT). At first I had planned on laying this post out as a private note, but I decided to make it public to try and get feedback. I am not sure if my idea already exists or not, and if the reader knows please do tell me! Now in this post I only detail the initial categorical framework I will interpret DTT in, and so, I will be presenting filtered categories as multicategories, but the final model we will eventually arrive at in a future post will be a polycategorical version of what is described here. However, the latter has its own hurdles to get through, and I am still trying to understand those hurdles.

A filtered category (FC) can be thought of as starting with an arbitrary multicategory, say \(\mathcal{C}\), and layering over the top of it another category, say \( \mathcal{F} \) (the filter). The following image illustrates this idea:

The job of this layer is to act as a filter, and only let through specific structures. The above image captures this idea by having the filter, \(\mathcal{F}\) over \(\mathcal{C}\), and the filter is shown by making the filter layer a little transparent so that we can only make out some of the bottom layer. The way in which the filter will restrict \(\mathcal{C}\) will become more apparent when we give the definition of a FC. In fact, lets do that now.

### Filtered Categories

A **filtered category (FC)** is a multicategory defined in terms of two structures given by a pair denoted \(\ottsym{(} \mathcal{C} \downarrow \mathsf{Cat}( \mathcal{W} ) \ottsym{)} \) where \(\mathcal{C}\) is a multicategory called the lax component, \(\mathcal{W}\) is a collection of worlds, and \( \mathsf{Cat}( \mathcal{W} ) \) is \( \mathcal{W} \times \mathcal{W} \) considered as a category which we call the constraint universe of the FC. A FC, \(( \mathcal{C} \downarrow \mathsf{Cat}( \mathcal{W} ) )\), is defined as follows:

**(Objects)**A collection of objects each denoted \(\ottmv{A} \ottsym{@} \ottmv{w}\), where \( \ottmv{A} \in \mathsf{Obj}( \mathcal{C} ) \) and \( \ottmv{w} \in \mathcal{W} \).**(Morphisms)**A collection of multimorphisms. Each morphism is a triple \((f , M, \{(\ottmv{A_{{\mathrm{1}}}},\ottmv{w_{{\mathrm{1}}}}),\ldots,(\ottmv{A_{\ottmv{m}}},\ottmv{w_{\ottmv{m}}}),(B,w)\})\) where \(f \in \mathcal{C} \ottsym{(} \ottmv{A_{{\mathrm{1}}}} \ottsym{,} \, … \, \ottsym{,} \ottmv{A_{\ottmv{m}}} \ottsym{,} \ottmv{B} \ottsym{)} \), \(M\) — the morphism constraints — is a subcategory of \( \mathsf{Cat}( \mathcal{W} ) \), such that, \(\{\ottmv{w_{{\mathrm{1}}}},\ldots,\ottmv{w_{\ottmv{m}}},\ottmv{w}\} \subseteq \mathsf{Obj}( \ottmv{M} ) \). We denote each morphism by \(f : \ottmv{M}; \ottmv{A_{{\mathrm{1}}}} \ottsym{@} \ottmv{w_{{\mathrm{1}}}},\ldots,\ottmv{A_{\ottmv{m}}} \ottsym{@} \ottmv{w_{\ottmv{m}}} \to \ottmv{B} \ottsym{@} \ottmv{w}\).**(Identities)**For any list of objects, \(\ottmv{A_{{\mathrm{1}}}} \ottsym{@} \ottmv{w_{{\mathrm{1}}}}, \ldots, \ottmv{A} \ottsym{@} \ottmv{w}, \ldots, \ottmv{A_{\ottmv{i}}} \ottsym{@} \ottmv{w_{\ottmv{i}}}\) there is a morphism \(\mathsf{id} : M;\ottmv{A_{{\mathrm{1}}}} \ottsym{@} \ottmv{w_{{\mathrm{1}}}}, \ldots, \ottmv{A} \ottsym{@} \ottmv{w}, \ldots, \ottmv{A_{\ottmv{i}}} \ottsym{@} \ottmv{w_{\ottmv{i}}} \to \ottmv{A} \ottsym{@} \ottmv{w}\).**(Vertical Composition)**For any two morphisms \(f \in \ottsym{(} \mathcal{C} \downarrow \mathsf{Cat}( \mathcal{W} ) \ottsym{)} ( \ottmv{M} ; \ottmv{A_{{\mathrm{1}}}} @ \ottmv{w_{{\mathrm{1}}}} , \ldots, \ottmv{A_{\ottmv{i}}} @ \ottmv{w_{\ottmv{i}}} , \ottmv{B} @ \ottmv{w’} ) \) and

\(g \in \ottsym{(} \mathcal{C} \downarrow \mathsf{Cat}( \mathcal{W} ) \ottsym{)}(M';C_{{\mathrm{1}}} \ottsym{@} \ottmv{w’_{{\mathrm{1}}}}, \ldots, \ottmv{B} \ottsym{@} \ottmv{w’}, \ldots,C_{\ottmv{j}} \ottsym{@} \ottmv{w’_{\ottmv{j}}}, \ottmv{D} \ottsym{@} \ottmv{w”})\) their composition is also a morphism, that is, \(f;g \in \ottsym{(} \mathcal{C} \downarrow \mathsf{Cat}( \mathcal{W} ) \ottsym{)}(M,M';C_{{\mathrm{1}}} \ottsym{@} \ottmv{w’_{{\mathrm{1}}}},\ldots,\ottmv{A_{{\mathrm{1}}}} \ottsym{@} \ottmv{w_{{\mathrm{1}}}},\ldots,\ottmv{A_{\ottmv{i}}} \ottsym{@} \ottmv{w_{\ottmv{i}}},\ldots,C_{\ottmv{j}} \ottsym{@} \ottmv{w’_{\ottmv{j}}},\ottmv{D} \ottsym{@} \ottmv{w”})\).**(Horizontal Source Composition)**For any morphisms \(f \in \ottsym{(} \mathcal{C} \downarrow \mathsf{Cat}( \mathcal{W} ) \ottsym{)}(M;A_1@w_1, \ldots, A@w, \ldots,A_n@w_n,B@w”)\) and \(\alpha \in M(w,w’) \) the horizontal composition \(f \rightharpoonup \alpha :M;A_1@w_1, \ldots, A@w’, \ldots,A_n@w_n,B@w” \) is also a morphism.**(Horizontal Target Composition)**For any morphisms \(f \in \ottsym{(} \mathcal{C} \downarrow \mathsf{Cat}( \mathcal{W} ) \ottsym{)}(M;A_1@w_1, \ldots, A_n@w_n,B@w)\) and \(\alpha \in M(w,w’) \) the horizontal target composition \(f \rightharpoondown \alpha :M;A_1@w_1, \ldots, A_n@w_n,B@w’ \) is also a morphism.- Finally, we have the following axioms:
**(Vertical Identity)**For any morphism \( f \in \ottsym{(} \mathcal{C} \downarrow \mathsf{Cat}( \mathcal{W} ) \ottsym{)}(M;A_1@w_1, \ldots, A@w, \ldots, A_i@w_i,B@w’)\) we have \(f ; \mathsf{id}_{B@w’} = f = \mathsf{id}_{A@w};f \).**(Associativity of Vertical Composition)**For any morphisms\( f \in ( \mathcal{C} \downarrow \mathsf{Cat}( \mathcal{W} ) )(M_1;A_1@w_1, \ldots, A_i@w_i,B@w’)\),\( g \in \ottsym{(} \mathcal{C} \downarrow \mathsf{Cat}( \mathcal{W} ) \ottsym{)}(M_2;B_1@w_1, \ldots, B@w’, \ldots, B_i@w_i,C@w”)\), and \( h \in \ottsym{(} \mathcal{C} \downarrow \mathsf{Cat}( \mathcal{W} ) \ottsym{)}(M_3;C_1@w_1, \ldots, C@w”, \ldots, C_i@w_i,D@w”’)\) we have \(f;(g;h) = (f;g);h\).**(Horizontal Source Identity)**For any morphism \( f \in \ottsym{(} \mathcal{C} \downarrow \mathsf{Cat}( \mathcal{W} ) \ottsym{)}(M;A_1@w_1, \ldots, A@w, \ldots, A_i@w_i,B@w’)\) we have \(f \rightharpoonup \mathsf{id}_w = f\).**(Horizontal Source Unfold)**For any morphisms \(f \in \ottsym{(} \mathcal{C} \downarrow \mathsf{Cat}( \mathcal{W} ) \ottsym{)}(M;A_1@w_1, \ldots, A@w, \ldots,A_n@w_n,B@w”’)\), \(\alpha_1 \in M(w,w’) \), and \(\alpha_2 \in M(w’,w”) \) we have \(f \rightharpoonup (\alpha_1;\alpha_2)\) = \((f \rightharpoonup \alpha_1) \rightharpoonup \alpha_2\).**(Horizontal Source Symmetry)**For any morphisms \(f \in \ottsym{(} \mathcal{C} \downarrow \mathsf{Cat}( \mathcal{W} ) \ottsym{)}(M;A_1@w_1, \ldots, A@w, \ldots,A_n@w_n,B@w”’)\), \(\alpha_1 \in M(w,w’) \), and \(\alpha_2 \in M(w’,w) \) we have \(f = f \rightharpoonup (\alpha_1;\alpha_2)\).**(Horizontal Target Identity)**For any morphism \( f \in \ottsym{(} \mathcal{C} \downarrow \mathsf{Cat}( \mathcal{W} ) \ottsym{)}(M;A_1@w_1, \ldots, A_i@w_i,B@w)\) we have \(f \rightharpoondown \mathsf{id}_w = f\).**(Horizontal Target Unfold)**For any morphisms \(f \in \ottsym{(} \mathcal{C} \downarrow \mathsf{Cat}( \mathcal{W} ) \ottsym{)}(M;A_1@w_1, \ldots,A_n@w_n,B@w)\), \(\alpha_1 \in M(w,w’) \), and \(\alpha_2 \in M(w’,w”) \) we have \(f \rightharpoondown (\alpha_1;\alpha_2)\) = \((f \rightharpoondown \alpha_1) \rightharpoondown \alpha_2\).**(Horizontal Target Symmetry)**For any morphisms \(f \in \ottsym{(} \mathcal{C} \downarrow \mathsf{Cat}( \mathcal{W} ) \ottsym{)}(M;A_1@w_1, \ldots,A_n@w_n,B@w)\), \(\alpha_1 \in M(w,w’) \), and \(\alpha_2 \in M(w’,w) \) we have \(f = f \rightharpoondown (\alpha_1;\alpha_2)\).**(Horizontal-Vertical Symmetry)**For any morphisms \(f \in \ottsym{(} \mathcal{C} \downarrow \mathsf{Cat}( \mathcal{W} ) \ottsym{)}(M;A_1@w_1, \ldots,A_n@w_n,B@w)\), \(\alpha_1 \in M(w_i,w’_i) \), and \(\alpha_2 \in M(w,w’) \) we have \((f \rightharpoonup \alpha_1) \rightharpoondown \alpha_2)\) = \((f \rightharpoondown \alpha_2)\rightharpoonup \alpha_1)\).

The categories on morphisms should be thought of as being constraints on particular morphisms, and thus, the only part of the category that matters is the set of morphisms. So we will denote these categories as simply lists of morphisms, that is, \( \ottmv{w_{{\mathrm{1}}}} \leq \ottmv{w_{{\mathrm{2}}}} , \ldots, \ottmv{w_{\ottmv{i}}} \leq \ottmv{w}_{i+1}\) but with the additional property that this list should be a category, and hence, identity and composition morphisms must be present. That being said, these constraint categories could get large due to having to have identities for every object, and the composition morphisms, so we will often only list out the non-trivial morphisms and leave the existence of the identity and composition morphisms implicit. The notation \(\ottmv{M_{{\mathrm{1}}}},\ottmv{M_{{\mathrm{2}}}}\) for categories \(\ottmv{M_{{\mathrm{1}}}}\) and \(\ottmv{M_{{\mathrm{2}}}}\) is a combination operation. This notation stands for the category defined as the union of the two categories.

- \( \mathsf{Obj}( \ottmv{M_{{\mathrm{1}}}} \ottsym{,} \ottmv{M_{{\mathrm{2}}}} ) = \mathsf{Obj}( \ottmv{M_{{\mathrm{1}}}} ) \cup \mathsf{Obj}( \ottmv{M_{{\mathrm{2}}}} ) \)
- For any objects \(A,B \in \mathsf{Obj}( \ottmv{M_{{\mathrm{1}}}} \ottsym{,} \ottmv{M_{{\mathrm{2}}}} ) \), either \((\ottmv{M_{{\mathrm{1}}}} \ottsym{,} \ottmv{M_{{\mathrm{2}}}})(A,B) = \ottmv{M_{{\mathrm{1}}}}(A,B)\) if \(A,B \in \ottmv{M_{{\mathrm{1}}}}\), or \((\ottmv{M_{{\mathrm{1}}}} \ottsym{,} \ottmv{M_{{\mathrm{2}}}})(A,B) = \ottmv{M_{{\mathrm{2}}}}(A,B)\) if \(A,B \in \ottmv{M_{{\mathrm{2}}}}\).

Keeping with the theme of representing the constraint categories as lists of non-trivial morphisms we define the union — the operation defined above — of \(\ottmv{M_{{\mathrm{1}}}} = \ottmv{w_{{\mathrm{1}}}} \leq \ottmv{w_{{\mathrm{2}}}} , \ldots, \ottmv{w_{\ottmv{i}}} \leq \ottmv{w}_{i+1}\) and \(\ottmv{M_{{\mathrm{2}}}} = \ottmv{w’_{{\mathrm{1}}}} \leq \ottmv{w’_{{\mathrm{2}}}} , \ldots, \ottmv{w’_{\ottmv{j}}} \leq \ottmv{w’}_{j+1}\) as \(\ottmv{M_{{\mathrm{1}}}} \ottsym{,} \ottmv{M_{{\mathrm{2}}}} = \ottmv{w_{{\mathrm{1}}}} \leq \ottmv{w_{{\mathrm{2}}}} , \ldots, \ottmv{w_{\ottmv{i}}} \leq \ottmv{w}_{i+1}, \ottmv{w’_{{\mathrm{1}}}} \leq \ottmv{w’_{{\mathrm{2}}}} , \ldots, \ottmv{w’_{\ottmv{j}}} \leq \ottmv{w’}_{j+1} \).

### Some Intuition

The best intuition I can give for a FC, \( \mathcal{C} \downarrow \mathsf{Cat}( \mathcal{W} ) \), is to think about the elements of \(\mathcal{W}\) as worlds where objects of \(\mathcal{C}\) live. Then one should think of the morphisms of \( \mathsf{Cat}( \mathcal{W} ) \) as transitions between the worlds. Thus, the reader familiar with Kripke models should be able to see that we are considering \( \mathsf{Cat}( \mathcal{W} ) \) as imposing a Kripke like structure over \(\mathcal{C}\).

Now horizontal composition corresponds to monotonicity if we think of a morphism as a proof of its target assuming its list of source objects. Notice, that horizontal composition only moves forward, that is because, when formulas are true in a Kripke model we can only move them forward along the transition relation. So since there is no negation here we can only move forward.

### Examples

- \(\mathsf{Lax}(A@w) = A\)
- \(\mathsf{Lax}(f : \mathsf{Cat}(\mathcal{W});A_1@w,\ldots,A_i@w \to B@w) = f : A_1,\ldots,A_i \to B\)
- \(\mathsf{Filtered}(A) = A@w\)
- \(\mathsf{Filtered}(f : A_1,\ldots,A_i \to B) = f : \mathsf{Cat}(\mathcal{W});A_1@w,\ldots,A_i@w \to B@w\)

### Functors

One can define functors between filtered categories:

**functor**, \(H\), between two FCs \((\mathcal{C_1}\downarrow\mathsf{Cat}(\mathcal{W}_1))\) and \((\mathcal{C_2}\downarrow\mathsf{Cat}(\mathcal{W}_2))\) is a pair of functors \((F : \mathcal{C}_1 \to \mathcal{C}_2, G : \mathsf{Cat}(\mathcal{W}_1) \to \mathsf{Cat}(\mathcal{W}_2) )\) defined as follows:

- (Objects) \(H(A@w) = F(A)@G(w)\)
- (Morphisms) \(H(f : M;A_1@w_1,\ldots,A_i@w_i \to B@w) =\)

\(F(f) : G(M);F(A_1)@G(w_1),\ldots,F(A_i)@G(w_i) \to F(B)@G(w)\)

Since \(F\) and \(G\) are functors \(H\) will respect both vertical and horizontal compositions as well as identities.

### Structures in FCs

FCs can have two different types of structures: structures inherited from the lax component, and structures global to the FC. The latter are the usual structures built from morphisms such as products, co-products, and exponentials. However, the former are structures that are constrained versions of the structures in the lax component. Defining these is were the constraints are really going to come into play. Now there are lots of ways one could constrain the structures of the lax component using the constraint universe. The following are examples of the types of structures I will need when interpreting DIL/DTT. Throughout this section I will denote lists of objects of an FC by \(\Gamma\) and \(\Delta\).

**pointed initial object**, denoted \(\perp @ w \), if for any category \(M\), worlds \(w,w’ \in \mathsf{Obj}(M)\), sequences of objects \(\Gamma\) and \(\Delta\), and object \(A@w’ \in \mathsf{Obj}(\mathcal{C}\downarrow\mathcal{W})\), there exists a unique morphism \(\triangle : M; \Gamma,\perp@w,\Delta \to A@w’\).

**pointed final object**, denoted \(\top @ w \), if for any category \(M\), world \(w \in \mathsf{Obj}(M)\), and sequence of objects \(\Gamma\), there exists a unique morphism \(\nabla : M; \Gamma \to \top @ w\).

**pointed products**, if for any category \(M\), world \(w \in \mathsf{Obj}(M)\), two objects \(A@w\) and \(B@w\) of \((\mathcal{C}\downarrow\mathcal{W})\), and morphisms \(f : M_1; \overrightarrow{C@w’} \to A@w\) and \(g : M_2 ; \overrightarrow{C@w’} \to B@w\), there is an object denoted \((A \times B)@w\), two morphisms \(\pi_1 : M ; (A \times B)@w \to A@w\) and \(\pi_2 : M ; (A \times B)@w \to B@w\), and there exists a unique morphism

\(\langle f,g\rangle : M_1,M_2; \overrightarrow{C@w’} \to (A \times B)@w\) in \((\mathcal{C}\downarrow\mathcal{W})\) where the following diagram commutes:

We call a FC

**pointed cartesian**if all finite pointed products exist, and there exists a pointed final object.

**pointed co-products**, if for any category \(M\), world \(w \in \mathsf{Obj}(M)\), two objects \(A@w\) and \(B@w\) of \((\mathcal{C}\downarrow\mathcal{W})\), and morphisms \(f : M_1; A@w \to C@w’\) and \(g : M_2 ; B@w \to C@w’\), there is an object denoted \((A + B)@w\), two morphisms \(\iota_1 : M ; A@w \to (A + B)@w\) and \(\iota_2 : M ; B@w \to (A + B)@w\), and there exists a unique morphism

\([f,g] : M_1,M_2; (A + B)@w \to C@w’\) in \((\mathcal{C}\downarrow\mathcal{W})\) where the following diagram commutes:

We call a FC

**pointed bi-cartesian**if all finite pointed co-products exist, and there exists a pointed inital object.

I think I will leave this post here. This is just a look at what I am considering. In the close future I will be thinking about internal homs in FC, and generalizing to polycategories, then after these are figured out, we will be able to interpret DIL and DTT in a categorical framework.