# A Fibrational Approach to Multiplicative Additive Indexed Linear Logic

Flavien Breuvart, Thomas Ehrhard, Nicolas Munnich, Federico Olimpieri

<figure><img src="image_1.png" /></figure>

## To cite this version:

Flavien Breuvart, Thomas Ehrhard, Nicolas Munnich, Federico Olimpieri. A Fibrational Approach to Multiplicative Additive Indexed Linear Logic. 2023. hal-03978764

HAL Id: hal-03978764

https://hal.science/hal-03978764

Preprint submitted on 8 Feb 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>
# A Fibrational Approach to Multiplicative Additive Indexed Linear Logic*

Flavien Breuvart¹, Thomas Ehrhard², Nicolas Munnich¹, and
Federico Olimpieri³

¹Univ. USPN, Sorbonne Paris Cité, LIPN, UMR 7030, CNRS, F-93430 Villetaneuse, France

²Université Paris Cité, CNRS, IRIF, F-86013, Paris, France

³School of Mathematics, University of Leeds, U

8th February 2023

## Abstract

In this paper, we achieve a modular and fairly concise presentation of the semantic ideas that lie behind the multiplicative-additive fragment of indexed linear logic. We generalize the basic definition of its syntax, utilizing objects of appropriate categories, referred to as “loci”, in place of sets of resources. We prove that this generalized proof system enjoys cut-elimination. We then present its semantics, exploiting the notion of categorical fibration. We interpret formulae defined under a loci as elements of its fiber. We observe that, while multiplicative connectives (i.e., the star-autonomous structure) are confined to each fiber, the additives (i.e., the product and coproduct structures) live within the entire fibration. Finally, we build various examples of categorical models for our system.

## 1 Introduction

*Indexed Linear Logic (IndLL)* has been introduced by Bucciarelli and Ehrhard [3, 4] as a syntactic counterpart to some aspects of linear logic relational semantics. The semantic analysis brought to the discovery that one could define an extension of linear logic, where formulae and proofs depends on a *choice of resources*. A significant outcome of this extension is the capability to disregard this choice and recover standard linear logic formulae and proofs. Intuitively, an indexed formula can be understood as an indexed family of elements that live in the relational interpretation of its underlying linear logic formula.

The present paper, together with its sequel, are an attempt to *modularize* and model IndLL, twenty years after. Since the initial publications on the topic, a number of logics have undergone modularization, that is, they have been defined with respect to some external algebraic structure. This structure provides

<footnote>*The authors are supported by ANRJCJC project CoGITARe</footnote>
means for analysis and/or inference, but is irrelevant from a purely logical per-
spective. Examples of such logics include type systems with graded monads
and/or graded exponentials [11, 9], which are structurally similar to indexed
linear logic. However, these systems are deficient in two key areas:

1. The ability to analyse *computational resources*.

2. The capacity to capture the structure of LL-additives, that correspond to algebraic data types in functional languages.

**Relations between Resources: towards relational abstraction.** As shown recently [14], type system with graded exponentials [2, 12] can be considered as a higher order variant of non-relational and backward imperative abstract interpretations. Specifically, it has been shown that the second can be simulated within the first-order fragment of the first. The backward restriction, which arises from the utilization of graded comonads rather than graded monads, is not a significant limitation. However, the non-relational restriction is critical for many practical uses of abstract interpretation such as the so called polyhedral interpretation (that use linear inequations between variables).

At higher order, this absence of relations is even more restrictive, as the
scope of relations is much more varied. In our work, we are interested in a
specific kind of relation: one that would bind differently each occurrence of the
same argument/result.

To give some intuition about the shortcomings of graded systems that we
aim to address, we discuss a particular example. Consider the higher order sum
function that takes a function $f$ on integers, an integer $n$ and sum each $f(n)$.
One can bound the number of times the function is called and the size of the
integer, but this has to be done separately so that, the type of our program
would be something like $!_{\le 3}(\mathbb{N}_{\le 3} \to \mathbb{N}) \to !_1\mathbb{N}_{\le 3} \to \mathbb{N}$ which says that given
an integer bounded by 3 you use your function at most 3 times over integers
bounded by 3, and you can do this for every $n$ in place of 3. Of course, we
can have a polymorphic version $\forall n, !_{\le n}(\mathbb{N}_{\le n} \to \mathbb{N}) \to !_1\mathbb{N}_{\le n} \to \mathbb{N}$. In our work,
we focus on an orthogonal generalization that consists in bounding differently
each usage of $f$. In this case, we would like to say that given an integer $n$ the
function is used $n$ times, one for each $i \le n$: $\forall n, !_{i \in [1...n]}(\mathbb{N}_n \to \mathbb{N}) \to !_1\mathbb{N}_{\le n} \to \mathbb{N}$.
This kind of analysis could be useful, for example, to quantify the speedup of a
memoized function call (i.e., from Call-by-Need).

Solving this kind of issues is one of our long-term goals, and we believe that
they can be properly addressed by means of *indexed exponentials*. This is one
the main sources for our interest in indexed linear logic.

**Additive Behaviour: recovering Seely isomorphism.** In BLL generalizations, additives are treated by forced over/under approximation. For example, in a list structure we cannot distinguish the behaviour of the first element from the others. This is often acceptable for coarse analyses but critical for fined grained ones. In Indexed linear logic, the additives are central and their structure has to be respected. This is, to our knowledge, a unique trait among logics offering an access to the quantitative behaviour of the typed program.

Additives are crucial to treat algebraic data types, but also for reasoning
on integers or even Booleans. Over-approximations of the additive “or” means
that our analysis will always take the *sup* when treating conditionals, which is
unsatisfactory. Over-approximations of the additive “and” is even worst: if one
use one component of a tuple and then another, the tuple is considered used
*twice*.

From a purely linear logic point-of-view, disregarding additives is also dan-
gerous. Seely isomorphisms !$A\otimes!B \simeq!$(A & B) are indeed crucial to properly
understand the subtleties of the linear structure.

**IndLL: a logic of Intersection Types.** Introduced in the early 2000's to study sequentiality, indexed linear logic (IndLL) [3, 4] was never investigated structurally despite its most fundamental property: it is equivalent to *uniform intersection types* [7]. By uniform we mean intersection types that are refinement of a same formula of linear logic (or the same simple type when restricted to the $\lambda$-calculus). Hence, Intersections are only allowed between types of the same 'shape'. The main interest, for us, is that this uniform restriction allows intersection types to be presented as a *logic system* contained in IndLL, as shown in [7]. This restriction to "uniform" intersection types can be simply understood as focusing on typed programming languages. Here the "intersection type" is considered a *posteriori* or *à la Curry*, while the "simple types" of programs are considered a *posteriori* or *à la Church*. Our generalization of the indexed system could then produce a *modular* notion of uniform intersection types. This would lead to a purely logical and remarkably general approach to intersection types, that is quite different in nature from the others known approaches in the literature, such as [16, 21]. However, the proper development of this line of research needs the exponential structure, hence we leave these speculations to future work.

**Main Results** Following Bucciarelli and Ehrhard's original presentation choice of IndLL, in the present paper we are only investigating its multiplicative-additive fragment. The work that we perform here has to be thought of as propedeutic to the proper handling of the indexed exponential structure. Our system is parametric on the choice of an appropriate extensive category, hereafter called category of loci. This means that, for each category of loci $\emptyset$ we have a different indexed linear logic, that we call MAInd$_{\emptyset}$LL.

We choose to maintain the focus of the paper on the comparison with linear
logic and its traditional models. We hope that these links will motivate our con-
struction, justify our definition of models, but also allow to further the analysis
and refinement of existing models.

**Structure** Section 2 aims make our work as self-contained as possible and can be skipped by the reader who has enough categorical background. The real article begin with Section 3 which gives a gentle presentation of our work. It is followed by the necessary technical presentation of our modular logic and its categorical semantics in Section 4. The remaining two sections present some concrete models, or more precisely, some general methods to build models. Indeed, since the logic is parametric on the choice of $\emptyset$, a particular model only make sense for a given choice; to fully appreciate the parametricity of our construction, we then present two general ways to produce categorical semantics for our systems.
## 2 Categorical Preliminaries

In this section we recall some categorical notions that are crucial for our work.

**Notations and Conventions** Given a category $\mathbb{C}$ and morphisms $f \in \mathbb{C}(A, B)$, $g \in \mathbb{C}(B, C)$, we denote as $f; g$ their composition. Given a cocartesian monoidal category $(\mathbb{C}, +, \emptyset)$, we use the notations $\rho : A \cong \emptyset + A$, $\lambda : A \cong A + \emptyset$, $\text{init} : \emptyset \to A$, $\iota_1 : A \to A + B$, $\iota_2 : B \to A + B$ and $\nabla : A + A \to A$ for the usual natural transformations of cocartesian categories.

**Extensivity** Intuitively, an extensive category is a category with finite coproducts $(+, \emptyset)$ where the injections can be tracked along all morphisms in a coherent way, i.e., where, for any $f : X \to Y_1 + Y_2$, there is a decomposition of $X$ and $f$ as appropriate coproducts.

**Definition 2.1** (Extensive category [6]). Let $(\mathbb{C}, +, \emptyset)$ be a cocartesian category where $\emptyset$ is initial. An extensive category is such a category $\mathbb{C}$ in which pullbacks of finite coproduct injections along arbitrary morphisms $g$ exist, and for which, in any commutative diagram:

<figure><img src="image_3.png" /></figure>

the two squares are pullbacks if and only if the top row is a coproduct diagram. In this case, $Y = X + Z$ and we use the notation $g|_A := f$ and $g|_B := h$. Notice that this implies that $\emptyset$ is strict (i.e., the only morphism targeting $\emptyset$ is the identity).

**Example 2.2.** The following are extensive categories:

* the category FinSet of finite sets and functions,

* the category Set of all sets and functions,

* the category Graph of graphs and graph morphisms,

* the category Top of topological spaces and continuous functions,

* the initial category $\mathbb{1}$ with a sole object and a sole morphism,

* the thin category $\mathbb{2}$ with two objects and a unique non-id morphism between the two objects.

**Star-Autonomous Categories** Star-autonomous categories are wildly accepted as categorical semantics for classical multiplicative linear logic (MLL).

**Definition 2.3** (Star-Autonomous Category). A star-autonomous category is a symmetric monoidal closed category $(\mathbb{C}, \otimes, \mathbb{1}, -\emptyset)$ with a contravariant functor $(-)^\perp : \mathbb{C}^\perp \to \mathbb{C}$ that is weakly involutive $(A^\perp)^\perp \cong A$, and such that $A \dashv B = (A \otimes B^\perp)^\perp$. We denote as StAut the category of star-autonomous categories and structure-preserving functors.
We use the following notation for the closed structure:

$$ \mathbb{C}(A \otimes B, C) \underset{\text{uncur}(-) \leftarrow}{\overset{\text{cur}(-)}{\rightleftharpoons}} \mathbb{C}(A, B \dashv C) . $$

**Definition 2.4 (Models of MALL).** A model of MALL consists of a star-autonomous category $(\mathbb{C}, \mathbb{1}, \otimes, (-)^{\perp})$ equipped with a cartesian product structure $(\mathbb{0}, \oplus)$. The category MALL of models of linear logic is given by $*-autonomous categories and structure-preserving functors$.

**Fibrations and the Grothendieck Construction** We denote as Cat the category of small categories and functors. We now introduce the crucial notion for our semantic investigations, that is categorical fibrations.

**Definition 2.5 (Grothendieck Construction).** Given a functor $L: \mathbb{C}^{\text{op}} \to \text{Cat}$ from a category $\mathbb{C}$ to $\text{Cat}$. The Grothendieck construction for $L$ is defined by:

* a category $\int L$:

- whose objects are the pairs $\text{ob}(\int L) = (X \in \text{ob}(\mathbb{1}), A \in \text{ob}(LX))$,

- whose morphisms are pairs $(\int L)((X, A), (Y, B)) = (f \in \mathbb{1}(X, Y), \phi \in LX(A, LfB))$

* a functor $p_L: \int L \to \mathbb{1}$ defined by the first projection.

The Grothendieck opconstruction for $L$ gives an opfibration defined by:

* a category $\mathcal{L}$, called the category of elements of $L$,

- whose objects are the pairs $\text{ob}(\mathcal{L}) = (X \in \text{ob}(\mathbb{1}), A \in \text{ob}(LX))$,

- whose morphisms are pairs $(\mathcal{L})((X, A), (Y, B)) = (f \in \mathbb{1}(Y, X), \phi \in LY(LfA, B))$

* a functor $p_L: \mathcal{L} \to \mathbb{1}^{\text{op}}$ defined by the first projection.

We call *fibration* the pair category plus projection obtained from the Grothendieck construction. The category $LX \in \text{Cat}$ is called the *fiber of X*. Fibrations are generally (and equivalently) defined as a pair $(\mathbb{C}, p: \mathbb{C} \to \mathbb{1})$ where $\mathbb{1}$-morphisms have cartesian liftings in $\mathbb{C}$, but we will always construct them from a functor. In what follows, we perform Grothendieck constructions on functors $L: \mathbb{C}^{\text{op}} \to \text{StAut}$, meaning that we formally consider the postcomposition with the forgetful functor from $\text{StAut}$ to $\text{Cat}$.

**Enriched Structures** We introduce some notions of poset-enriched category theory, that we exploit in the construction of models for IndLL.

**Definition 2.6 (Poset-Enriched Category).** A Poset-enriched category is a category $\mathbb{C}$ plus, for every objects $A, B \in \text{ob}(\mathbb{C})$, a partial order on $\mathbb{C}(A, B)$ making the composition

$$ \_\_\_\_ : \mathbb{C}(A, B) \times \mathbb{C}(B, C) \to \mathbb{C}(A, C) $$

monotonic. We write $\mathbb{C}^{\text{op}}$ for the Poset-enriched category obtained by inverting the homset $\mathbb{C}^{\text{op}}(A, B) = \mathbb{C}(B, A)$ but not the order.
**Definition 2.7 (Compact Closed Poset-Enriched Category).** *A* (strict) compact closed poset enriched category is a symmetric monoidal poset-enriched category in which all objects have duals. Spelling out, it consists of the following data:

• a Poset-enriched category $\mathbb{C}$,

• an object $1 \in \mathbf{ob}(\mathbb{C})$ and a Poset-enriched functor $\mathbb{_\otimes}_\mathbb{C}: \mathbb{C} \times \mathbb{C} \to \mathbb{C}$ (i.e., a functor monotonic on morphisms) satisfying associativity, symmetry and unity diagrams,

• for each object $A \in \mathbf{ob}(\mathbb{C})$, a dual object $A^{\perp}$ and two morphisms $\mu_A \in \mathbb{C}(1, A \otimes_A A^{\perp})$ and $\epsilon_A \in \mathbb{C}(A^{\perp} \otimes_A A, 1)$, satisfying additional axioms.

## 3 From Indexed Linear Logic to Fibrations

In order to balance the incoming technical sections, we first give an informal presentation of indexed linear logic and how it does relate to the categorical notion of fibration.

An indexed formula intuitively consists of a version of a standard LL formula that is defined only in a given domain of resources, that we call its locus. In the original formulation of indexed LL, loci are sets. To say that a formula $A$ is defined under a locus $X$, we write $X \vdash A$, notice that we allow the same formula to be defined under different loci.<fnref n="1" /> Loci do not change the structure of formulae, which shall respect the standard linear logic grammar. From an indexed formula $A$, we can naturally obtain a standard linear logic formula, that we denote as $\underline{A}$, and that we are just refining. A semantic intuition behind the syntax is the following: an indexed formula $A$ corresponds to a family of elements of the relational interpretation of its underlying LL formula, indexed over a locus $X$, i.e. to a function $\llbracket A \rrbracket : X \to \llbracket \underline{A} \rrbracket_{\text{Rel}}$.

Proofs are defined by structural induction, adapting the standard rules of linear logic. The most important aspect of the deductive system is that formulae that appear in the same sequent have to be defined under the same locus: for this reason we write $A \upharpoonright_X B$, meaning that both $A$ and $B$ are defined under $X$. Again, an indexed proof $\pi$ of conclusion $A \upharpoonright_X B$ is the refinement of a standard proof $\underline{\pi}$ of conclusion $\underline{A} \vdash \underline{B}$.

Semantically, an indexed proof is a choice of correct approximations for its underlying LL proof. To make this more explicit, consider an indexed proof $\pi$ with conclusion $A \upharpoonright_X B$. We know that $\llbracket A \rrbracket : X \to \llbracket \underline{A} \rrbracket_{\text{Rel}}$ and $\llbracket B \rrbracket : X \to \llbracket \underline{B} \rrbracket_{\text{Rel}}$. The indexed proof stands for all pairs $\langle \llbracket A \rrbracket (x), \llbracket B \rrbracket (x) \rangle \in \llbracket \underline{\pi} \rrbracket_{\text{Rel}} \subseteq \llbracket A \rrbracket_{\text{Rel}} \times \llbracket B \rrbracket_{\text{Rel}}$, that are pointed by the same object $x \in X$. Hence the interpretation $\llbracket \underline{\pi} \rrbracket$ can be seen as a subset of $\llbracket \underline{\pi} \rrbracket_{\text{Rel}}$. It is the subset of executions of the programs for which the choice of indexes given by $A$ and $B$ is coherent.

The semantic construction we sketched is rooted in the relational interpretation, and it is at the foundation of the original work on indexed linear logic [3, 4]. However, if we step back for a moment and look at this system from a more abstract angle, we may be able to extract a general framework that is independent from the particular case of sets and relation: One could imagine to introduce an arbitrary category of loci $\mathcal{L}$, whose objects can be used as resource domain of a modular generalization of indexed linear logic. The main property

<footnote n="1">¹This is not the case in the original IndLL.</footnote>
that this category has to bear turns out to be *extensivity* (Definition 2.1), which
grants the proper syntactical handling of the additive structure, as we shall see
in detail in the next section.

The semantic intuition we discussed above can then be fruitfully recast in
the following categorical way. If we take a locus $X \in \mathcal{L}$, clearly we can consider
$L(X)$ as the “universe” where all the formulae $A$ s.t. $X \Vdash A$ “live”. Since in
this paper we are not considering LL exponential, $L(X)$ can be identified with a
star-autonomous category, i.e. with a model of multiplicative linear logic. In the
relational setting described above, the objects of $L(X)$ would just be functions
$X \to [A]_{\mathrm{Rel}}$, s.t. $X \Vdash A$. Morphisms $r \in [A \vdash_X B]$ of $L(X)$ should then be
relations $r \in [A \vdash B]_{\mathrm{Rel}}$ that are coherent with the interpretation of indexed
formulae in the sense we just discussed.

From a more abstract point of view, we are close enough to give to L the
structure of a *functor* between the category of loci and the category of star-
autonomous categories and monoidal functors. The only element that we are
missing are the functors $Lf$ between the categories $LX$ and $LY$ for each mor-
phism $f$ between loci. Those functors are syntactically used everywhere in the
definition of the original indexed linear logic. They do not correspond to logi-
cal operators, but to rewritings that traverse the syntax of formulae to modify
indexes. In this respect, they are similar to the negation operator $(-)^{\perp}$ of LL.

The given of such a functor $L : \mathcal{L}^{\mathrm{op}} \to \mathrm{StAut}$ is the same as that one of an appropriate categorical *fibration*. We can define its corresponding *fibration* $\int L \to \mathcal{L}$, where $\int L$ is the *category of elements of L*, whose objects are pairs $(X, A \in L(X))$ for $X \in \mathcal{L}$. This is the well-known *Grothendieck construction* (Definition 2.5) and the projection $\int L \to I$ satisfies the properties of a *fibration*.

For what concerns our point-of-view, this means that the our logic lives in
two coherent universes at the same time: that of the fibers $L(X)$ in which we
interpret formulae, and that of the whole fibration $\int L$. We will see that, while
multiplicative connectives mirror the star-autonomous structure of fibers, the
additives connectives mirror, in the fibers, the structure of (co)limits pertaining
to the (op)fibration. Section 4.1 will detail this new and intriguing way to think
about additives.

# 4 MAInd$_{\mathcal{L}}$LL

**Definition 4.1 (Index Structures).** An index structure is given by an exten-
sive category ($\emptyset$, $+$, $\emptyset$) called the category of loci and by a contravariant functor
`atom`: $\emptyset \to \mathrm{Set}$ where elements of $\bigcup_{X \in \mathrm{ob}(\emptyset)} \mathrm{atom}(X)$ are called atoms.

The definition of the category of loci can be relaxed from cartesian to semi-
cartesian coproduct, such as injections:

**Definition 4.2 (Semi-extensive category of loci).** A semi-extensive category is a monoidal category with an initial object and the extensiveness property.

The definition of indexed structure can be relaxed to accept a semi-extensive
category of loci.

This happen, in particular, when one restricts itself to monomorphic mor-
phisms between loci:
**Proposition 1.** If a category $\mathcal{I}$ is extensive, then monoollel, the sub-category of monomorphisms, is semi-extensive.

Proof. • If $f, g$ are mono, then $f + g : X + Y \to X' + Y'$ is mono thus the monoidality is preserved: for any $h, h' : Z \to X + Y$ such that $h ; (f + g) = h' ; (f + g)$, by extensivity, $h = h_{|X} + h_{|Y}$ and $h' = h'_{|X} + h'_{|Y}$ thus $h_{|X} ; f = h'_{|X} ; f$ and $h_{|Y} ; g = h'_{|Y} ; g$, which implies that $h_{|X} = h'_{|X}$ and $h_{|Y} = h'_{|Y}$ hence $f$ and $g$ are mono.

• The terminal arrows term<sub>A</sub> are monos thus the semi-caresian structure is preserved.

• Pullbacks along monos are monos, thus the extensivity is preserved.

□

**Definition 4.3 (Formulae).** Given an index structure $\mathcal{I}$, the formulae of MAInd<sub>II</sub>LL are given by the following inductive grammar:

$$
\begin{array}{l}
a \in \bigcup_{X \in \text{ob}(\mathcal{I})} \text{atom}(X) \\
A, B ::= a \mid a^{\perp} \mid \mathbf{1} \mid \bot \mid \emptyset \mid \top \mid A \otimes B \mid A \nparallel B \mid A_X \oplus_Y B \mid A_X \&_Y B
\end{array}
$$

We will sometimes drop the annotations under the additive connectives, just
writing $A \oplus B$ and $A \& B$. Formulae are defined under a locus $X \in \text{ob}(\mathcal{I})$, with
the following deductive system:

$$
\frac{
  \begin{array}{c}
    \displaystyle \frac{a \in \text{atom}(X)}{X \Vdash a} \\
    \hline
    X \Vdash \mathbf{1}
  \end{array}
  \qquad
  \begin{array}{c}
    \displaystyle \frac{a \in \text{atom}(X)}{X \Vdash a^{\perp}} \\
    \hline
    X \Vdash \bot
  \end{array}
  \qquad
  \begin{array}{c}
    \displaystyle \frac{X \Vdash A \quad X \Vdash B}{X \Vdash A \otimes B} \\
    \hline
    \frac{X \Vdash A \quad Y \Vdash B}{X + Y \Vdash A_X \oplus_Y B}
  \end{array}
}{
  \begin{array}{c}
    \displaystyle \frac{X \Vdash A \quad X \Vdash B}{X \Vdash A \nparallel B} \\
    \hline
    0 \Vdash 0
  \end{array}
}
$$

In the following, when we deal with MAInd<sub>II</sub>LL we implicitly assume that we
are given a category of loci <I>. Given an indexed formula A, we can retrieve
a formula of standard MALL just by ‘forgetting’ the indexes. We denote that
formula as A.

**Example 4.4.** The index structure of the original indexed linear logic, hereby called MAInd<sub>Set</sub>LL, is given by:

• the extensive category Set of set and function,

• a contravariant functor of atoms given by atom(X) := {f | f : X → Y, for some Y ∈ Set}, the functions of domain X, and atom(f)(a) = a ◦ f, the precomposition.

Notice that the atoms are chosen arbitrarily as they where not given in the orig-
inal paper. The only requirement is for them to be coherent with the semantics.<fnref n="2" />

Arguably, the original indexed linear logic is MAInd<sub>Inj</sub>LL which is indexed
over Inj = mono(())Set), but this is just a restriction to the “useful part” as
shown below.

<footnote n="2"><sup>2</sup>Here, we choose to allow an atom per point in the second semantics.</footnote>
**Definition 4.5 (Negation).** As usual, we can define the negation inductively on formulae:

$$ (a^{\perp})^{\perp} := a \quad 1^{\perp} := \bot \quad \top^{\perp} := \emptyset \quad (A \otimes B)^{\perp} := A^{\perp} \mathfrak{A} B^{\perp} \quad (A_X \&_Y B)^{\perp} := A^{\perp} X \oplus_Y B^{\perp} \\ \bot^{\perp} := 1 \quad \emptyset^{\perp} := \top \quad (A \mathfrak{A} B)^{\perp} := A^{\perp} \otimes B^{\perp} \quad (A_X \oplus_Y B)^{\perp} := A^{\perp} X \&_Y B^{\perp}. $$

So that

$$ X \Vdash A \Leftrightarrow X \Vdash A^{\perp}. $$

**Definition 4.6 (Morphisms Action on Formulae).** Similarly, we can define $X \Vdash f(A)$, the action of $f$ on $A$, inductively on $Y \Vdash A$ for any $f \in \mathcal{I}(X, Y)$. The action simply commutes with the multiplicative structure:

$$ \begin{array}{lclcl} f(a) & := & \mathbf{atom}(f)(a) & f(1) & := 1 \\ f(a^{\perp}) & := & f(a)^{\perp} & f(\bot) & := \bot \end{array} \qquad f(A \otimes B) := f(A) \otimes f(B) \\ \qquad \qquad \qquad \qquad f(A \mathfrak{A} B) := f(A) \mathfrak{A} f(B). $$

The additive units are trivial since $\mathrm{id}_0$ is the only $f: 0 \to 0$ by extensivity; and the additive operators use the extensive pullbacks $f|_{Y_1}$ and $f|_{Y_2}$ of $f \in \mathcal{I}(X, Y_1 + Y_2)$ along the injections.

$$ \mathrm{id}_0(\top) := \top \qquad f(A_{X_1} \&_X B) := f|_{Y_1}(A) f_{Y_1}^{f^{-1}(Y_1)} \& f_{Y_2}^{f^{-1}(Y_2)} f|_{Y_2}(B) $$

$$ \mathrm{id}_0(\emptyset) := \emptyset \qquad f(A_{X_1 \oplus X_2} B) := f|_{Y_1}(A) f_{Y_1}^{f^{-1}(Y_1) \oplus f^{-1}(Y_2)} f|_{Y_2}(B). $$

**Lemma 4.7 (Right Action).** The action on formulae is contravariant:

$$ \mathrm{id}_X(A) = A \quad \text{and} \quad f(g(A)) = (g; f)(A). $$

Sequents are defined under an explicit locus $X$ that have to be in the domain of each of its formulae. In addition, we quotient the set of sequents by usual interchange laws.

**Definition 4.8 (Sequents).** Sequents are shaped $\Gamma \vdash_X \Delta$ for $\Gamma, \Delta$ sequences of formulae $A$ such that $X \Vdash A$. They are considered up-to structural exchanges and symmetries:

$$ \Gamma_1, \Gamma_2 \vdash_X \Delta_1, A, \Delta_2 \quad \equiv \quad \Gamma_1, A^{\perp}, \Gamma_2 \vdash_X \Delta_1, \Delta_2 $$

$$ \Gamma \vdash_X \Delta \quad \equiv \quad \Gamma, 1 \vdash_X \Delta. $$

**Definition 4.9 (Proofs).** The proof system is defined inductively as follows:

$$ \frac{a \in \mathbf{atom}(X)}{a \vdash_X a} \qquad \frac{\Gamma \vdash_X A \qquad A \vdash_X \Delta}{\Gamma \vdash_X \Delta} \\ \frac{\Gamma \vdash_X A \qquad \Delta \vdash_X B}{\Gamma, \Delta \vdash_X A \otimes B} \qquad \frac{\Gamma \vdash_X A, B}{\Gamma \vdash_X A \mathfrak{A} B} \\ \frac{0 \Vdash \Gamma}{\Gamma \vdash_0 \top} \qquad \frac{\iota_1(\Gamma) \vdash_X A \qquad \iota_2(\Gamma) \vdash_Y B}{\Gamma \vdash_{X+Y} A \& B} \qquad \frac{\Gamma \vdash_X A \qquad 0 \Vdash B}{\Gamma \vdash_X A_X \oplus_0 B} \qquad \frac{\Gamma \vdash_X B \qquad 0 \Vdash A}{\Gamma \vdash_X A_0 \oplus_X B} $$

Given an indexed proof $\pi$ of $\Gamma \vdash_X A$ we can retrieve a MALL proof of conclusion $\Gamma \vdash \underline{A}$, just by ‘forgetting’ the indexes. We denote that proof as $\pi$.

**Lemma 4.10.** The identity is an admissible rule, i.e., for any formula $A$ there is a proof of

$$ \frac{X \Vdash A}{A \vdash_X A} $$
*Proof.* It the standard proof by induction on $X \vdash A$, using $(A^{\perp} \vdash_X A^{\perp}) \equiv (A \vdash_X A)$ to bypass half the cases:

• if $\frac{a \in \mathit{atom}(X)}{X \vdash a}$, we have $\frac{a \in \mathit{atom}(X)}{a \vdash_X a}$

• if $\overline{X \vdash 1}$, since $(1 \vdash_X 1) \equiv (\vdash_X 1)$, we have $\overline{1 \vdash_X 1}$

• if $\frac{X \vdash A \qquad X \vdash B}{X \vdash A \otimes B}$, we have $\frac{\frac{X \vdash B}{B \vdash_X B}}{\frac{A \vdash_X A \qquad A, B \vdash_X A \otimes B}{A \otimes B \vdash_X A \otimes B}}$

• $\frac{0 \vdash \bar{T}}{\bar{T} \vdash_0 \bar{T}}$

• if $\frac{X \vdash A \qquad Y \vdash B}{X+Y \vdash A \& B}$, recall that $\iota_1(A \& B) = A \& \mathit{init}(B)$, thus
$$
\frac{
  \begin{array}{c@{\quad}c}
    \begin{array}{c}
      X \vdash A \\
      A \vdash_X A
    \end{array}
    &
    \begin{array}{c@{\quad}c}
      Y \vdash B \\
      0 \vdash \mathit{init}(B)
    \end{array}
  \end{array}
}{
  \begin{array}{c@{\quad}c}
    A \& \mathit{init}(B) \vdash_X A &
    \mathit{init}(A) \& B \vdash_Y B \\
    A \& B \vdash_{X+Y} A \& B
  \end{array}
}
$$

In addition, the action, below, transports identity proofs into identity proofs. $\square$

**Definition 4.11 (Morphisms Action on Proofs).** For any $f \in \mathcal{I}(X, Y)$ and proof $\pi$ of $\Gamma \vdash_Y \Delta$, we inductively define the proof $f(\pi)$ of $f(\gamma) \vdash_X f(\delta)$, the action of $f$ on $\pi$.

$$f\left(\frac{a \in \mathit{atom}(Y)}{a \vdash_Y a}\right) := \frac{f(a) \in \mathit{atom}(X)}{\vdash_X f(a)}$$

$$f\left(\frac{\frac{\pi_1}{\Gamma \vdash_Y A} \qquad \frac{\pi_2}{A \vdash_Y \Delta}}{\Gamma \vdash_Y \Delta}\right) := \frac{\frac{f(\pi_1)}{f(\Gamma) \vdash_X (A)} \qquad \frac{f(\pi_2)}{f(A) \vdash_X f(\Delta)}}{f(\Gamma) \vdash_X f(\Delta)}$$

$$f\left(\frac{\bar{\Gamma}_Y 1}{\bar{\Gamma}_Y 1}\right) := \frac{\bar{\Gamma}_X 1}{\bar{\Gamma}_X 1}$$

$$f\left(\frac{\frac{\pi_1}{\Gamma \vdash_Y A} \qquad \frac{\pi_2}{\Delta \vdash_Y B}}{\Gamma, \Delta \vdash_Y A \otimes B}\right) := \frac{\frac{f(\pi_1)}{f(\Gamma) \vdash_X f(A)} \qquad \frac{f(\pi_2)}{f(\Delta) \vdash_X f(B)}}{f(\Gamma), f(\Delta) \vdash_X f(A) \otimes f(B)}$$

$$f\left(\frac{\frac{\pi}{\Gamma \vdash_Y A, B} \qquad \frac{\pi}{\Gamma \vdash_Y A \otimes B}}{\Gamma \vdash_Y A \otimes B}\right) := \frac{\frac{f(\pi)}{f(\Gamma) \vdash_X f(A), f(B)}}{\frac{f(\pi)}{f(\Gamma) \vdash_X f(A) \otimes f(B)}}$$
$$ \mathrm{id}_0 \left( \frac{0 \vDash \Gamma}{\Gamma \vdash_0 \top} \right) := \frac{0 \vDash \Gamma}{\mathrm{id}_0(\Gamma) \vdash_0 \top} $$

$$ f \left( \frac{\begin{array}{cc} \pi_1 & \pi_2 \\ \frac{\iota_1(\Gamma) \vdash_{\Gamma_1} A}{\Gamma \vdash_{\Gamma_1+\Gamma_2} A \& B} & \frac{\iota_2(\Gamma) \vdash_{\Gamma_2} B}{A \& B} \end{array}}{\Gamma \vdash_{\Gamma_1+\Gamma_2} A \& B} \right) := \frac{\begin{array}{cc} f_{|Y_1}(\pi_1) & f_{|Y_2}(\pi_2) \\ \frac{\iota_1(f(\Gamma)) \vdash_{\Gamma_1-1}(Y_1) f_{|Y_1}(A)}{f(\Gamma) \vdash_X f_{|Y_1}(A) f_{|Y_1-1}(Y_1) \& f_{|Y_2}(\Gamma_2) f_{|Y_2}(B)} & \frac{\iota_2(f(\Gamma)) \vdash_{\Gamma_2-1}(Y_2) f_{|Y_2}(B)}{f(\Gamma) \vdash_X f_{|Y_2}(A) f_{|Y_2-1}(Y_2) \& f_{|Y_1}(\Gamma_1) f_{|Y_1-1}(\Gamma_1)} \end{array}}{\Gamma \vdash_{\Gamma_1+\Gamma_2} A \& B} $$

$$ f \left( \frac{\frac{\pi}{\Gamma \vdash_Y A} \quad 0 \vDash B}{\Gamma \vdash_Y A \oplus_0 B} \right) := \frac{f(\pi)}{f(\Gamma) \vdash_X f(A) \quad 0 \vDash B} \quad \text{since } f_{|Y} = f \text{ and } f_{|0} = \mathrm{id}_0 $$

$$ f \left( \frac{\frac{\pi}{\Gamma \vdash_Y B} \quad 0 \vDash A}{\Gamma \vdash_Y A_0 \oplus_Y B} \right) := \frac{f(\pi)}{f(\Gamma) \vdash_X f(B) \quad 0 \vDash A} \frac{f(\Gamma) \vdash_X A_0 \oplus_X f(B)}{f(\Gamma) \vdash_X A_0 \oplus_X f(B)} $$

**Definition 4.12 (Cut-elimination).** MAInd<sub>ll</sub> have a cut-elimination procedure. This procedure is a decoration of LL cut-elimination.

Non-commutation rules:

$$ \frac{\begin{array}{ccc} \frac{\pi_1}{\Gamma \vdash_X A} & \frac{\pi_2}{\Delta \vdash_X B} & \frac{\pi_3}{A, B \vdash_X \Xi} \\ \hline \Gamma, \Delta \vdash_X A \otimes B & A \otimes B \vdash_X \Xi & A \otimes B \vdash_X \Xi \end{array}}{\Gamma, \Delta \vdash_X \Xi} \rightsquigarrow \frac{\pi_1}{\Gamma \vdash_X A} \frac{\pi_2}{\Delta \vdash_X B} \frac{\pi_3}{A, B \vdash_X \Xi} \quad \text{since } A \vdash_X \Xi \text{ implies } 0 \vDash \Xi $$

$$ \frac{\begin{array}{ccc} \pi_1 & \pi_2 & \pi_3 \\ \frac{\Xi \vdash_X A \quad 0 \vDash B}{\Xi \vdash_X A_\oplus_0 B} & \frac{\Delta \vdash_X \iota_1(\Gamma) \quad B \vdash_0 \iota_2(\Gamma)}{A_\oplus_0 B \vdash_X \Gamma} & \frac{\Xi \vdash_{X+0} A_\oplus_0 B}{A_\oplus_0 B \vdash_{X+0} \Gamma} \end{array}}{\Xi \vdash_{X+0} A_\oplus_0 B} \rightsquigarrow \frac{\pi_1}{\Xi \vdash_{X+0} A} \frac{\rho(\pi_2)}{\rho(A) \vdash_{X+0} \Gamma} \quad \text{since } A \vdash_{X+0} \Xi \text{ implies } 0 \vDash \Xi $$

$$ \frac{\begin{array}{ccc} \pi_1 & \pi_2 & \pi_3 \\ \frac{\Xi \vdash_{0+Y} B \quad 0 \vDash A}{\Xi \vdash_{0+Y} A_0 \oplus_Y B} & \frac{\Delta \vdash_{0+Y} \lambda_1(\Gamma) \quad B \vdash_Y \lambda_2(\Gamma)}{A_0 \oplus_Y B \vdash_{0+Y} \Gamma} & \frac{\Xi \vdash_{0+Y} A_0 \oplus_Y B}{A_0 \oplus_Y B \vdash_{0+Y} \Gamma} \end{array}}{\Xi \vdash_{0+Y} \Gamma} \rightsquigarrow \frac{\pi_1}{\Xi \vdash_{0+Y} A} \frac{\lambda(\pi_2)}{A \vdash_{0+Y} \lambda(\Gamma)} \quad \text{since } A \vdash_{0+Y} \Xi \text{ implies } 0 \vDash \Xi $$

Non-trivial commutation rules:

$$ \frac{\begin{array}{ccc} \frac{0 \vDash \Gamma, A}{0 \vdash_0 \Gamma, A} & \frac{\pi_1}{A \vdash_0 \Xi} & \frac{0 \vDash \Xi, \Gamma}{0 \vdash_0 \Xi, \Gamma} \end{array}}{0 \vdash_0 \Xi, \Gamma} \rightsquigarrow \frac{0 \vDash \Xi, \Gamma}{0 \vdash_0 \Xi, \Gamma} \quad \text{viable since } A \vdash_0 \Xi \text{ implies } 0 \vDash \Xi $$

$$ \frac{\begin{array}{ccc} \pi_1 & \pi_2 & \pi_3 \\ \frac{B \vdash_X \iota_1(\Gamma), \iota_1(A)}{B \vdash_X C \vdash_{X+Y} \Gamma, A} & \frac{C \vdash_Y \iota_2(\Gamma), \iota_2(A)}{B \vdash_X C \vdash_{X+Y} \Gamma, \Xi} & \frac{\pi_3}{A \vdash_{X+Y} \Xi} \end{array}}{B \vdash_X C \vdash_{X+Y} \Gamma, \Xi} \rightsquigarrow \frac{\begin{array}{ccc} \pi_1 & \pi_2 & \pi_3 \\ \frac{B \vdash_X \iota_1(\Gamma), \iota_1(A)}{B \vdash_X \iota_1(\Gamma), \iota_1(\Xi)} & \frac{\iota_1(\pi_3)}{\iota_1(A) \vdash_X \iota_1(\Xi)} & \frac{\pi_2}{C \vdash_X \iota_2(\Gamma), \iota_2(A)} \\ \hline C \vdash_Y \iota_2(\Gamma), \iota_2(\Xi) & C \vdash_Y \iota_2(\Gamma), \iota_2(\Xi) & \frac{\iota_2(\pi_3)}{\iota_2(A) \vdash_Y \iota_2(\Xi)} \end{array}}{B \vdash_X C \vdash_{X+Y} \Gamma, \Xi} $$
• Proofs and cut-elimination procedure, when we forget about indexes, are those of MALL.

• When restrict to proofs under the locus 0, we have a bijection between MAInd_LL and MALL proofs.

• This is a forward and backward simulation, i.e., for any proof $\pi$ of MAInd_LL, if $\pi_1 \rightsquigarrow \bar{\pi}$ (resp. $\bar{\pi} \rightsquigarrow \pi_2$) in MALL, then there is a unique $\pi'_1$ (resp. a unique $\pi'_2$) such that $\pi'_1 \rightsquigarrow \pi$ and $\bar{\pi}'_1 = \pi_1$ (resp. $\bar{\pi} \rightsquigarrow \pi'_2$ and $\bar{\pi}'_2 = \pi_2$).

## 4.1 Categorical Models

We now introduce the categorical semantics for our system. Our construction will be parametric on the choice of an appropriate category of loci, which we assume as given.

**Definition 4.13 (Model of MAInd_LL).** A model of MAInd_LL is given by

1. a functor $L : \mathbb{1}^{\mathrm{OP}} \to \mathrm{StAut}$

2. where the fibration $\int L$ is a cocartesian monoidal fibration, spelling it out:

• $\int L$ has a cocartesian structure $(\oplus, \emptyset, \mathrm{init}, \nabla)$,

• the forgetful functor $p_L : \int L \to \mathbb{1}$ is cocartesian, i.e., $p_L(\emptyset) = 0$, $p_L((X, A) \oplus (Y, B)) = X + Y$ and $p_L((f, m) \oplus (g, n)) = f + g$,

• the coproduct $\oplus$ preserves cartesian arrows, i.e., for all $f : \mathbb{1}(X, X')$, $g : \mathbb{1}(Y, Y')$ and $A : LY$,

$$ (f, \mathrm{id}_{LfA}^{LX}) \oplus (g, \mathrm{id}_{LgB}^{LY}) = (f + g, \mathrm{id}_{L(f+g)(A\oplus B)}^{L(X+Y)}) . $$

Formulae and proofs should be interpreted as objects and morphisms of the fiber of their locus. The additive structure however consists of operations defined on the whole fibration, i.e., on objects and morphisms of possibly different fibers. We will show that, for $X \Vdash A$ and $Y \Vdash B$, one can see $A \& B$ as an element of the fiber $L(X + Y)$, hence validating the expected interpretation.

**Remark 4.14.** We use the following notation for the image of additives through the Grothendieck construction:

• $(0, \emptyset : L(0)) := \emptyset,$

• for any two objects $(X, A), (Y, B) \in \int L$, we set

$$ (X + Y, A_{X \oplus Y} B : L(X + Y)) := (X, A) \oplus (Y, B) $$

and for any two fiber morphisms $m : LX_1(A_1, B_1), n : LX_2(A_2, B_2)$, we set

$$ (\mathrm{id}, m_{X_1 \oplus X_2} n : L(X_1 + X_2)(A_1_{X_1} \oplus_{X_2} A_2, B_1_{X_1} \oplus_{X_2} B_2)) := (\mathrm{id}, m)_{X_1 \oplus X_2} (\mathrm{id}, n) . $$

**Lemma 4.15.** $\bar{x} \oplus \bar{y} : L(X) \times L(Y) \to L(X + Y)$ is a functor.
Proof. (ID) Let $A \in LX, B \in LY$, we will show that $\mathrm{id}_{A \oplus Y} \mathrm{id}_{B} = \mathrm{id}_{A \oplus Y} \oplus \mathrm{id}_{B}$:
by definition, $(\mathrm{id}_{X+Y}, \mathrm{id}_{A \oplus Y} \mathrm{id}_{B} : A \oplus Y \to A \oplus Y B) := (\mathrm{id}_{X}, A) \oplus (\mathrm{id}_{Y}, B) = \mathrm{id}_{(X+Y,A \oplus Y B)} = (\mathrm{id}_{X+Y}, \mathrm{id}_{A \oplus Y B})$ (Composition) Let $m, \in L(X)(A_1, B_1), m, \in L(X)(B_1, C_1), n \in L(Y)(A_2, B_2), n' \in L(Y)(B_2, C_2)$, we will show that $(m \oplus Y n); (m' \oplus Y n') = (m; m') \oplus Y (n; n')$.

By definition

$$ 
\begin{align*}
m \oplus n &= (\mathrm{id}, m) \oplus (\mathrm{id}, n) \\
m' \oplus n' &= (\mathrm{id}, m') \oplus (\mathrm{id}, n') \\
m; m' \oplus^L n; n' &= (\mathrm{id}, m; m') \oplus (\mathrm{id}, n; n')
\end{align*}
$$

By functoriality of the coproduct $\oplus$, we can conclude. $\square$

**Lemma 4.16.** For any $f \in \mathbb{I}(X, Y + Z)$, there is the equality of functor:

$$ L(f + g)(\mathrm{id}_{Y} \oplus \mathrm{id}_{Z}) = Lf(\mathrm{id})_{f^{-1}(Y)} \oplus_{f^{-1}(Z)} Lg(\mathrm{id}) \quad (1) $$

and the following equality holds in $\int L$:

$$ (f, m) \oplus (g, n) = (f + g, m \oplus n) \quad (2) $$

Proof. First we are proving 2:

$$ 
\begin{align*}
(f, m) \oplus (g, n) &= ((\mathrm{id}, m); (f, \mathrm{id})) \oplus ((\mathrm{id}, n); (g; \mathrm{id})) \\
&= ((\mathrm{id}, m) \oplus (\mathrm{id}, n)); ((f, \mathrm{id}) \oplus (g; \mathrm{id})) \\
&= ((\mathrm{id}, m) \oplus (\mathrm{id}, n)); (f + g, \mathrm{id}) \quad \oplus \text{ preserves Cart. arrows} \\
&= (\mathrm{id}, m \oplus n); (f + g, \mathrm{id}) \quad \text{def $\oplus$} \\
&= (f + g, m \oplus n)
\end{align*}
$$

Now, remark that $(f, \mathrm{id}_{LfA}) : \int L((X_1, LfA), (Y_1, A))$ and $(g, \mathrm{id}_{LgB}) : \int L((X_2, LgB), (Y_2, B))$, thus

$$ (f, \mathrm{id}_{LfA}) \oplus (g, \mathrm{id}_{LgB}) : \int L((X_1 + X_2, LfA \oplus LgB), (Y_1 + Y_2, A \oplus B)) $$

Which means that:

$$ \mathrm{id}_{LfA} \oplus \mathrm{id}_{LgB} : L(X_1 + X_2)(LfA \oplus LgB, L(f+g)(A \oplus B)) $$

But $\oplus$ preserves cartesian arrows, thus $\mathrm{id}_{LfA} \oplus \mathrm{id}_{LgB} = \mathrm{id}_{LfA \oplus LfB}$. $\square$

**Lemma 4.17.**

$$ \iota_{i,L(f_1)(A_1),L(f_2)(A_2)}^L = L(f_i)(\iota_{i,A_1,A_2}^L) $$

Proof. We will only show that $\iota_{1,L(f)(A),L(g)(B)}^L = L(f)(\iota_{i,A,B}^L)$, the other side being symmetric.

we have that $\iota_{1,LfA,LgB}^L : LX(LfA, L\iota_1^L(LfA \oplus LgB))$ and $Lf(\iota_{1,A,B}^L) : LX(LfA, LfL\iota_1^L(A \oplus B))$.

We have to show that the targets are identical: $LfL\iota_1^L = L(\iota_1^L; f) = L((f + g); \iota_1^L) = L\iota_1^L L(f + g)$ and we get the identity by applying Lemma 4.16.
In addition, we have to prove the equality, for this we will work in $\int L$:

$$ 
\begin{align*}
(f; \iota_1^\flat, Lf(\iota_1^L)) &= (f, \mathrm{id}_{LfA}); \iota_{1,(Y,A),(Y',B)} \\
&= \iota_{1,(X,LfA),(X',LgB)}; ((f, \mathrm{id}_{LfA}) \oplus (g, \mathrm{id}_{LgB})) & \text{nat of } \iota \\
&= \iota_{1,(X,LfA),(X',LgB)}; (f + g, \mathrm{id}_{LfA \oplus LgB}) & \text{preserv. Cart. arrows} \\
&= (\iota_1^\flat; (f + g), \iota_1^L; L\iota_1^\flat(\mathrm{id})) & = (\iota_1^\flat; (f + g), \iota_1^L) \quad \Box
\end{align*}
$$

Since the operator $X \oplus Y$ is not a coproduct in the fibers, we need to prove that the co-pairing is surjective.

**Lemma 4.18** (Surjective copairing). For any $X, Y \in \mathbf{ob}(\mathcal{I})$, there is a unique natural transformation

$$ \sigma_A : L\iota_1 A \otimes_X \oplus_Y L\iota_2 A \to A $$

in $L(X + Y)$ such that $\iota_1^L$; $L\iota_1 \sigma_A = \mathrm{id}_{L\iota_1 A}^{LX}$ and $\iota_2^L$; $L\iota_1 \sigma_A = \mathrm{id}_{L\iota_2 A}^{LY}$.

*Proof.* We have $(X, L\iota_1 A), (Y, L\iota_2 A) : \mathbf{ob}(\int L)$, thus $(X, L\iota_1 A) \oplus (Y, L\iota_2 A) : \mathbf{ob}(\int L)$, and we know that $(X, L\iota_1 A) \oplus (Y, L\iota_2 A) = (X + \flat Y, L\iota_1 A \oplus L\iota_2 A)$ by definition of $X \oplus Y$.

In addition, we have $u := (\iota_1, \mathrm{id}_{\iota_1 A}^{LX}) : (X, \iota_1 A) \to (X + Y, A)$ and $v := (\iota_2, \mathrm{id}_{\iota_2 A}^{LY}) : (Y, \iota_2 A) \to (X + Y, A)$, thus there is $[u, v] : (X + \flat Y, L\iota_1 A \oplus L\iota_2 A) \to (X + Y, A)$ so that $\iota_1$; $[u, v] = u$ and $\iota_2$; $[u, v] = v$. From the last equalities, and the cartesian-ness of $p_L$, we obtain that $p_L([u, v]) = [\iota_1, \iota_2] = \mathrm{id}_{X+Y}$ and thus $[u, v] = (\mathrm{id}_{X+Y}, \sigma_A : L(X + Y)(L\iota_1 A \oplus L\iota_2 A, A))$, the unicity of $\sigma_A$ comes from that of $[u, v]$.

Using the preservation of cartesian arrows by the fibrational coproduct gives that

$$ \sigma_A = L(\iota_1^\flat + \iota_2^\flat)(\nabla_A^L) $$

which proves the naturality.

<figure><img src="image_4.png" /></figure>

The surjective copairing is nothing else than the projection of the codiagonal in the fibers. However, it is arguably more “fundamental” as we can define such a transformation even when the Loci category $\mathcal{I}$ have no co-diagonal (i.e., when it is only semi-cocartesian).

**Lemma 4.19.** For any $f : \mathcal{I}(X, Y + Z)$:

$$ \sigma_{LfA} = Lf\sigma_A $$

*Proof.* The type is correct as

$$ 
\begin{align*}
L(f)(L\iota_1 A \oplus L\iota_2 A) &= Lf|_Y L\iota_1 A \oplus Lf|_Z L\iota_2 B && \text{by lemma 4.16} \\
&= L\iota_1 Lf A \oplus L\iota_2 Lf B
\end{align*}
$$

The naturality is immediate and we have the equation

$$ 
\begin{align*}
\iota_1^L; L\iota_1 Lf \sigma_A &= \iota_1^L; Lf|_Y L\iota_1 \sigma_A \\
&= Lf(\iota_1^L; L\iota_1 \sigma_A) \\
&= Lfid \\
&= \mathrm{id}
\end{align*}
$$

which, together with its symmetric version and the unicity of $\sigma$, proves the statement.

<figure><img src="image_5.png" /></figure>
In the case of a semi-extensive category of loci, it is possible to generalize the notion of model by requiring as axioms the lemmas 4.18 and 4.19.

**Definition 4.20 (Relaxation to semi-extensivity).**

A model of $\mathbf{MAInd}_{\otimes}LL$ for a semi-extensive category of loci $\otimes$ is given by

1. a functor $L : \mathbb{1}^{\mathrm{OP}} \to \mathrm{StAut}$

2. where the Grothendieck fibration $\int L$ is a semi-cocartesian monoidal fibration, spelling out:

• $\int L$ has semi-cocartesian coproducts $(\oplus, \emptyset, \mathrm{init})$,

• the forgetful functor $p_L : \int L \to \mathbb{1}$ is monoidal, i.e., $p_L(\emptyset) = 0$, $p_L((X, A) \oplus (Y, B)) = X + Y$ and $p_L((f, m) \oplus (g, n)) = f + g$,

• the coproduct $\oplus$ preserves cartesian arrows, i.e., for all $f : \mathbb{1}(X, X')$, $g : \mathbb{1}(Y, Y')$ and $A : LY$,

$$ (f, \mathrm{id}_{LfA}^{LX}) \oplus (g, \mathrm{id}_{LgB}^{LY}) = (f + g, \mathrm{id}_{L(f+g)(A \oplus B)}^{L(X+Y)}) . $$

3. the co-pairing is surjective: For any $X, Y \in \mathrm{ob}(\mathbb{1})$, there is a natural transformation

$$ \sigma_A : L(X + Y)(L_{t_1}A \oplus L_{t_2}A, A) $$

such that $\iota_1^L; L_{t_1}\sigma_A = \mathrm{id}_{L_{t_1}A}^{LX}$, $\iota_2^L; L_{t_1}\sigma_A = \mathrm{id}_{L_{t_2}A}^{LY}$ and for any $f, Lf\sigma_A = \sigma_{LfA}$.

4. As for the previous version, we require atoms to be interpreted by targets of $L$:

$$ \forall a \in \mathrm{atom}(X), \forall f \in \mathbb{1}(X, Y), \quad [[a]] \in \mathrm{ob}(L(X)), \quad [[f(a)]] = L(f)([[a]]) $$

**Lemma 4.21.** If $\mathbb{1}$ is extensive, then the two definitions of models are equivalent with $\nabla_A^L = \sigma_L \nabla_A^1(A)$.

**Proposition 3 (Refinement of a model).** The restriction $L|_{\mathrm{mono}(\mathbb{1})}$ of a model $L : \mathbb{1} \to \mathrm{StAut}$ to mono $(\mathbb{1})$ is a model of the calculus indexed over the semi-extensive category of loci mono $(\mathbb{1})$.

**Models of $\mathbf{MAIndLL}$ vs models of $\mathbf{MALL}$** We now show that any indexed model “contains” a model of $\mathbf{MALL}$ inside the fiber of 0, which corresponds to erase all index-annotations in the logic.

**Proposition 4.** Let $\mathbb{1}$ be a category of loci and $L : \mathbb{1}^{\mathrm{OP}} \to \mathrm{StAut}$ a model of $\mathbf{MAInd}_{\otimes}LL$. Then $L0$ is a model of $\mathbf{MALL}$.

*Proof.* The category $L0 \in \mathrm{ob}(\mathrm{StAut})$ is star autonomous by definition. The coproduct is defined by:

• restricted to $L0$, the sum $\sum_{0 \oplus 0} : L0 \times L0 \to L(0 + 0) = L0$ is a monoidal product on $L0$ which unit is $\emptyset^L : L0$,

• $\mathrm{init}^\otimes$ is defined over $L0$ and $\nabla^\otimes$ over $L(0 + 0) = L0$, and they respect the required coproduct diagrams (same for the injections).
A star-autonomous with coproducts also has products by duality, which con-
clude our proof.
□

This inclusion is even an equivalence when restricted to models of $\mathbf{MAInd}_{\mathbf{1}}\mathbf{LL}$,
which is expected as $\mathbf{MAInd}_{\mathbf{1}}\mathbf{LL}$ is exactly $\mathbf{MALL}$ as a logic.

**Proposition 5.** *Models of MALL correspond exactly to models of MAInd₁LL, where 1 is the terminal category.*

Proof. If $\mathbb{C}$ is a model of MALL, then the constant functor ($\ast \mapsto \mathbb{C}$) : $\mathbb{1}^{\mathrm{Cat}} \to \mathrm{StAut}$ is a model of $\mathbf{MAInd}_{\mathbb{1}}\mathbf{LL}$.
$\square$

**Products** We now prove that the structure consisting of $\top^L := (\emptyset^L)^\perp$
and $\_\&\_ := (\perp^\perp \oplus \_\perp)$ determines a cartesian product on the opfibration of
$L$. We recall that the opfibration of a functor $L : \mathbb{1}^{\mathrm{op}} \to \mathrm{StAut}$ is given by the
category $\lambda L$ with the same objects as $\int L$, but, as morphisms from $(X, A)$ to
$(Y, B)$ above $f : B \to A$, the morphisms of $LY(FfA, B)$, and as projection the
contravariant projection $q_L$ (see Definition 2.5). This remark will ease the tech-
nical developments of the following sections. First, we show that the opfibration
behaves well wrt orthogonality.

**Proposition 6.** For $L : \mathbb{1}^{\mathrm{op}} \to \mathrm{StAut}$ we have that $(\int L)^{\mathrm{op}} = \lambda(-)^{\mathrm{op}} \circ L$.

Using this equality and the negation $-\perp$ on the fibers, we obtain the following
contravariant isomorphism of categories:

**Lemma 4.22.** For any $L : \mathbb{1}^{\mathrm{op}} \to \mathrm{StAut}$, $(\int L)^{\mathrm{op}} \stackrel{\perp}{\cong} \lambda L$.

The former isomorphism leads to a possible rephrasing of the second require-
ment of Definition 4.13.

**Lemma 4.23.** Given $L : \mathbb{1}^{\mathrm{op}} \to \mathrm{StAut}$, the following are equivalent:

• $(\int L, p_L)$ is a cocartesian monoidal fibration,

• $(\lambda L, q_L)$ is a cartesian monoidal fibration.

**Lemma 4.24.** Let $(\emptyset, 0, +)$ be a category of loci with cartesian products, and $L : \mathbb{1}^{\mathrm{op}} \to \mathrm{StAut}$ a model of MALL indexed over $\emptyset$.

Then $(\int L, \lambda L)$ is a dialogue chirality with $L0$ as continuation category [17].

*Proof.* The monoidal product is defined in $\int L$ and $\lambda L$ using [22, p. 12.7] by:

• $(X, A) \otimes \int^L (Y, B) := (X \times Y, L\pi_1 A \otimes L^{(X \times Y)} L\pi_2 B)$ and $\mathbb{1} \int^L := (1, \mathbb{1}^{L1})$,

• $(X, A) \otimes \lambda^L (Y, B) := (X \times Y, L\pi_1 A \mathcal{Y}^{L(X \times Y)} L\pi_2 B)$, and $\mathbb{1} \lambda^L := (1, \perp^{L1})$.

The monoidal equivalence of category $(-)^*, (-) : \int L \simeq (\lambda L)^{\mathrm{op}}$ is defined using
$(-)^\perp$:

• $(X, A)^* = (X, A^\perp)$ and $(f, \phi)^* = (f, \phi^\perp)$

• $(X, A) = (X, A^\perp)$ and $(f, \phi) = (f, \phi^\perp)$

The adjunction $(\lambda \dashv \rho)$ is defined by:
• $\lambda(X, A) = (0, LinitA)$ and $\lambda(f, \phi) = (\mathrm{id}_0, Linit\phi)$

• $\rho(X, A) = (0, LinitA)$ and $\rho(f, \phi) = (\mathrm{id}_0, Linit\phi)$

• $\eta_A = (\mathrm{init}, \mathrm{id}_{LinitA})$ and $\epsilon_A = (\mathrm{init}, \mathrm{id}_{LinitA})$

□

As a dialog category with products in one side and coproducts in the other, this chirality constitute a model of tensorial logic with products and coproduct (or, equivalently, a polarized MALL with a non-involutive negation).

## 4.2 Interpretation

In this section we define the interpretation of indexed formulae and proofs. Let $\mathbb{I}$ be an indexed structure, and $L: \mathbb{I} \to \mathrm{StAut}$ a model of $\mathrm{MAInd}_{\mathbb{I}}\mathrm{LL}$.

**Definition 4.25 (Interpretation of Formulae).** Formulae under a locus $X$ are interpreted by objects of $L(X)$:

• We assume that the interpretation of atoms $[[a]]_X$ lives in the fibers:

$$ \forall a \in \mathrm{atom}(X), \forall f \in \mathbb{I}(X, Y), \quad [[a]]_X \in \mathrm{ob}(L(X)), \quad [[f(a)]]_X = L(f)([[a]]_X). $$

• The negation is interpreted by the duality of the target:

$$ [[A^{\perp}]]_X := [[A]]_{\bar{X}}^{\perp}. $$

• The multiplicatives are interpreted as usual:

$$ [[A \otimes B]]_X := [[A]]_X \otimes^{L(X)} [[B]]_X \qquad [[1]]_X := 1^{L(X)}. $$

• The additives are the projection of the fibrational coproduct:

$$ [[A_X \oplus_Y B]]_{X+Y} := [[A]]_X \oplus_Y [[B]]_Y \qquad [[0]]_0 := 0^L. $$

For readability, we often omits the locus $X$ of the interpretation of formulae.

**Lemma 4.26 (Interpretation of Actions).**

$$ \textit{For any } f \in \mathbb{I}(X, Y) \textit{ and } Y \models A, \quad [[f(A)]]_X = Lf[[A]]_Y. $$

*Proof.* The cases of the product and coproduct exploits lemma 4.16 :

$$ \begin{align*} [[f(A \oplus B)]] &= [[f|_X(A) \oplus f|_Y(B)]] \\ &= [[f|_X(A)]] \oplus [[f|_Y(B)]] \\ &= L(f|_X)[[A]] \oplus L(f|_Y)[[B]] \\ &= L(f|_X + f|_Y)([[A]] \oplus [[B]]) \qquad \text{lemma 4.16} \\ &= Lf([A] \oplus [B]) \end{align*} $$

$$ [[f(1)]] = [[\mathrm{id}_0(1)]] = \mathrm{Lid}_0[[1]] \text{ because } \mathrm{id}_0 \text{ is the only morphism targeting } 0. \quad \square $$

**Definition 4.27 (Interpretation of Sequents).**

A sequent over the locus $X$ is interpreted as the corresponding homset of $LX$:

$$ [[A_1, \dots, A_n \vdash_X B_1, \dots, B_k]] := LX(\otimes[[A_i]], \mathcal{N}[[B_i]]) $$
**Lemma 4.28.** The equivalence relations on sequences are interpreted by natural bijections of homsets:

$$ [[\Gamma_1, \Gamma_2]_{\Gamma_X} \Delta_1, A, \Delta_2] \simeq [[\Gamma_1, A^{\perp}, \Gamma_2]_{\Gamma_X} \Delta_1, \Delta_2]] \quad [[\Gamma]_{\Gamma_X} \Delta] \simeq [[\Gamma, 1]_{\Gamma_X} \Delta] $$

**Definition 4.29** (Interpretation of Proofs).

Proofs $\pi$ of a sequent $\Gamma \vdash_X \Delta$ interpreted as morphisms $[[\pi]] \in [[\Gamma]_{\Gamma_X} \Delta]$.

$$ \begin{array}{lclcl} \left[ \frac{a \in \mathbf{atom}(X)}{a \vdash_X a} \right] & := & \mathrm{id}_{[[a]]_X}^{L(X)} & : & \mathrm{LX}([[a]]_X, [[a]]_X) \\ \left[ \frac{\begin{array}{cc} \pi_1 & \pi_2 \\ \Gamma \vdash_X A & A \vdash_X \Delta \end{array}}{\Gamma \vdash_X \Delta} \right] & := & [[\pi_1]]_X; [[\pi_2]]_X & : & \mathrm{LX}([[\Gamma]]_X, [[\Delta]]_X) \\ \left[ \frac{\begin{array}{cc} \pi_1 & \pi_2 \\ \Gamma \vdash_X A & \Delta \vdash_X B \end{array}}{\Gamma, \Delta \vdash_X A \otimes B} \right] & := & [[\pi_1]]_X \otimes [[\pi_2]]_X & : & \mathrm{LX}([[\Gamma]]_X \otimes [[\Delta]]_X, [[A]]_X \otimes [[B]]_X) \\ \left[ \frac{\begin{array}{cc} \pi \\ \Gamma \vdash_X A, B \\ \Gamma \vdash_X A \not\to B \end{array}}{\begin{array}{c} 0 \vdash \Gamma \\ 0 \vdash_0 \Gamma \end{array}} \right] & := & [[\pi]]_X & : & \mathrm{LX}([[\Gamma]]_X, ([[A]]_X^{\perp} \otimes [[B]]_X^{\perp})^{\perp})) \\ \left[ \frac{0 \vdash \Gamma}{0 \vdash_0 \Gamma} \right] & := & \mathrm{init}_{[[\Gamma]]}^{L} & : & \mathrm{L0}(0^L, [[\Gamma]]) \\ \left[ \frac{\begin{array}{cc} \pi_1 \\ A \vdash_X \iota_1(\Gamma) \\ A \vdash_{X \oplus Y} B \vdash_{X+Y} \Gamma \end{array}}{B \vdash_Y \iota_2(\Gamma)} \right] & := & ([[\pi_1]]_X \oplus_Y [[\pi_2]]); \sigma & : & \mathrm{L}(X + Y)(([A]_X \oplus_Y [B]), [[\Gamma]]) \\ \left[ \frac{\begin{array}{cc} \pi \\ \Gamma \vdash_X A & 0 \vdash B \\ \Gamma \vdash_X A_X \oplus_0 B \end{array}}{\Gamma \vdash_X A_X \oplus_0 B} \right] & := & [[\pi]]; \iota_2, [[B]] & : & \mathrm{LX}([[\Gamma]], [[A]]_X \oplus_0 [[B]]) \\ \left[ \frac{\begin{array}{cc} \pi \\ \Gamma \vdash_X B & 0 \vdash A \\ \Gamma \vdash_X A_0 \oplus_X B \end{array}}{\Gamma \vdash_X A_0 \oplus_X B} \right] & := & [[\pi]]_X; \iota_2, [[B]] & : & \mathrm{LX}([[\Gamma]]_X, [[A]]_{0,0} \oplus_X [[B]]_X) \end{array} $$

Notice that the second one use the surjectiveness $\sigma$ of the co-pairing from lemma 4.18.

**Theorem 4.30** (Soundness wrt Morphisms Action).

For any $f: X \to Y$ and any proof $\pi$ of $\Gamma \vdash_Y \Delta$, $[[f(\pi)]] = Lf[[\pi]]$.
Proof. Easy cases:

$$ \left[ \frac{f(a) \in \text{atom}(X)}{\vdash_X f(a)} \right] = \text{id}_{[f(a)]_X}^{LX} $$

$$ = \text{id}_{Lf([a]_X)}^{LX} $$

$$ = Lf(\text{id}_{[a]_Y}^{LY}) $$

$$ = Lf \left( \left[ \frac{a \in \text{atom}(Y)}{\vdash_Y a} \right] \right) $$

$$ \left[ \frac{f(\pi_1)}{f(\Gamma) \vdash_X A} \quad \frac{f(\pi_2)}{f(A) \vdash_X f(\Delta)} \middle/ f(\Gamma) \vdash_X f(\Delta) \right] $$

$$ = [f(\pi_1)]_X; [f(\pi_2)]_X $$

$$ = Lf[\pi_1]_Y; Lf[\pi_2]_Y $$

$$ = Lf([\pi_1]_Y; [\pi_2]_Y) $$

$$ = Lf \left( \left[ \frac{\pi_1}{\Gamma \vdash_Y A} \quad \frac{\pi_2}{A \vdash_Y \Delta} \middle/ \Gamma \vdash_Y \Delta \right] \right) $$

$$ \left[ \frac{\vdash_X 1}{} \right] = \text{id}_{1}^{LX} $$

$$ = \text{id}_{Lf1}^{LX} $$

$$ = Lf(\text{id}_{1}^{LY}) $$

$$ = Lf \left( \left[ \frac{}{\vdash_X 1} \right] \right) $$

$$ \left[ \frac{f(\pi_1)}{f(\Gamma) \vdash_X f(A)} \quad \frac{f(\pi_2)}{f(\Delta) \vdash_X f(B)} \middle/ f(\Gamma), f(\Delta) \vdash_X f(A) \otimes f(B) \right] $$

$$ = [f(\pi_1)] \otimes [f(\pi_2)] $$

$$ = Lf[\pi_1] \otimes Lf[\pi_2] $$

$$ = Lf([\pi_1] \otimes [\pi_2]) $$

$$ = Lf \left( \left[ \frac{\pi_1}{\Gamma \vdash_Y A} \quad \frac{\pi_2}{\Delta \vdash_Y B} \middle/ \Gamma, \Delta \vdash_Y A \otimes B \right] \right) $$

$$ \left[ \frac{f(\pi)}{f(\Gamma) \vdash_X f(A), f(B)} \middle/ f(\Gamma) \vdash_X f(A) \not\vdash f(B) \right] $$

$$ = [f(\pi)] $$

$$ = Lf[\pi] $$

$$ = Lf \left( \left[ \frac{\pi}{\Gamma \vdash_Y A, B} \middle/ \Gamma \vdash_Y A \not\vdash B \right] \right) $$

$$ \left[ \frac{0 \vdash \Gamma}{0 \vdash_0 \text{id}_0(\Gamma)} \right] = \text{init}_{[\Gamma]}^{L} $$

$$ = \text{Lid}_0(\text{init}_{[\Gamma]}^{L}) $$

$$ = \text{Lid}_0 \left( \left[ \frac{0 \vdash \Gamma}{0 \vdash_0 \Gamma} \right] \right) $$
Difficult cases:

$$
\[
\left[
  \begin{array}{c@{\quad}c}
    \frac{
      \begin{array}{c}
        f_{|Y}(\pi_1) \\
        \big|_{f|Y(A) \vdash_{f^{-1}(X)} \iota_1(f(\Gamma))}
      \end{array}
    }{
      f_{|Y}(A) \oplus f_{|Z}(B) \vdash_X f(\Gamma)
    }
    &
    \frac{
      \begin{array}{c}
        f_{|Z}(\pi_2) \\
        \big|_{f|Z(B) \vdash_{f^{-1}(Y)} \iota_2(f(\Gamma))}
      \end{array}
    }{
      f_{|Z}(A) \oplus f_{|Z}(B) \vdash_X f(\Gamma)
    }
  \end{array}
\right]
$$
$$
\begin{align*}
&= (\llbracket f_{|Y}(\pi_1) \rrbracket_{f^{-1}(X)} \oplus \llbracket f_{|Z}(\pi_2) \rrbracket_{f^{-1}(Z)}); \sigma_{\llbracket f(\Gamma) \rrbracket} \\
&= (L(f_{|Y})(\pi_1) \big|_X \oplus L(f_{|Z})(\pi_2) \big|_Y); \sigma_{Lf[\Gamma]} \\
&= Lf(\llbracket \pi_1 \rrbracket_X \oplus \llbracket \pi_2 \rrbracket_Y); \sigma_{Lf[\Gamma]} \tag*{by lemma 4.16} \\
&= Lf(\llbracket \pi_1 \rrbracket_X \oplus \llbracket \pi_2 \rrbracket_Y); Lf\sigma_{\llbracket \Gamma \rrbracket} \tag*{by lemma 4.19} \\
&= Lf((\llbracket \pi_1 \rrbracket_X \oplus \llbracket \pi_2 \rrbracket_Y); \sigma_{\llbracket \Gamma \rrbracket}) \\
&= Lf\left( \left[ \begin{array}{c@{\quad}c}
    \frac{\pi_1}{A \vdash_X \iota_1(\Gamma)} & \frac{\pi_2}{B \vdash_Y \iota_2(\Gamma)} \\
    \hline
    A \oplus B \vdash_{Y+Z} \Gamma
  \end{array} \right] \right)
\end{align*}
$$
$$
\[
\left[
  \begin{array}{c@{\quad}c}
    \frac{
      \begin{array}{c}
        f(\pi) \\
        \big|_{f(\Gamma) \vdash_X f(A)}
      \end{array}
    }{
      f(\Gamma) \vdash_X f(A) \oplus B
    }
    &
    \begin{array}{c}
      0 \nvDash B \\
      \big|_{f(\Gamma) \vdash_X f(A) \oplus B}
    \end{array}
  \end{array}
\right]
$$
$$
\begin{align*}
&= \llbracket f(\pi) \rrbracket; \iota_{1, \llbracket f(A) \rrbracket, \llbracket B \rrbracket}^L \\
&= Lf[\pi]; \iota_{1, Lf[\llbracket A \rrbracket, \llbracket B \rrbracket]}^L \\
&= Lf[\pi]; \iota_{1, L(f_{|X})(\llbracket A \rrbracket, L(f_{|0})(\llbracket B \rrbracket)}^L \\
&= Lf[\pi]; Lf(\iota_{1, \llbracket A \rrbracket, \llbracket B \rrbracket}^L) \tag*{by lemma 4.17} \\
&= Lf[\pi]; \iota_{1, \llbracket A \rrbracket, \llbracket B \rrbracket}^L \\
&= Lf\left( \left[ \begin{array}{c@{\quad}c}
    \frac{\pi}{\Gamma \vdash_Y A} & 0 \nvDash B \\
    \hline
    \Gamma \vdash_X A_0 \oplus B
  \end{array} \right] \right)
\end{align*}
\]
$$

□

**Theorem 4.31** (Soundness wrt Cut-Elimination).

For any $\pi_1 \rightsquigarrow \pi_2$, $\llbracket \pi_1 \rrbracket = \llbracket \pi_2 \rrbracket$.

*Proof.* Non-commutation rules:
$$ \left[ \frac{\begin{array}{ccc} \pi_1 & \pi_2 & \pi_3 \\ \hline \Gamma \vdash_X A & \Delta \vdash_X B & A, B \vdash_X \Xi \\ \hline \Gamma, \Delta \vdash_X A \otimes B & A \otimes B \vdash_X \Xi \end{array} \right] = (\llbracket \pi_1 \rrbracket \otimes \llbracket \pi_2 \rrbracket); \llbracket \pi_3 \rrbracket $$

$$ = (\llbracket \pi_1 \rrbracket \otimes \mathrm{id}_{\Delta} \llbracket X \rrbracket); ((\mathrm{id}_{A} \llbracket X \rrbracket \otimes \pi_2)); \llbracket \pi_3 \rrbracket) $$

$$ = \left[ \frac{\begin{array}{cc} \pi_1 & \pi_2 \\ \hline \Gamma \vdash_X A & A, \Delta \vdash_X \Xi \end{array}}{\Gamma, \Delta \vdash_X \Xi} \frac{\begin{array}{cc} \Delta \vdash_X B & \pi_3 \\ \hline A, \Delta \vdash_X \Xi & \end{array}}{\Gamma, \Delta \vdash_X \Xi} \right] $$

$$ \left[ \frac{\begin{array}{ccc} \pi_1 & 0 \nvDash B & \pi_2 \\ \hline \Xi \vdash_{X+0} A & A_X \oplus_0 B & \pi_3 \\ \hline \Xi \vdash_{X+0} A_X \oplus_0 B & A_X \oplus_0 B \vdash_{X+0} \Gamma & \end{array}}{\Gamma \vdash_{X+0} \Gamma} \right] = \llbracket \pi_1 \rrbracket; \iota_2, \llbracket B \rrbracket; (\llbracket \pi_2 \rrbracket \times \oplus_0 \llbracket \pi_3 \rrbracket); \sigma $$

$$ = \llbracket \pi_1 \rrbracket; L \rho \llbracket \pi_2 \rrbracket; \iota_2, \llbracket B \rrbracket; \sigma \qquad \text{(up to iso)} $$

$$ = \llbracket \pi_1 \rrbracket; L \rho \llbracket \pi_2 \rrbracket \qquad \text{lemma 4.18} $$

$$ = \left[ \frac{\begin{array}{cc} \pi_1 & \rho(\pi_2) \\ \hline \Xi \vdash_{X+0} A & \rho(A) \vdash_{X+0} \Gamma \end{array}}{\Xi \vdash_{X+0} \Gamma} \right] $$

Plus the symmetric (same proof).

Non-trivial commutation rules:

$$ \left[ \frac{\begin{array}{cc} 0 \nvDash \Gamma, A & \pi \\ \hline 0 \vdash_0 \Gamma, A & A \vdash_0 \Xi \end{array}}{0 \vdash_0 \Xi, \Gamma} \right] = \mathrm{init}_{\llbracket \Gamma \rrbracket_0} \mathfrak{g}_{\llbracket A \rrbracket_0}; (\mathrm{id}_{\llbracket \Gamma \rrbracket_0} \mathfrak{g} \llbracket \pi \rrbracket) $$

$$ = \mathrm{init}_{\llbracket \Gamma \rrbracket_0} \mathfrak{g}_{\llbracket \Xi \rrbracket_0} \qquad \text{nat. of init} $$

$$ = \left[ \frac{0 \nvDash \Gamma, \Xi}{\top \vdash_0 \Gamma, \Xi} \right] $$

$$ \begin{align*} (\llbracket \pi_1 \rrbracket \oplus \llbracket \pi_2 \rrbracket); \sigma; (\mathrm{id}_{\llbracket \Gamma \rrbracket_{X+Y}} \mathfrak{g} \llbracket \pi_3 \rrbracket) &= (\llbracket \pi_1 \rrbracket \oplus \llbracket \pi_2 \rrbracket); (L_{l_1}(\mathrm{id}_{\llbracket \Gamma \rrbracket_{X+Y}} \mathfrak{g} \llbracket \pi_3 \rrbracket)) \oplus L_{l_2}(\mathrm{id}_{\llbracket \Gamma \rrbracket_{X+Y}} \mathfrak{g} \llbracket \pi_3 \rrbracket}); \sigma \quad \text{nat. of } \sigma \\ &= (\llbracket \pi_1 \rrbracket \oplus \llbracket \pi_2 \rrbracket); ((L_{l_1} \mathrm{id}_{\llbracket \Gamma \rrbracket_{X+Y}} \mathfrak{g} L_{l_1} \llbracket \pi_3 \rrbracket)) \oplus (L_{l_2} \mathrm{id}_{\llbracket \Gamma \rrbracket_{X+Y}} \mathfrak{g} L_{l_2} \llbracket \pi_3 \rrbracket)); \sigma \quad L_{l_i} \in \mathrm{StAut}(\_, \_) \\ &= (\llbracket \pi_1 \rrbracket \oplus \llbracket \pi_2 \rrbracket); ((\mathrm{id}_{L_{l_1} \llbracket \Gamma \rrbracket_{X+Y}} \mathfrak{g} L_{l_1} \llbracket \pi_3 \rrbracket)) \oplus (\mathrm{id}_{L_{l_2} \llbracket \Gamma \rrbracket_{X+Y}} \mathfrak{g} L_{l_2} \llbracket \pi_3 \rrbracket)); \sigma \\ &= ((\llbracket \pi_1 \rrbracket; (\mathrm{id}_{L_{l_1} \llbracket \Gamma \rrbracket_{X+Y}} \mathfrak{g} L_{l_1} \llbracket \pi_3 \rrbracket)) \oplus (\llbracket \pi_2 \rrbracket; (\mathrm{id}_{L_{l_2} \llbracket \Gamma \rrbracket_{X+Y}} \mathfrak{g} L_{l_2} \llbracket \pi_3 \rrbracket))); \sigma \tag*{\square} \end{align*} $$

# 5 Syntactical model

Let $\llbracket \cdot \cdot \rrbracket$ a loci category, i.e., a semi extensive category.

We call syntactical model, the model:

* whose $*$-autonomous fibers $LX$ are defined by:

- $\mathrm{ob}(LX)$ are the formulae $A$ such that $X \nvDash A$,

- $LX(A, B)$ are the proof of the sequents $A_1, \dots, A_n \vdash_X B_1, \dots, B_k$ where $A = A_1 \otimes \dots \otimes A_n$ and $B = B_1 \mathfrak{g} \dots \mathfrak{g} B_k$ and with the quotients over the smallest relation containing:

* the cut-elimination $\rightsquigarrow$,
* the application<fnref n="4" /> of the right introduction of ℘ (or equivalently the left introduction of ⊗).

- the identities are given by the proofs of $A \vdash A$ of Lemma 4.10,

- the composition is the cut rule.

- the *-autonomous structure is standard.

• whose functors $Lf : LY \to LX$ between fibers are defined by the morphisms action: $LfA = f(A)$ and $Lf\pi = f(\pi)$.

• whose semi-coartesian fibration is defined by:

- initial element: $0 := (0^1, 0)$

- coproduct of objects: $(X, A) \oplus (Y, B) := (X + Y, A \oplus B)$

- coproduct of morphisms:

$$ \left( f, \frac{\pi_1}{A \vdash_W f(C)} \right) \oplus \left( g, \frac{\pi_2}{B \vdash_X g(D)} \right) \\ := \left( f + g, \frac{\pi_1}{A \oplus B \vdash_{W+X} (f+g)(C \oplus D)} \quad \frac{\pi_2}{B \vdash_X g(D)} \right) $$

which is correct since

$$ (f+g)(C \oplus D) = (f+g)|_Y(C) \oplus (f+g)|_Z(D) = f(C) \oplus g(D), $$

- preservation of cartesian arrows:

$$ \left( f, \frac{\mathrm{id}}{f(A) \vdash_W f(A)} \right) \oplus \left( g, \frac{\mathrm{id}}{g(B) \vdash_X g(B)} \right) \\ = \left( f + g, \frac{\mathrm{id}}{\frac{f(A) \vdash_W f(A)}{A \oplus B \vdash_{W+X} (f+g)(A \oplus B)}} \quad \frac{\mathrm{id}}{\frac{g(B) \vdash_X g(B)}{A \oplus B \vdash_{W+X} (f+g)(A \oplus B)}} \right) $$

which second member is the definition of the identity proof over $f(A) \oplus g(B) = (f+g)(A \oplus B)$ according to the proof of Lemma 4.10.

- functoriality of the coproduct:

* identity:

$$ \left( \mathrm{id}_W, \frac{\mathrm{id}}{A \vdash_W A} \right) \oplus \left( \mathrm{id}_X, \frac{\mathrm{id}}{B \vdash_X B} \right) \\ = \left( \mathrm{id}_{W+X}, \frac{\mathrm{id}}{\frac{A \vdash_W A}{A \oplus B \vdash_{W+X} A \oplus B}} \quad \frac{\mathrm{id}}{B \vdash_X B} \right) $$

which second member is the definition of the identity proof over $A \oplus B$ according to the proof of Lemma 4.10.

* composition: it uses one step of cut elimination

$$ \left( f + g, \frac{\pi_1}{A \vdash_W f(C)} \quad \frac{\pi_2}{B \vdash_X g(D)} \right); \left( f' + g', \frac{\pi'_1}{C \vdash_Y f'(D)} \quad \frac{\pi'_2}{D \vdash_Z g'(F)} \right); \\ = \left( ((f; f') + (g; g')), \frac{\pi_1}{A \vdash_W f(C)} \quad \frac{\pi_2}{B \vdash_X g(D)} \quad \frac{f(\pi'_1)}{f(C) \vdash_W f(f'(D))} \quad \frac{g(\pi'_2)}{g(D) \vdash_X g(g'(F))} \\ \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \frac{f(C) \oplus g(D) \vdash_{W+X} f(f'(E)) \oplus g(g'(F))}{A \oplus B \vdash_{W+X} f(f'(E)) \oplus g(g'(F))} \right) $$

<footnote n="4">⁴This additional quotient is standard and correspond to the restriction to monoidal categories rather than multicategories that are less “standard”.</footnote>
$$ - \sigma = \frac{\frac{\text{id}}{\iota_1(A) \vdash_X \iota_1(A)} \quad \frac{\text{id}}{\iota_2(A) \vdash_Y \iota_2(A)}}{\iota_1(A) \oplus \iota_2(A) \vdash_{X+Y} A} \text{ is natural} $$

– it is surjective:

$$ \begin{array}{ccc} \frac{\text{id}}{\iota_1(A) \vdash_X \iota_1(A)} & 0 \nvDash \text{init}(A) & \frac{\text{id}}{\iota_1(A) \vdash_X \iota_1(A)} \\ \frac{\text{id}}{\iota_1(A) \vdash_X \iota_1(A) \oplus \text{init}(A)} & \frac{\text{id}}{\iota_1(A) \oplus \text{init}(A) \vdash_X \iota_1(A)} & \frac{\text{id}}{\iota_1(A) \vdash_X \iota_1(A)} \\ \frac{\text{id}}{\iota_1(A) \vdash_X \iota_1(A)} & \frac{\text{id}}{\iota_1(A) \vdash_X \iota_1(A)} & \frac{\text{id}}{\iota_1(A) \vdash_X \iota_1(A)} \\ \frac{\text{id}}{\iota_1(A) \vdash_X \iota_1(A)} & \frac{\text{id}}{\iota_1(A) \vdash_X \iota_1(A)} & \frac{\text{id}}{\iota_1(A) \vdash_X \iota_1(A)} \\ \frac{\text{id}}{\iota_1(A) \vdash_X \iota_1(A)} & \frac{\text{id}}{\iota_1(A) \vdash_X \iota_1(A)} & \frac{\text{id}}{\iota_1(A) \vdash_X \iota_1(A)} \end{array} $$

– it is preserved by fibrational functors:

$$ \begin{align*} L f \sigma_A &= \frac{\frac{f|_W(\text{id})}{f|_W(\iota_1(A)) \vdash_W f|_W(\iota_1(A))}}{\frac{f|_Z(\iota_2(A)) \vdash_Z f|_Z(\iota_2(A))}{f|_X(\iota_1(A)) \oplus f|_Y(\iota_2(A)) \vdash_{W+Z} f(A)}} \\ &= \frac{\frac{\text{id}}{\iota_1(f(A)) \vdash_W \iota_1(f(A))} \quad \frac{\text{id}}{\iota_2(f(A)) \vdash_Z \iota_2(f(A))}}{\frac{\text{id}}{\iota_1(f(A)) \oplus \iota_2(f(A)) \vdash_{W+Z} f(A)}} \end{align*} $$

For a given $\mathcal{I}$ this model should be the initial model of $\mathbf{MAInd}_{\mathcal{I}}\mathbf{LL}$, for a good notion of category of models.

# 6 Generating Models by Free Coproducts

We introduce a general semantic construction rooted in the notion of coproduct completion of categories.

It is tempting to consider a provable sequent $A \vdash_X B$ of $\mathbf{MAInd}_{\mathcal{I}}\mathbf{LL}$, for $X \in \mathbf{Set}$, as a set $\{\iota_x(A) \vdash \iota_x(B) \mid x \in X\}$ of provable sequents of MALL, intuitively representing all possible behaviors of programs by selecting conditionals non-deterministically.

From a semantic perspective, this corresponds to the coproduct completion, which takes a model $\mathcal{C}$ of MALL and add all coproducts to get a category $\mathcal{C}$ which determines a fibration over some $L: \mathbf{Set} \to \mathbf{StAut}$.

## 6.1 A relational model for $\mathbf{MAInd}_{\mathcal{I}}\mathbf{SetLL}$

The functor $L: \mathbf{Set}^{\text{OP}} \to \mathbf{StAut}$ defined as

* for $X \in \mathbf{Set}$, $L(X) := \prod_X \mathbf{Rel}$ is the category of $X$-indexed sets of sets (as objects of $\mathbf{Rel}$) and pointwise relations,

* and for $f \in \mathbf{Set}(X, Y)$, the functor $L(f)$ is given by $L(f)((A_y)_{y \in Y}) := (A_{f(x)})_{x \in X}$ and $L(f)((r_y)_{y \in Y}) := (r_{f(x)})_{x \in X}$.

We can verify that $L(X) = \mathbf{Rel}^X$, as a product of star-autonomous categories, is a star-autonomous category, with $\mathbb{1}_{L(X)} := (\mathbb{1})_{x \in X}$, $(A_x)_{x \in X} \otimes (B_x)_{x \in X} := (A_x \otimes B_x)_{x \in X}$, and $(A_x)_{x \in X} := (A_x^{\perp})_{x \in X}$. Similarly, $L(f)$ trivially preserves the star-autonomous structure.
The Grothendieck construction $\int L$ is given by

• as objects the pairs $(X, (A_x)_{x \in X})$ for $X \in \mathbf{Set}$ and each $A_x \in \mathbf{Set}$,

• as morphisms from $(X, (A_x)_{x \in X})$ to $(Y, (B_y)_{y \in Y})$, the pairs $(f, (r_x)_{x \in X})$ for $f: X \to Y$ and each $r_x \subseteq A_x \times B_{f(x)}$.

The cartesian coproduct on $\int L$ is given by:

$$ \emptyset := (\emptyset, ()), \quad (X, (A_x)_{x \in X}) \oplus (Y, (B_y)_{y \in Y}) := (X \uplus Y, (A_x)_{x \in X}, (B_y)_{y \in Y}) $$

with

$$ \mathrm{init}_{(X,(A_x)_x)} := (\mathrm{init}_X^{\mathrm{Set}}, ()), $$

$$ \nabla_{(X,(A_x)_{x \in X})} := ((i, x) \mapsto x, (\mathrm{id}_{A_x}^{\mathrm{Rel}})_{(i,x) \in X \uplus X}) $$

$$ \iota_{1,(X,(A_x)_{x \in X}),(Y,(B_y)_{y \in Y})} := (x \mapsto (1, x), (\{(a, (1, a)) \mid a \in A_x\})_{x \in X}) $$

which is preserved by the projection functor $p_L: \int L \to \mathbf{Set}$ defined as $p_L(X, (A_x)_{x \in X}) := X$ and $p_L(f, (r_x)_{x \in X}) := f$.

The coproduct preserves cartesian arrows:

$$ \begin{align*} (f_1, (\mathrm{id}_{A_1,f_1(x)})_{x \in X_1}) \oplus (f_2, (\mathrm{id}_{A_2,f_2(x)})_{x \in X_2}) &= (f_1 + f_2, (\mathrm{id}_{A_1,f_1(x)})_{x \in X_1} (\mathrm{id}_{A_2,f_2(x)})_{x \in X_2}) \\ &= (f_1 + f_2, (\mathrm{id}_{A_{i,f_i(x)}})_{(i,x) \in X_1 \uplus X_2}) \\ &= (f_1 + f_2, (\mathrm{id}_{A_{(f_1+f_2)_{(i,x)}}})_{(i,x) \in X_1 \uplus X_2}) \end{align*} $$

Remains to fix and verify the interpretation atoms:

$$ \llbracket a : X \to \underline{A} \rrbracket := (\{a(x)\})_{x \in X} \qquad \llbracket f(a) \rrbracket := (\{a(f(x))\})_{x \in X} = Lf \llbracket a \rrbracket $$

## 6.2 The general construction

**Definition 6.1 (Coproduct completion).** Let $\mathbb{C}$ a category, we consider the Coproduct completion of $\mathbb{C}$, $\bar{\mathbb{C}}$, that can be presented as follows.

• $\mathrm{ob}(\bar{\mathbb{C}}) := \{(I, (X_i)_{i \in I}) \mid I \in \mathbf{Set}, X_i \in \mathrm{ob}(\mathbb{C})\}$ are the indexed subsets of $\mathrm{ob}(\mathbb{C})$.

• $\bar{\mathbb{C}}((I, (X_i)_{i \in I}), (J, (Y_j)_{j \in J})) = \{(f, (g_i)_{i \in I}) \mid f: \mathbf{Set}(I, J), g_i: \mathbb{C}(X_i, Y_{f(i)})\}$.

• The composition law is the pointwise composition, and the identity morphisms is the evident one, i.e., $\mathrm{id} = (\mathrm{id}, (\mathrm{id})_i)$ and $(f, (g_i)_{i \in I})$; $(f', (g'_i)_{i \in I}))((f; f'), (g_i; g'_{f(i)})_{i \in I})$.

The category $\bar{\mathbb{C}}$ is cocartesian monoidal, with coproducts given by set unions:

$$ (I, (X_{1,i})_{i \in I}) \oplus (J, (X_{2,i})_{i \in J}) := (I \uplus J, (X_{n,i})_{(n,i) \in I \oplus J}) $$

with the obvious functoriality and the injections:

$$ \iota_{k,(I_1,(X_{1,i})_{i \in I_1}),(I_2,(X_{2,i})_{i \in I_2})} = (\iota_{k,I_1,I_2}^{\mathrm{Set}}, (\mathrm{id}_{X_{k,i}})_{i \in I_k}). $$

**Lemma 6.2 ([5]).** Any free coproduct completion is an extensive category.

**Definition 6.3 (MAInd$_{\llbracket}$LL).** Any category $\llbracket$ together with a functor $\mathrm{atom}: \llbracket^{\mathrm{op}} \to \mathbf{Set}$ can be freely completed into an index structure, given by:
• the coproduct completion $\bar{\mathbb{I}}$ of $\mathbb{I}$,

• a contravariant functor of atoms given by $\overline{\mathrm{atom}}(I, (X_i)_{i \in I}) := \prod_{i \in I} \mathrm{atom}(X_i)$, and $\mathrm{atom}(f, (g_i)_{i \in I}) = ((y_j)_{j \in J}) \mapsto (\mathrm{atom}(g_i)(y_{f(i)}))_{i \in I}$.

**Theorem 6.4** (Models via Coproduct Completion). Let $\mathbb{I}$ be a category and $\mathrm{atom} : \mathbb{I}^{\mathrm{OP}} \to \mathrm{Set}$ a functor, so that $\mathrm{MAInd}_{\bar{\mathbb{I}}}LL$ is an indexed logic.

Any functor $L : \mathbb{I} \to \mathrm{StAut}$ together with an interpretation $[\cdot, \cdot]_X : \mathrm{atom}(X) \to \mathrm{ob}(L(X))$ such that $[[f(a)]] = Lf([\cdot, a])$, can be completed into a model of $\mathrm{MAInd}_{\bar{\mathbb{I}}}LL$ by

$$ \bar{L}(I, (X_i)_{i \in I}) := \prod_{i \in I} L(X_i) \\ \bar{L}(f, (g_i)_{i \in I})((y_j)_{j \in J}) := (Lg_i(y_{f(i)}))_{i \in I} $$

*Proof.* Since $\mathrm{StAut}$ has all coproducts, the only thing to show is that $\int \bar{L}$ is a cocartesian monoidal fibration:

• The category $\int \bar{L}$ is the free coproduct completion of $\int L$, thus it has coproducts, and the preservation of cartesian arrows is immediate.

• The projection preserves coproducts by functoriality of the free coproduct completion from $\mathrm{Cat}$ to $\mathrm{CartCat}^{\mathrm{op}}$, the category of cocartesian categories and cocartesian functors.

□

This construction has clear limitations. The main one is that $\bar{L}\emptyset$ is always the trivial category with one object and one morphism, thus we can't use it to support our claim that any model of indexed linear logics contains a meaningful model of LL. Another limitation is the size and/or lack of structure of $\bar{I}$.

# 7 Generating Models by Unfolding Compact Closed Models of MALL

We now present a more informative semantics of $\mathrm{MAInd}_{\bar{\mathbb{I}}}LL$ that comes from compact closed models of MALL. We first discuss the case of the relational model, being at the same time at the origin of indexed linear logic itself and a widely studied model. Then we generalize our construction to appropriate compact closed models of MALL, that have an underlying structure which recalls the category of sets and relations.

## 7.1 A Relational Model for $\mathrm{MAInd}_{\bar{\mathbb{I}}}LL$

We consider the case where $\mathbb{I} = \mathrm{Set}$. Given, $X \in \mathrm{Set}$, We want to build $LX$ as an appropriate star-autonomous category. We proceed as follows. The functor $L : \mathrm{Set}^{\mathrm{OP}} \to \mathrm{StAut}$ defined as

• for $X \in \mathrm{Set}$, $LX$ is defined as:

– $\mathrm{ob}(LX) := \{(\underline{A}, A) | \underline{A} \in \mathrm{Set}, A \in \mathrm{Set}(X, \underline{A})\}$, by abuse of notation, we will often write $A$ for the pair $(\underline{A}, A)$,
- $LX(A, B) := \{m \in \mathbf{Rel}(\underline{A}, \underline{B}) | \forall x \in X, (A(x), B(x)) \in m\}$.

- Composition and identities are those of Rel. indeed, if for all $x \in X$, $(A(x), B(x)) \in m$ and $(B(x), C(x)) \in n$, a fortiori $(A(x), C(x)) \in (m; n)$, similarly, $(A(x), A(x)) \in \mathrm{id}_{\underline{X}}^{\mathrm{Rel}}$.

* For $f \in \mathbf{Set}(X, Y)$, the functor $Lf$ is given by precomposition: $Lf(\underline{A}, A) := (\underline{A}, (f; A))$ and $Lf(m) := m$.

**Remark 7.1.** We use the notation $\underline{A}$ to recall the basic intuition behind the original indexed linear logic construction, namely that formulae $X \vdash A$ corresponds to functions $A: X \to \llbracket A \rrbracket_{\mathrm{Rel}}$, where $\underline{A}$ stands for the standard linear logic formula we can obtain from $A$ and $\llbracket A \rrbracket_{\mathrm{Rel}}$ is its relational interpretation. Obviously, $\llbracket A \rrbracket_{\mathrm{Rel}}$ is just a set.

**Proposition 7.** For any set $X$, the category $LX$ is compact closed (and thus star-autonomous).

*Proof.* We detail the compact closed structure.

* The tensor product is defined as

$$(A \otimes B)(x) := (A(x), B(x)) \in \underline{A} \times \underline{B} \qquad m \otimes n := m \otimes^{\mathrm{Rel}} n.$$

We have to verify that for all $x \in X$, $((A \otimes B)(x), (A' \otimes B')(x)) = ((A(x), B(x)), (A'(x), B'(x)) \in (m \otimes n)$ knowing that $(A(x), A'(x)) \in m$ and $(B(x), B'(x)) \in m$, which is immediate.

* The terminal object is $\mathbb{1}(x) := * \in \{*\}$.

* The dual $A^{\perp}$ of an object $A$ is simply defined as $A^{\perp} := A$ (as in Rel).

* The $\mu_A : LX(\mathbb{1}, A \times A^{\perp})$ and $\epsilon_A : LX(A^{\perp} \times A, \mathbb{1})]$ are defined as those of Rel:

$$\mu_A := \mu_{\underline{A}}^{\mathrm{Rel}} \qquad \epsilon_A := \epsilon_{\underline{A}}^{\mathrm{Rel}}.$$

* All diagrams are automatically respected since the structure we defined is preserved by the forgetful functor to Rel, which is already compact closed.

□

**Remark 7.2.** The Grothendieck construction $\int L$ is defined as follows.

* $\mathrm{ob}(\int L) = \{(X, \underline{A}, A) | A \in \mathbf{Set}(X, \underline{A})\} = \mathrm{mor}(\mathbf{Set})$.

* $\int L((X, \underline{A}, A), (Y, \underline{B}, B)) = \{(f, m) | f: X \to Y, m \in \mathrm{Rel}(\underline{A}, \underline{B}), \forall x \in X, (A(x), B(f(x))) \in m\}$.

This category has a cocartesian monoidal structure, defined as follows.

* The coproduct and initial object are given by

$$A \oplus B := A \oplus^{\mathrm{Set}} B \quad (f, m) \oplus (g, n) := (f \oplus^{\mathrm{Set}} g, m \oplus^{\mathrm{Rel}} n) \quad \emptyset := \mathrm{id}_{\emptyset} \\ \mathrm{init}_{X, \underline{A}, A} = (\mathrm{init}^{\mathrm{Set}}_{X}, \emptyset) \quad \ell_{i, A_1, A_2} = (\ell_i^{\mathrm{Set}}, \ell_i^{\mathrm{Rel}}).$$

Since the coproduct of Set is that of Rel restricted to Set, everything works as routine.

* The projection is obviously cartesian. The cartesian arrows are preserved since the second projection on arrows targets the coproduct of Rel which is a functor:

$$(f, \mathrm{id}) \oplus (g, \mathrm{id}) := (f \oplus^{\mathrm{Set}} g, \mathrm{id} \oplus^{\mathrm{Rel}} \mathrm{id}) = (f \oplus g, \mathrm{id}).$$
## 7.2 The General Construction

We now extend the former construction from the relational case to a more general setting. From a poset-enriched model $\mathbb{C}$ of MALL with appropriate structure, we can construct a non trivial model of $\mathbb{M}Ind_{\mathbb{C}}LL$ for some index category $\mathbb{I}$.

**Definition 7.3 (Category with Linear Relations).** We call category with linear relations a category equipped with:

1. a relation equipment $(\mathbb{C}, -^*, -_*)$ [22], spelling this out :

* A poset-enriched category $\mathbb{C}$. A functor $*_\mathbb{I} : \mathbb{I} \to \mathbb{C}$ that is bijective on objects and locally fully faithful.

* For each arrow $f \in \mathbb{I}(X, Y)$, an arrow $f^* \in \mathbb{C}(Y, X)$ that is a right adjoint of $f_*$, i.e., such that $f^*; f_* \le \mathrm{id}_Y$ and $f_*; f^* \ge \mathrm{id}_Y$.

2. a compact closed structure $(\otimes, -^\perp, \mu, \epsilon)$ and a biproduct $(+, \emptyset, \nabla, \Delta, \mathrm{init}, \mathrm{term})$ making $\mathbb{C}$ a compact closed model of MALL.

3. A coproduct $(+, \emptyset, \mathrm{init}, \nabla)$ on $\mathbb{I}$ inherited from the biproduct of $\mathbb{C}$:

$$X + \mathbb{I} Y = X + \mathbb{C} Y, \quad \emptyset \mathbb{I} = \emptyset \mathbb{C}, \quad \mathrm{init}_* = \mathrm{init}, \quad \nabla_* = \nabla \quad \mathrm{init}^* = \mathrm{term}, \quad \nabla^* = \Delta.$$

4. An involutive functor $\mathbb{I}^{\mathrm{op}} : \mathbb{I} \to \mathbb{I}$ such that

$$X^{\mathrm{op}} = X^{\perp}, \quad (f^{\mathrm{op}})_* = (f^*)^{\perp}, \quad (f^{\mathrm{op}})^* = (f_*)^{\perp}.$$

5. A cartesian product $(+, \emptyset, \mathrm{term}, \Delta)$ on $\mathbb{I}$ inherited from the tensor product of $\mathbb{C}$:

$$X \times \mathbb{I} Y = X \times \mathbb{C} Y, \quad \mathbb{I} \mathbb{I} = \mathbb{I} \mathbb{C}.$$

6. A monoidal natural transformation $\alpha_X : X \to X^{\mathrm{op}}$ such that:

$$\alpha_X; \alpha_{X^{\mathrm{op}}} = \mathrm{id}_X \qquad \alpha_* = \mathrm{uncur}_{\mathbb{I}, X, X^{\mathrm{op}}}(\mathrm{term}^*_{X^{\mathrm{op}}}; \Delta_{X^{\mathrm{op}*}}).$$

**Example 7.4.** The category Rel is obviously a category with linear relations. Another example is given by the category Polr, of preorders and monotonic relations. In particular, from this category one can define the Scott semantics of linear logic [8]. Another example is given by the category Span(Set), whose objects are sets and morphisms $F : A \to B$ are spans of sets, i.e., pairs of functions $A \leftarrow X \to B$ for some set $X$.

**Definition 7.5.** For any object $X \in \mathbb{I}$, let $\mathbb{C}^X$ be the following category:

* objects: $A \in \mathbb{I}(X, \Delta)$

* morphisms: $\mathbb{C}^X(A, B)$ are morphisms $m \in \mathbb{C}(A, B)$ such that

<figure><img src="image_6.png" /></figure>
The identity is the identity of $\mathbb{C}$ since $A^*$; $A_* \ge \mathrm{id}_{\underline{A}}$, and the composition likewise since $\mathrm{id}_X \ge B_*; B^*$.

<figure><img src="image_7.png" /></figure>

**Lemma 7.6.** For any $X \in \mathbb{I}_{\mathbb{C}}$, $(\mathbb{C}^{\wedge}X, \langle \cdot, \cdot \rangle, \mathrm{term})$ is a monoidal category.

*Proof.* Inherited from the 2-monoidality of $\times$ in $\mathbb{C}$:

<figure><img src="image_8.png" /></figure>

**Lemma 7.7.** We have an orthogonality $\mathbb{C}^\bullet : \mathbb{C}^{\wedge}X \to \mathbb{C}^{\wedge}X^{\mathrm{op}}$ defined as follow:

$$A^\bullet := (\alpha_X; A^{\mathrm{op}}) \qquad : X \to \underline{A}^{\mathrm{op}}$$

$$m^\bullet := m^\perp \qquad : \mathbb{C}^{\wedge}X(B^\bullet, A^\bullet)$$

*Proof.* The definition is correct, i.e., if $m : \mathbb{C}^{\wedge}X(A, B)$ then $m^\perp : \mathbb{C}^{\wedge}X(B^\bullet, A^\bullet)$:

<figure><img src="image_9.png" /></figure>
where the bottom 2-cell is obtained by reversing the 2-cell of $m : A \to B$.
The preservation of the identity and composition are inherited from those of the
functor $-^{\perp}$ in $\mathbb{C}$. The involution comes from the involutions of $\alpha$ and $-^{\text{op}}$. $\square$

**Corollary 7.8.** For any $X \in \mathbb{C}$, $(\mathbb{C}^{\wedge}X, \times, 1, -^{\bullet}, \mu, \epsilon)$ is a compact closed category.

*Proof.* The dualizing morphisms are given by $\mu^L = \mu^C : A^\bullet \times A \to 1$ and $\epsilon^L = \epsilon^C : 1 \to A \times A^\bullet$:

<figure><img src="image_10.png" /></figure>

<figure><img src="image_11.png" /></figure>

**Lemma 7.9.** $\mathbb{C}^{\wedge}: \mathbb{I}_{\mathbb{C}}^{\text{op}} \to \text{StAut}$ is a functor defined, on arrows, as the pre-composition functor, i.e., for $f : X \to Y$:

$$
\mathbb{C}^{\wedge} f(A) := f; A \quad \text{and} \quad \mathbb{C}^{\wedge} f(m) := m \quad \text{so that}
$$

<figure><img src="image_12.png" /></figure>

**Remark 7.10.** The Grothendieck construction on $\mathbb{C}^{\wedge}$ determines the category $\mathcal{C}^{\wedge}$, whose objects are morphisms $A : X \to \underline{A}$, for $\underline{A} \in \mathbb{C}$. Morphisms from $A : X \to \underline{A}$ to $B : Y \to \underline{B}$ are pairs $(f : X \to Y, m : \underline{A} \to \underline{B})$ such that $A^*; f_*; G_* \Rightarrow m$.

**Lemma 7.11.** $\mathcal{C}^{\wedge}$ is cocartesian with:

$$
(X, A) \oplus (Y, B) := (X+Y, A+B : X+Y \to \underline{A}+\underline{B}) \quad (f, m) \oplus (g, n) := (f+g, m+n)
$$

$$
\emptyset := (0, \mathrm{id}_0) \qquad \mathrm{init}_{X,A} := (\mathrm{init}_X^{\mathrm{Map}(\mathbb{C})}, \mathrm{init}_{\underline{A}}^{\mathbb{C}}) \qquad \nabla_{X,A} := (\nabla_X^{\mathrm{Map}(\mathbb{C})}, \nabla_{\underline{A}}^{\mathbb{C}}).
$$

*Proof.* • _ ⊕ _ well defined and functorial :
- if $m \ge A^*; f_*; B_*$ and $n \ge A'^*; g_*; B'_*$ then $m+n \ge (A^*; f_*; B_*) + (A'^*; g_*; B'^*) = (A+A')^*(f+g; B+B')_*$.

- $(id, id) \oplus (id, id) = (id, id)$ by definition,

- $((f, m) \oplus (g, n)); ((f', m') \oplus (g', n')) = ((f+g); (f'+g'), (m+n); (m'+n')) = ((f; f')+(g; g'), (m; m')+(n; n')) = ((f, m); (f', m')) \oplus ((g, n); (g', n'))$

• $\emptyset$ is initial since $\mathrm{init}_{X,A}$ always exist and is unique by unicity of $\mathrm{init}_{\emptyset}^C$.

• The other diagrams are obtained directly from the co-cartesian structures of $\llcorner$ and $\llbracket$.

□

**Theorem 7.12.** $C^{\wedge}$ is a model of $\mathrm{MAInd}_{\llcorner LL}$.

# 8 Variants of MAIndLL inspired from their semantics

Our semantics may be a bit abstract, but it is in fact very simple. And this simplicity allows us to change small conditions and consider the corresponding logics. Notice that our notion of “variants” here is orthogonal to the notion of modularity relative to the categories of loci, in fact each of the variations below are modular relatively to the same categories of loci (or variants of those).

## 8.1 MAIndILL logics

A natural variant to look at is the functors $L: \llcorner \to SMCC$ targeting symmetric monoidal closed categories rather than $*-\text{autonomous categories}$.

Everything works the same way, and we obtain models for the obvious intuitionistic restrictions of MAIndLL, except for the $\&$: Lemma 4.23 being only true if we force the $\perp$ in the SMCCs, we need to force the opfibration $\frown L$ to be cartesian.

## 8.2 IndLJ logics

Similarly, we can look at functors $L: \llcorner \to CCC$ targeting cartesian closed categories rather than $*-\text{autonomous categories}$.

In this case, as above the opfibration $\frown L$ will need to be cartesian. In addition, despite having two products, the external product $\&$ and the internal product $\otimes$, those products are identified in the category $L0$.

Notice also that if $\llcorner$ has products, then $\int L$ will have products by externalisation of the internal products [22, p. 12.7].

## 8.3 Getting rid of extensivity

We can also have variations on the extensivity of $\llcorner$. Indeed, the extensivity, contrary to the existence of finite coproducts, is a syntactical condition here as it has no utility to define the model. Its interest only lies in defining $f(A \oplus B)$ correctly.

The extensiveness is just one of many ways to define $f(A \oplus B)$. Another way would be to add an operator $\mathrm{let}_f$ and define $f(A \oplus B)$ as $\mathrm{let}_f(A \oplus B)$. We
call functor such an operator as this will correspond to the notion of functor we will define in the exponential generalization.

This is, in a way, what is done in [23]. This is also what happens when slicing a model of MALL.

## 8.4 MABLL

The solution above, consisting in using a multifunctor $let_f$ for any $f$ is quite extreme. In a lot of cases, we can restrict ourselves to only a few of them, this is what happens, for example, if $\mathcal{I}$ has biproducts, in this case, we can define $f(A \oplus B)$ as $let_\delta(f(\pi_1(A)) \oplus f(\pi_2(B)))$.

But if $\mathcal{I}$ has biproducts, then the external coproducts of $\int L$ can be internalized in the fibers [22] and it is equivalent to consider a logic with products and coproducts in every fiber and only monomorphic actions. This is can thus be generalized in considering weakenable indexes that do not interact with operators (excepts for atoms/constants). Such a situation appears when considering additives in logics like BLL [13] or with graded exponentials [2].

## 8.5 Merging with separation logics ?

Finally, another simple variation one can consider is to require more properties on the fibration.

In particular, it seems natural to require the opfibration $\mathcal{L} \to L$ to not only be cartesian, but also closed. In addition, we require the adjunction isomorphisms $\Lambda: \mathcal{L}(U, V \Rightarrow W) \simeq \mathcal{L}(U \& V, W)$ to preserve fibers, i.e., that $\Lambda(id, \phi) = (id, \phi')$. Using this preservation of fibers, we get the derivation:

$$ \frac{\Gamma \& B \vdash_{X+Y} C}{\Gamma \vdash_X B \dashv C} $$

The issue comes with the domain of definition, indeed, $B \dashv C$ is defined over a certain $X$ such that $Y \dashv B$ and $X + Y \dashv C$, while there can be several such $X$. Nonetheless, the structures seems to be a reminiscent of what happens in separation logic<fnref n="5" />, except that we inverse cartesian and monoidal products. This inversion is easy to discard, by removing the Cartesian constraint of $\&$ in $\mathcal{L}$ and adding one for $\otimes$ in each fiber.

# 9 Conclusion

**Related Work** Our work should be compared to Licata, Shulman and Riley's [15] where they present a logic living, like ours, in the fibers of a fibration over an appropriate category. However, their 'index category' is representing constrains over the resource usage and/or allowed operator, making their logic extremely different in nature from ours.

From a syntactic perspective, in addition to the original papers of Ehrhard and Bucciarelli [3, 4], we should mention Breuvart's Thesis [1] and to a recent article from Fukihara and Katsumata [10], both of which aim to modularize bounded linear logic, which is close enough to IndLL.

<footnote n="5">⁵Though, not with BI logic which erase heap-dependency the way LL erase loci dependency of IndLL.</footnote>
From a semantics perspective, we can relate to Melliès and Zeilberger's func-
torial interpretation of separation logic [19, Section 5]. They see the bunch
product * of separation logic as a monoidal product of op-fibration. However,
they place the logic in the op-fibration Rather than tracking it back in the fibers
like we do. This is because they consider (bi)fibrations over calculus, while we
consider those over invariants, so that functions naturally live in fibers. Other
works from the authors [20, 18] are also relevant.

**Summary and future works** We gave a presentation of MALL with in-
dexes that tracks the additive structure. We have seen that the rules of our
logic can be modular with respect to a choice of category `I` of loci, encompass-
ing the multiplicative-additive fragment of the original indexed linear logic, the
standard MALL, but also many other instances.

We defined a categorical semantics for our system that makes explicit how
the connectives of indexed logics live in at least two different worlds: the fibers
and the fibration itself. We believe that this study can be extended to other
kinds of logics and that results of total or partial internalization of the properties
of fibrations should correspond to new syntactic constructors of indexed logics.

However, applications of such logic are hardly imaginable as the only interac-
tion between formulae and loci are the atoms, which are so constraint that they
can't represent much more that an unknown formula. In order to understand
the potential of such system, we need another kind of operators that allows to
arbitrary change the locus of a formula.

In the incoming sequel of this paper, we treat a particular example of such an
operator: the *indexed exponentials*. The exponentials `!_u A` of IndLL are indexed
by a function *u* similar to that of graded exponentials, except that those have a
source *X* and target *Y* in `I`, and, in term of semantics, `!_u` is a functor from *LY*
to *LX*, a *priori* different from any of the functorial actions *Lf*.

We formalize this by requiring the loci category to be the vertical restriction
of a (thin) *double category* which horizontal restriction would be the category in-
dexes of our exponentials. This presentation, albeit quite synthetic and elegant,
carries new challenges, both semantic (definition of double fibration and ax-
iomatisation of Seely isomorphisms) and syntactic (definition of actions $f(!_u A)$
and subtyping). That is why we chose to split the work in half and address
separately the simpler issues of the multiplicative-additive fragment.

References

[1] Flavien Breuvart. “Dissecting denotational semantics: from the well-established $\mathcal{H}^*$ to the more recent quantitative coefficients”. PhD thesis. Université Paris Diderot, 2015.

[2] Aloïs Brunel et al. “A Core Quantitative Coeffect Calculus”. In: *Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014*. Vol. 8410. Lecture Notes in Computer Science. Springer, 2014, pp. 351–370. DOI: 10.1007/978-3-642-54833-8\_19.
[3] Antonio Bucciarelli and Thomas Ehrhard. "On Phase Semantics and Denotational Semantics in Multiplicative-Additive Linear Logic". In: *Ann. Pure Appl. Log.* 102.3 (2000), pp. 247–282. DOI: 10.1016/S0168-0072(99)00040-8.

[4] Antonio Bucciarelli and Thomas Ehrhard. "On phase semantics and denotational semantics: the exponentials". In: *Ann. Pure Appl. Log.* 109.3 (2001), pp. 205–241. DOI: 10.1016/S0168-0072(00)00056-7.

[5] Aurelio Carboni, Stephen Lack, and R.F.C. Walters. "Introduction to extensive and distributive categories". In: *Journal of Pure and Applied Algebra* 84.2 (1993), pp. 145–158. ISSN: 0022-4049. DOI: https://doi.org/10.1016/0022-4049(93)90035-R.

[6] collaborative. nLab. https://ncatlab.org.

[7] Thomas Ehrhard. "Non-idempotent intersection types in logical form". In: *CoRR* abs/1911.01899 (2019). arXiv: 1911.01899. URL: http://arxiv.org/abs/1911.01899.

[8] Thomas Ehrhard. "The Scott model of linear logic is the extensional collapse of its relational model". In: *Theor. Comput. Sci.* 424 (2012), pp. 20–45. DOI: 10.1016/j.tcs.2011.11.027.

[9] Soichiro Fujii, Shin-ya Katsumata, and Paul-André Melliès. "Towards a Formal Theory of Graded Monads". In: *Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS*. Vol. 9634. Lecture Notes in Computer Science. Springer, 2016, pp. 513–530. DOI: 10.1007/978-3-662-49630-5\_30.

[10] Yoji Fukihara and Shin-ya Katsumata. "Generalized Bounded Linear Logic and its Categorical Semantics". In: *Foundations of Software Science and Computation Structures - 24th International Conference, FOSSACS*. Vol. 12650. Lecture Notes in Computer Science. Springer, 2021, pp. 226–246. DOI: 10.1007/978-3-030-71995-1\_12.

[11] Marco Gabardi et al. "Combining effects and coefficients via grading". In: *Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP, 2016*. ACM, 2016, pp. 476–489. DOI: 10.1145/2951913.2951939.

[12] Dan R. Ghica and Alex I. Smith. "Bounded Linear Types in a Resource Semiring". In: *Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014*. Vol. 8410. Lecture Notes in Computer Science. Springer, 2014, pp. 331–350. DOI: 10.1007/978-3-642-54833-8\_18.

[13] Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. "Bounded Linear Logic: A Modular Approach to Polynomial-Time Computability". In: *Theor. Comput. Sci.* 97.1 (1992), pp. 1–66. DOI: 10.1016/0304-3975(92)90386-T.

[14] Andrej Ivaskovic, Alan Mycroft, and Dominic Orchard. "Data-Flow Analyses as Effects and Graded Monads". In: *5th International Conference on Formal Structures for Computation and Deduction, FSCD*. Ed. by Zena M. Ariola. Vol. 167. LIPIcs. 2020, 15:1–15:23. DOI: 10.4230/LIPIcs.FSCD.2020.15.
[15] Daniel R. Licata, Michael Shulman, and Mitchell Riley. "A Fibrational Framework for Substructural and Modal Logics". In: *2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017*. Vol. 84. LIPIcs. 2017, 25:1-25:22. DOI: 10.4230/LIPIcs.FSCD.2017.25.

[16] Damiano Mazza, Luc Pellissier, and Pierre Vial. "Polyadic approximations, fibrations and intersection types". In: *Proc. ACM Program. Lang. 2.POPL (2018)*, 6:1-6:28. DOI: 10.1145/3158094.

[17] Paul-André Melliès. "A micrological study of negation". In: *Ann. Pure Appl. Log.* 168.2 (2017), pp. 321-372. DOI: 10.1016/j.apal.2016.10.008.

[18] Paul-André Melliès and Noam Zeilberger. "A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine". In: *Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016*. ACM, 2016, pp. 555-564. DOI: 10.1145/2933575.2934525.

[19] Paul-André Melliès and Noam Zeilberger. "Functors are Type Refinement Systems". In: *Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL*. ACM, 2015, pp. 3-16. DOI: 10.1145/2676726.2676970.

[20] Paul-André Melliès and Noam Zeilberger. "Type refinement and monoidal closed bifibrations". In: *CoRR abs/1310.0263 (2013)*. arXiv: 1310.0263. URL: http://arxiv.org/abs/1310.0263.

[21] Federico Olimpieri. "Intersection Type Distributors". In: *36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021*. IEEE, 2021, pp. 1-15. DOI: 10.1109/LICS52264.2021.9470617.

[22] Michael A. Shulman. "Framed bicategories and monoidal fibrations". In: *CoRR* (2007). DOI: 10.48550/ARXIV.0706.1286. arXiv: 0706.1286.

[23] Matthijs Vákár and Tom Smeding. "CHAD: Combinatory Homomorphic Automatic Differentiation". In: *ACM Trans. Program. Lang. Syst.* 44.3 (2022), 20:1-20:49. DOI: 10.1145/3527634.