{'fraction_non_alphanumeric': 0.06744784765077802, 'fraction_numerical': 0.00920001514405785, 'mean_word_length': 3.5419138509156562, 'pattern_counts': {'":': 0, '<': 10, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 31, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Categorical models of Linear Logic with fixed points of formulas

We develop a denotational semantics of muLL, a version of propositional Linear Logic with least and greatest fixed points extending David Baelde's propositional muMALL with exponentials. Our general categorical setting is based on the notion of Seely category and on strong functors acting on them. We exhibit two simple instances of this setting. In the first one, which is based on the category of sets and relations, least and greatest fixed points are interpreted in the same way. In the second one, based on a category of sets equipped with a notion of totality (non-uniform totality spaces) and relations preserving them, least and greatest fixed points have distinct interpretations. This latter model shows that muLL enjoys a denotational form of normalization of proofs.


I. INTRODUCTION
Propositional Linear Logic is a well-established logical system introduced by Girard in [1]. It provides a fine-grain analysis of proofs in intuitionistic and classical logic, and more specifically of their cut-elimination. LL features a logical account of the structural rules (weakening, contraction) which are handled implicitly in intuitionistic and classical logic. For this reason, LL has many useful outcomes in the Curry-Howard based approach to the theory of programming: logical understanding of evaluation strategies, new syntax of proofs/programs (proof-nets), connections with other branches of mathematics (linear algebra, functional analysis, differential calculus), new operational semantics (geometry of interaction) etc.
However propositional LL is not a reasonable programming language, by lack of data-types and iteration or recursion principles. This is usually remedied by extending propositional LL to the 2 nd order, thus defining a logical system in which Girard's System F [2] can be embedded. Another option to turn propositional LL into a programming languagecloser to usual programming -is to extend it with least and greatest fixed points of formulas. Such an extension was early suggested by Girard in an unpublished note [3], though the first comprehensive proof-theoretic investigation of such an extension of LL is recent: in [4] Baelde considers an extension µMALL of Multiplicative Additive LL sequent calculus with least and greatest fixed points. His motivations arose from a proof-search and system verification perspective and therefore his µMALL logical system is a predicate calculus. Our purpose is to develop a more Curry-Howard oriented point of view on LL with fixed points and therefore we stick to the proposition calculus setting of [2]. But, unlike [4] we include the exponentials in our system from the beginning 1 , so we call it µLL rather than propositional µMALL and we consider it as an alternative to the "system F" approach to representing programs in LL. Our system µLL could also have applications to session types, in the line of [5]. The ν-introduction rule of µLL (Park's rule, that is rule (ν-rec) of Section II-F1) leads to subtle cut-elimination rewrite rules for which Baelde could prove cut-elimination in µMALL, showing for instance that a proof of the type of integers µζ (1 ⊕ ζ) necessarily reduces to an integer (in contrast with LL, µMALL enjoys only a restricted form of sub-formula property). There are alternative proofsystems for the same logic, involving infinite or cyclic proofs, see [6], whose connections with the aforementioned finitary proof-system are not completely clear yet.
Since the proof-theory (and hence the "operational semantics") of µLL is still under development, it is important to investigate its categorical semantics, whose definition does not rely on the precise choice of inference and rewrite rules we equip µLL with, see the Outcome § below. We develop here a categorical semantics of µLL extending the standard notion of Seely category 2 of classical LL, see [7]. Such a model of µLL consists of a Seely category L and of a class of functors L n → L for all possible arities n which will be used for interpreting µLL formulas with free variables. These functors have to be equipped with a strength to deal properly with contexts in the rule (ν-rec), see Section II-F2 for a discussion on these contexts in particular.
Then we develop a simple instance of this setting which consists in taking for L the category of sets and relations, a well-known Seely model of LL. The variable sets are the strong functors we consider on this category. They are the pairs F = (F, F) where F is the strength and F : Rel n → Rel is a functor which is Scott-continuous in the sense that it commutes with directed unions of morphisms. This property implies that F maps injections to injections and is cocontinuous on the category of sets and injections. There is no special requirement about the strength F beyond naturality, monoidality and compatibility with the comultiplication of the comonad ! . Variable sets form a Seely model of µLL where linear negation is the identity on objects. The formulas µζ F and νζ F are interpreted as the same variable set, exactly as ⊗ and`are interpreted in the same way (and similarly for additives and exponentials). This denotational "degeneracy" at the level of types is a well known feature of Rel which does not mean at all that the model is trivial. For instance normal multiplicative exponential LL proofs which have distinct relational interpretations have distinct associated proof-nets [8], [9].
Last we enrich this model Rel by considering sets equipped with an additional structure of totality: a non-uniform totality space (NUTS) is a pair X = (|X|, T (X)) where |X| is a set and T (X) is a set of subsets of |X|which intuitively represent the total, that is, terminating computations of type X. This set T (X) is required to coincide with its bidual for a duality expressed in terms of non-empty intersections. This kind of definition by duality is ubiquitous in LL since [1] and has been categorically formalized as double gluing in [10]. We don't use this categorical formalization here however as it would not simplify the presentation. One nice feature of this specific duality is that the bidual of a set of subsets of |X| is simply its upwards-closure (wrt. inclusion) 3 , see Lemma 17. Given two NUTS X and Y there is a natural notion of total relation t ⊆ |X| × |Y | giving rise to a category Nuts which is easily seen to be a Seely model of LL. To turn it into a categorical model of µLL, we need a notion of strong functors Nuts n → Nuts. Rather than considering them directly as functors, we define variable non-uniform totality spaces (VNUTS) as pairs X = (|X|, T (X)) where |X| : Rel n → Rel is a variable set and, for each tuple X = (X 1 , . . . , X n ) of VNUTS's, T (X)( X) is a totality structure on the set |X|(| X|). It is also required that the action of the functor |X| on Nuts morphisms and the strength X respect this totality structures. Then it is easy to derive from such a VNUTS X a strong functor Nuts n → Nuts and we prove that, equipped with these strong functors, Nuts is a model of µLL. a) Outcome: One major benefit of this construction is that it gives a value to all proofs of µLL, invariant by cutelimination. Moreover, the fact that this value is total shows in a syntax independent way that when π is for instance a µLL proof of 1⊕1 (the type of booleans), the value associated with π is non-empty, that is, π has a defined boolean value true or false 4 . We could also obtain this by a normalization theorem: π reduces to one of the two normal proofs of 1 ⊕ 1 (and if we prove for instance a Church-Rosser theorem we will know that this proof is unique). Such proofs would depend of course on the actual presentation of the syntax whereas our denotational argument does not. b) Related work: There is a vast literature on extending logic with fixed point that we cannot reasonably summarize, see the discussions in [15], [6]. Cut-elimination of such systems has been extensively investigated, see for instance [16], [17], [18], [19]. Closer to ours is the work of Santocanale [20] and its categorical interpretation in µbicomplete categories [21] which, unlike most contributions in this field, considers also categorical interpretations of proofs. Santocanale et al. consider circular proofs whereas we use Park's rule. A deeper difference lies in the logic itself: from an LL point of view the logic considered by Santocanale et al. is purely additive linear logic with least and greatest fixed points µALL which seems too weak in our Curry-Howard perspective. And indeed µ-bicomplete categories do not provide the monoidal and exponential structures required for interpreting µLL.
In [22], that we became aware of only recently (and seems related to the earlier report [23]), Loader extends the simply typed λ-calculus with inductive types and develops its denotational semantics. His models are cartesian closed categories C equipped with a class of strong functors and seem very close to ours (Section II-F): one might think that any of our models yields a Loader model as its Kleisli category. This is not the case because in a Loader model the category C is cocartesian 5 whereas the Kleisli category of a Seely category is not cocartesian in general: this would require to have an iso between !(X ⊕ Y ) and !X ⊕ !Y which is usually absent. Loader studies two concrete instances of his models: one is based on recursion theory (partial equivalence relations) and the other on a notion of domains with totality described as a model of LL. This model might give rise to one of our Seely models, this point requires further studies. Our NUTS are quite different from Loader totality domains which feature a notion of "consistency" enforcing some kind of determinism and, combined with totality, allow the Kleisli category to be cocartesian as well. Our model is based on Rel and therefore is compatible with non-determinism [24] and PCF recursion. This is important for us because we would like to consider rules beyond Park's rule for inductive and coinductive types, based on PCF fixed points -with further guardedness conditions for guaranteeing termination -in the spirit of [25], [26], [27] or even on infinite terms in the spirit of [6].
We mention also the work of Clairambault [28], [29] who investigates the game with totality semantics of an extension of intuitionistic logic with least and greatest fixed points (independently of [22], [23]). A Kleisli-like connection with his work should be sought too. c) Notations: We use the following conventions: a stands for a list (a 1 , . . . , a n ). A unary operation f is extended to lists of arguments in the obvious way: f ( a) = (f (a 1 ), . . . , f (a n )). When we write natural transformations, we very often omit the objects where they are taken keeping them implicit for the sake of readability, when they can easily be retrieved from the context. If A is a category then Obj(A) is its class of objects and if A, B ∈ Obj(A) then A(A, B) is the set of morphisms from A to B in A (all the categories we consider are locally small). If F : A × B → C is a functor and A ∈ Obj(A) then F A : B → C is the functor defined by F A (B) = F (A, B) and Most proofs can be found in an Appendix.

II. CATEGORICAL MODELS OF LL
A. Seely categories.
We recall the basic notion of categorical model of LL. Our main reference is the notion of a Seely category as presented in [7]. We refer to that survey for all the technical material that we do not recall here.
A Seely category is a symmetric monoidal closed category are natural isomorphisms satisfying coherence diagrams that we do not record here. We use X ⊸ Y for the object of linear morphisms from X to Y , ev ∈ L((X ⊸ Y ) ⊗ X, Y ) for the evaluation morphism and cur for the linear curryfication map L(Z ⊗ X, Y ) → L(Z, X ⊸ Y ). We assume L to be * -autonomous with dualizing object ⊥ (this object is part of the structure of a Seely category). We use X ⊥ for the object X ⊸ ⊥ of L (the dual, or linear negation, of X). It is also assumed that L is cartesian with final object ⊤, product X 1 & X 2 with projections π 1 , π 2 . By * -autonomy L is cocartesian with initial object 0, coproduct ⊕ and injections π i .

B. Oplax monoidal comonads
Let M be a symmetric monoidal category (with the same notations as above for the tensor product) and (T, ε, µ) : M → M be a comonad (ε is the unit and µ the multiplication). An oplax monoidal structure on T consists of a morphism θ 0 ∈ M(T 1, 1) and a natural transformation θ 2 X1,X2 ∈ M(T (X 1 ⊗ X 2 ), T (X 1 ) ⊗ T (X 2 )) subject to standard symmetric monoidality and compatibility with ε and µ, this latter reading (ε X1 ⊗ ε X2 ) θ X1,X2 = ε X1⊗X2 and: Then the Kleisli category M T has a canonical symmetric monoidal structure, with unit 1 and tensor product X 1 ⊗ X 2 defined as in M for objects. Given Let F T : M → M T be the canonical functor which acts as the identity on objects and maps f ∈ M(X, Y ) to f ε X ∈ M T (X, Y ).

C. Eilenberg-Moore category and free comodules
Let L be a Seely category. Since ! is a comonad we can define the category L ! of !-coalgebras (Eilenberg-Moore category of ! ). An object of this category is a pair P = (P , h P ) where P ∈ Obj(L) and h P ∈ L(P , !P ) is such that der P h P = Id and dig P h P = !h P h P . Then f ∈ L ! (P, Q) if f ∈ L(P , Q) and h Q f = !f h P . The functor ! can be seen as a functor from L to L ! mapping X to (!X, dig X ) and f ∈ L(X, Y ) to !f . It is right adjoint to the forgetful functor L ! → L. Given f ∈ L(P , X), we use f ! ∈ L ! (P, !X) for the morphism associated with f by this adjunction, one Then L ! is cartesian with final object (1, h 1 = µ 0 ) still denoted as 1 and product P 1 ⊗ P 2 = (P 1 ⊗ P 2 , h P1⊗P2 ) with . This category is also cocartesian with initial object (0, h 0 ) still denoted as 0 and coproduct P 1 ⊕ P 2 = (P 1 ⊕ P 2 , h P1⊕P2 ) with h P1⊕Q defined as follows. For i = 1, 2 one defines and then h P1⊕P2 is the unique morphism P 1 ⊕ P 2 → !(P 1 ⊕ P 2 ) such that h P1⊕P2 π i = h i for i = 1, 2. More details can be found in [7]. We use contr P ∈ L ! (P, P ⊗ P ) (contraction) for the diagonal and w P ∈ L ! (P, 1) (weakening) for the unique morphism to the final object.
1) The LL model of free comodules on a given coalgebra: Given an object 6 P of L ! , we can define a functor fc P : L → L which maps an object X to P ⊗X and a morphism f to P ⊗f . This functor is clearly an oplax monoidal comonad (with structure maps defined using w P , contr P and the monoidal structure of L) 7 . A coalgebra for this comonad is a Pcomodule. By Section II-B the Kleisli category L[P ] = L fc P of this comonad (that is, the category of free P -comodules) has a canonical structure of symmetric monoidal category (SMC).
We set F P = F fc P : L → L[P ]. Girard showed in [30] that L[P ] is a Seely model of LL with operations on objects defined in the same way as in L, and using the coalgebra structure of P for the operations on morphisms. Intuitively, P should be considered as a given context and L[P ] as a model in this context. This idea appears at various places in the literature, see for instance [31], [32]. Let us summarize this construction.
The object of linear morphisms from X to Y in L[P ] is X ⊸ Y , and the evaluation morphism satisfies the required monoidal closedness equations. With these definitions, the category L[P ] is * -autonomous, with ⊥ as dualizing object.
Specifically, given f ∈ L[P ](X, Y ), then f ⊥[P ] is the following composition of morphisms: using implicitly the iso between (Z ⊗X) ⊥ and Z ⊸ X ⊥ , and the * -autonomy of L allows to prove that indeed f ⊥[P ]⊥[P ] = f . The category L[P ] is easily seen to be cartesian with ⊤ as final object, X 1 & X 2 as cartesian product (and projections defined in the obvious way, applying F P to the projections of L). Last we define a functor ! P : L[P ] → L[P ] by ! P X = !X and, given f ∈ L[P ](X, Y ), we define ! P f ∈ L[P ](!X, !Y ) and this functor has a comonad structure (der[P ], dig[P ]) defined by der[P ] = F P (der) and dig[P ] = F P (dig) 8 .
which acts as the identity on objects and maps . This functor is strict monoidal symmetric and preserves all the con- We can actually consider L[ ] as a functor from L ! op to the category of Seely categories and functors which preserve their structure on the nose. This functor could probably more suitably be considered as a fibration in the line of [33], Section 7.

D. Strong functors on L
Given n ∈ N, an n-ary strong functor on L is a pair ) is a natural transformation, called the strength of F. We use the notation Z ⊗ (Y 1 , . . . , Y n ) = (Z ⊗Y 1 , . . . , Z ⊗Y n ). It is assumed moreover that the diagrams of Figure 1 commute, expressing the monoidality of this strength as well as its compatibility with the comultiplication of ! . The main purpose of this definition is that for any object P of L ! one can lift F to a functor F[P ] : L[P ] n → L[P ] as follows. First one sets F[P ]( X) = F( X). Then, given The fact that we have defined a functor results from the three diagrams of Figure 1 and from the definition of w P and contr P based on the Seely isomorphisms. Remark 2. Since the seminal work of Moggi [34] strong functors play a central role in semantics for representing effects. Our adaptation of this notion to the present LL setting follows the definition of an L-tensorial strength in [35].

1) Operations on strong functors:
There is an obvious unary identity strong functor I and for each object Y of L there is an n-ary Y -valued constant strong functor K Y ; in the first case the strength natural transformation is the identity morphism and in the second case, it is defined using w !X . Let F be an n-ary strong functor and G 1 , . . . , G n be kary strong functors. Then one defines a k-ary strong functor H = F • (G 1 , . . . , G n ): the functorial component H is defined in the obvious compositional way. The strength is and is easily seen to satisfy the commutations of Figure 1.
Given an n-ary strong functor, we can define its De Morgan dual F ⊥ which is also an n-ary strong functor. On objects, we set F ⊥ ( Y ) = F( Y ⊥ ) ⊥ and similarly for morphisms. The strength of F ⊥ is defined as the Curry transpose of the following morphism (remember that !X ⊸ Y ⊥ = (!X ⊗ Y ) ⊥ up to canonical iso): Then it is possible to prove, using the * -autonomy of L, that F ⊥⊥ and F are canonically isomorphic (as strong functors) 9 .
As a direct consequence of the definition of F ⊥ and of the canonical iso between F ⊥⊥ and F we get: The bifunctor ⊗ can be turned into a strong functor: one defines the strength as 10 By De Morgan duality, this endows`with a strength as well.
The bifunctor ⊕ is also endowed with a strength, simply using the distributivity of ⊗ over ⊕ (which results from the monoidal closedness of L). By duality again, & inherits a strength. The functor ! is equipped with the strength

E. Fixed Points of strong functors
The following facts are standard in the literature on fixed points of functors.

Definition 2. Let A be a category and F :
The category of coalgebras of the functor F will be denoted as Coalg A (F ). The notion of algebra of an endofunctor is defined dually (reverse the directions of the arrows f and f ′ ) and the corresponding category is denoted as Alg A (F ).
) is a final object in Coalg A (F ) then f is an iso. We assume that this iso is always the identity 12 as this holds in our concrete models so that this final object (νF , Id) satisfies F (νF ) = νF . We focus on coalgebras rather than algebras for reasons which will become clear when we deal with fixed points of strong functors. This universal property of νF gives us a powerful tool for proving equalities of morphisms.
Then there is a functor νF : We consider now the same νF operation applied to strong functors on a model L of LL. Let F be an n + 1-ary strong functor on L (so that F is a functor L n × L → L). Assume that for each X ∈ Obj(L n ) the category Coalg L (F X ) has a final object. We have defined νF : Lemma 5. Let F be an n + 1-ary strong functor on L such that for each X ∈ Obj(L n ), the category Coalg L (F X ) has a final object νF X . Then there is a unique n-ary strong functor νF such that νF( X) = νF X (and hence F( X, νF( X)) = νF( X)), Lemma 6. Let F be an n + 1-ary strong functor on L such that for each X ∈ Obj(L n ), the category Alg L (F X ) has an initial object µF X . Then there is a unique n-ary strong functor µF such that µF( X) = µF X (and hence F( X, µF( X)) = µF( X)), Proof: Apply Lemma 5 to the strong functor F ⊥ .

F. A categorical axiomatization of models of µLL
Our general definition of Seely categorical model of µLL is based on the notions and results above. We refer in particular to Section II-D for the basic definitions of operations on strong functors in our LL categorical setting.

Definition 7.
A categorical model or Seely model of µLL is a pair (L, L) where 1 L is a Seely category 2 L = (L n ) n∈N where L n is a class of strong functors L n → L, and L 0 = Obj(L) 3 if X ∈ L n and X i ∈ L k (for i = 1, . . . , n) then X • X ∈ L k and all k projection strong functors L k → L belong to L k 4 the strong functors ⊗ and & belong to L 2 , the strong functor ! belongs to L 1 and, if X ∈ L n , then X ⊥ ∈ L n 5 and last, for all X ∈ L 1 the category Coalg L (X) (see Section II-E) has a final object. So for any X ∈ L k+1 there is a strong functor νX : L k → L (see Lemma 5). It is required that νX ∈ L k .
Remark 3. By Conditions 2 and 3 (applied with n = 0), all constant strong functors are in L n , for all n. Therefore given X ∈ L k+1 and X ∈ Obj(L) k , the strong functor X( , X) is in L 1 by Condition 3. This explains why we can apply Lemma 5 in Condition 5.
Our goal is now to outline the interpretation of µLL formulas and proofs in such a model. This requires first to describe the syntax of formulas and proofs.
Remark 4. One can certainly also define a notion of categorical model of µLL in a linear-non-linear adjunction setting as presented in [7]. This is postponed to further work.

1) Syntax of µLL:
We assume to be given an infinite set of propositional variables V (ranged over by Greek letters ζ, ξ . . . ). We introduce a language of propositional LL formulas with least and greatest fixed points.
The notion of closed formula is defined as usual, the two last constructions being the only binders.
Remark 5. In contrast with second-order LL or dependent type systems where open formulas play a crucial role, in the case of fixed points, all formulas appearing in sequents and other syntactical devices allowing to give types to programs will be closed. In our setting, open types/formulas appear only locally, for allowing the expression of (least and greatest) fixed points.
We can define two basic operations on formulas. • Substitution: A [B/ζ], taking care of not binding free variables (uses α-conversion). • Negation or dualization: defined by induction on formulas And indeed if it were possible to define a type D such that !D ⊸ D is isomorphic to (or is a retract of) D then we would be able to type all pure λ-terms in our system and this would contradict the fact that µLL enjoys strong normalization and has a denotational semantics based on totality as shown below.
Our logical system extends the usual unilateral sequent calculus of classical propositional LL [1], see also [7] Section 3.1 and 3.13. In this setting we deal with sequents ⊢ A 1 , . . . , A n where the A i 's are formulas. It is important to notice that the order of formulas in this list is not relevant, which means that we keep the exchange rule implicit as it is usual in sequent calculus. To the standard rules 13 of [7] Fig. 1, we add the two next introduction rules for fixed point formulas which are essentially borrowed to [4] (see Section II-F2) By taking, in the last rule, ∆ = A ⊥ and proving the left premise by an axiom, we obtain the following derived rule The corresponding cut-elimination rule is described in Section II-F4. For the other connectives (which are the standard connectives of LL), the cut-elimination rules are the usual ones as described in [1], [7].
2) Comments: Let us summarize and comment the differences between our system and Baelde's µMALL. • Baelde's logical system is a predicate calculus whereas our system is a propositional calculus. Indeed, Baelde is mainly interested in applying µMALL to program verification where the predicate calculus is essential for expressing properties of programs. We have a Curry-Howard perspective where formulas are seen at types and proofs as programs and where a propositional logical system is sufficient. • Our system has exponentials whereas Balede's system has not because they can be encoded in µMALL to some extent. However the exponentials encoded in that way do not satisfy all required isos (in particular the "Seely morphisms" are not isos with Baelde's exponentials) and this is a serious issue if we want to encode some form of λ-calculus in the system and consider it as a programming language.
• Our (ν-rec) rule differs from Baelde's by the fact that we admit a context in the right premise. Notice that all formulas of this context must bear a ? modality: this restriction is absolutely crucial for allowing to express the cut-elimination rule in Section II-F4 which uses an operation of substitution of proofs in formulas and this operation uses structural rules on the context. The semantic counterpart of this operation is described in Section II-D1 where it appears clearly that it uses the fact that P is an object of L ! . Such a version of (ν-rec) with a context would be problematic in Baelde's system by lack of built-in exponentials.
3) Syntactic functoriality of formulas: The reduction rule for the (µ-fold)/(ν-rec) cut requires the possibility of substituting a proof for a propositional variable in a formula. More precisely, let (ζ, ξ 1 , . . . , ξ k ) be a list of pairwise distinct propositional variables containing all the free variables of a formula F and let C = (C 1 , . . . , C k ) be a sequence of closed formulas. Let π be a proof of ⊢ ?Γ, A ⊥ , B, then one defines 14 a proof F π/ζ, C/ ξ of ⊢ ?Γ, (F A/ζ, C/ ξ ) ⊥ , F B/ζ, C/ ξ by induction on F , adapting the corresponding definition in [4]. We illustrate this definition by two inductive steps. Observe, in these examples, how the exchange rule is used implicitly.
Assume first that F = µξ G (so that (ζ, ξ, ξ 1 , . . . , ξ k ) is a list of pairwise distinct variables containing all free variables of G). Let G ′ = G C/ ξ whose only possible free variables are ζ and ξ. The proof F π/ζ, C/ ξ is defined by Notice that this case uses the additional parameters C in the definition of this substitution with k + 1 parameters in the inductive hypothesis. To see that the last inference in this deduction is an instance of (ν-rec ′ ), set H = G ′⊥ A ⊥ /ζ and notice that 14 Again the fact that the formulas of the context bear a ? is absolutely necessary to make this definition possible.
Observe that we use in an essential way the fact that all formulas of the context are of shape ?H (even if F is exponential-free) when we apply contraction rules on this context.

4) Cut elimination:
The only reduction that we will mention here is (µ-fold)/(ν-rec). Let θ be Then θ reduces to the proof shown in Figure 2. This reduction rule uses the functoriality of formulas as well as the ?-contexts in the (ν-rec) rule.
Remark 7. In [4] it is shown that µMALL enjoys cutelimination. We will show in a further paper how this method based on reducibility can be adapted to our µLL. Notice that a cut-free proof has not the sub-formula property in general because of rule (ν-rec). Though, the normalization theorem makes sure that a proof of a sequent which does not contain any ν-formula reduces to a cut-free proof enjoying the subformula property.

5) Interpreting formulas and proofs (outline):
We assume to be given a µLL Seely model (L, L), see Section II-F. With any formula A and any repetition-free sequence ζ = (ζ 1 , . . . , ζ k ) of type variables containing all the free variables of A, we associate A ζ ∈ L k in the obvious way, for instance A ⊗ B ζ = ⊗ • ( A ζ , B ζ ) ∈ L k by conditions (4) and (3) in Definition 7 and νζ A ζ = ν( A ζ ,ζ ) using condition (5).
up to a natural isomorphism. In this outline, we keep symmetric monoidality isomorphisms of L and of ! implicit (see for instance [36] how monoidal trees allow to take them into account). With any Γ = (A 1 , . . . , A n ) we associate an object Γ of L and with any proof π of ⊢ Γ we associate a morphism π ∈ L(1, Γ ) using the categorical constructs of L in a straightforward way, see [7]. Then one proves that if π and π ′ are proofs of ⊢ Γ and π reduces to π ′ by the cut-elimination rules, then π = π ′ . This is done by an inspection of the various cut-elimination rules. In the case of (µ-fold)/(ν-rec) cut-elimination, we need the following lemma.
Lemma 8. Let Γ = (D 1 , . . . , D n ) be a sequence of closed formulas and let P = ! D 1 ⊗ · · · ⊗ ! D n , considered as an object of L ! . Let F be a formula and ζ, ξ 1 , . . . , ξ k be a repetition-free list of variables containing all the free variables of F so that F = F ζ, ξ is a strong functor L k+1 → L which belongs to L k . As shown in Section II-D this strong functor lifts to a functor F  The proof of the lemma is a simple verification. Notice that we use the fact that the objects of L[P ] are the same as those of L.

III. SETS AND RELATIONS
The category Rel has sets as objects, and given sets E and F , Rel(E, F ) = P(E × F ). Identity is the diagonal relation and composition is the usual composition of relations, denoted by simple juxtaposition. If t ∈ Rel(E, F ) and u ⊆ E then t · u = {b ∈ F | ∃a ∈ u (a, b) ∈ t}.

A. Rel as a model of LL.
This category is a well-known model of LL in which As to the additives, 0 = ⊤ = ∅ and &i∈I E i = ⊕ i∈I E i = i∈I {i} × E i . The exponentials are given by !E = ?E = M fin (E) (finite multisets of elements of E which are functions m : E → N such that m(a) = 0 for finitely many a's; addition of multisets is defined in the obvious pointwise way, and [a 1 , . . . , a k ] is the multiset which maps a to the number of i's such that a i = a). For the additives and multiplicatives, the operations on morphisms are defined in the obvious way. Let us be more specific about the exponentials. Given s ∈ Rel(E, F ),

B. Locally continuous functors on Rel
The following considerations on continuity of functors are standard, see [37]. A functor F : Rel n → Rel is locally continuous if, for all E, F ∈ Rel n and all directed set D ⊆ Rel n ( E, F ), one has F( D) = {F( s) | s ∈ D} (we use D for the component-wise union). This implies in particular that if s ⊆ t, one has F( s) ⊆ F( t) (taking D = s, t ). To simplify notations assume that n = 1 (but what follows holds for all values of n).

Lemma 9. Let E and F be sets and let s ∈ Rel(E, F ) and t ∈ Rel(F, E). Assume that t s = Id E and that s t ⊆ Id F . Then s is (the graph of) an injective function and
Lemma 10. Let F : Rel → Rel be a locally continuous functor. Assume that E ⊆ F and let η + Let Rel ⊆ be the category whose objects are sets and morphisms are set inclusions (so that Rel ⊆ (E, F ) has η + E,F as unique element if E ⊆ F and is empty otherwise). Then η + can be thought of as the "inclusion functor" Rel ⊆ → Rel, acting as the identity on objects. Obviously, Rel ⊆ is cocomplete 15 .
Proposition 11. If F : Rel → Rel is locally continuous then F η + : Rel ⊆ → Rel is directed-cocontinuous (that is, preserves the colimits of directed sets of sets).
The proof can be found in [37]. We know that a locally continuous functor F maps inclusions to injections, we shall say that F is strict if it maps inclusions to inclusions, that is, if . As a direct consequence of Proposition 11, we get: Lemma 12. If F is strict locally continuous then, for any directed set of sets D, one has F( D) = E∈D F(E).

C. Variable sets and basic constructions on them
Definition 13. An n-ary variable set is a strong functor V : Rel n → Rel such that V is locally continuous and strict.
By the general considerations of Section II-D, there is a constant strong functor Rel n → Rel with value E for each set E. There are projection strong functors Rel n → Rel, × (that is ⊗) and + (that is ⊕) define strong functors Rel 2 → Rel, M fin ( ) (that is ! ) defines a strong functor Rel → Rel. Strong functors on Rel are stable under composition, and if V is a strong functor Rel n → Rel then there is a "dual" strong functor V ⊥ (which is actually identical to V in this very simple model). To check that these strong functors V are variable sets we have only to check that the underlying functors V are strict locally continuous.
We deal with ! and composition, the other cases are similar. We already defined the functor 16 a pair ([a 1 , . . . , a k ], [b 1 . . , k and the inclusion follows. Strictness is obvious. Let V i : Rel n → Rel be variable sets for i = 1, . . . , k and let W : Rel k → Rel be a variable set. Then the functor W • V : Rel n → Rel is clearly strict locally continuous (since these conditions are preservation properties) from which it follows that the strong functor U = W • V is a variable type.
1) Fixed point of a variable set: Let F : Rel → Rel be a strict locally continuous functor. Since ∅ ⊆ F(∅) we have F n (∅) ⊆ F n+1 (∅) for all n ∈ N, by induction on n and hence F( Notice that (σF, Id) is also an initial object in Alg Rel (F). When we insist on considering σF as a final coalgebra, we denote it as νF.
Lemma 15. Let F : Rel n+1 → Rel be a strict locally continuous functor. The functor νF : Rel n → Rel is strict locally continuous.
Let V : Rel n+1 → Rel be a variable set, by Lemma 5, there is a unique strong functor νV : Rel n → Rel which is characterized by: νV( E) = νV E , for each s ∈ Rel n ( E, F ), νV( s) = V( s, νV( s)) and last V(

Lemma 16. The functor νV is a variable set.
Proof: By the conditions above satisfied by νV we have that νV = νV and hence νV is strict locally continuous by Lemma 15. 2) A model of µLL based on variable sets: Let Rel n be the class of all n-ary variable sets, so that Rel 0 = Obj(Rel). The fact that (Rel, (Rel n ) n∈N ) is a Seely model of µLL in the sense of Definition 7 results mainly from the fact that we take all variable sets in the Rel n 's so that there is essentially nothing to check. More explicitly: (1) holds by Section III-A, (2) holds by construction, (3) holds by the fact that variable sets compose as explained in Section III-C (notice that this condition refers to the general composition of strong functors defined at the beginning of Section II-D1), (4) holds by Section III-C and by the fact that the De Morgan dual of a strong functor is strong, see Section II-D1 and (5) holds by Lemma 16.

IV. NON-UNIFORM TOTALITY SPACES
We enrich the model of Section III with a notion of totality, we use notations from that section for operations on sets and relations.

A. Basic definitions.
Let E be a set and let T ⊆ P(E). We define We also have T ⊆ T ⊥⊥ and therefore T ⊥⊥⊥ = T ⊥ . The biorthogonal closure has a nice and simple characterization.
We define the category Nuts whose objects are the NUTS and Nuts(X, Y ) = T (X ⊸ Y ), composition being defined as the usual composition in Rel (relational composition) and identities as the diagonal relations. Lemma 19 shows that we have indeed defined a category.

1) Multiplicative structure:
Lemma 20. Let X and Y be NUTS and t ∈ Nuts(X, Y ). Then t is an iso in Nuts iff t is (the graph of) a bijection |X| → |Y | such that ∀u ⊆ |X| u ∈ T (X) ⇔ t(u) ∈ T (Y ).
Proof: This is an obvious consequence of Lemma 19 and of the fact that ( We turn now ⊗ into a functor, its action on morphisms being defined as in Rel. Let t i ∈ Nuts(X i , Y i ) for i = 1, 2, we have t 1 ⊗ t 2 ∈ Nuts(X 1 ⊗ X 2 , Y 1 ⊗ Y 2 ) by Lemma 22 and by the equation (t 1 ⊗ t 2 ) · (u 1 ⊗ u 2 ) = (t 1 · u 1 ) ⊗ (t 2 · u 2 ). This functor is monoidal, with unit 1 and symmetric monoidality isomorphisms λ, ρ, γ and α defined as in Rel. The only nontrivial thing to check is that α is indeed a morphism, namely α |X1|,|X2|,|X3| ∈ Nuts((X 1 ⊗ X 2 ) ⊗ X 3 , X 1 ⊗ (X 2 ⊗ X 3 )). This results from Lemma 23 and from the observation that The SMC category Nuts is closed, with X ⊸ Y as internal hom object from X to Y , and evaluation morphism ev = { (((a, b), a), b | a ∈ |X| and b ∈ |Y |} which indeed belongs to Nuts((X ⊸ Y ) ⊗ X, Y ) by Lemma 22 since, for all t ∈ T (X ⊸ Y ) and u ∈ T (X) we have ev (t ⊗ u) = t u ∈ T (Y ). This category Nuts is also * -autonomous with dualizing object ⊥ = 1.
2) Additive structure: Let (X i ) i∈I be an at most countable family of objects of Nuts. We define X = &i∈I X i by: |X| = i∈I {i} × |X i | and T (X) = {u ⊆ |X| | ∀i ∈ I π i · u ∈ T (X i )} where π i = {((i, a), a) | a ∈ |X i |}. It is clear that T (X) = ↑T (X) and hence X is an object of Nuts. By definition of X and by Lemma 19 we have ∀i ∈ I π i ∈ Nuts(X, X i ). Given t = (t i ) i∈I with ∀i ∈ I t i ∈ Nuts(Y, X i ), we have t ∈ Nuts(Y, X) as easily checked (using Lemma 19 again). It follows that (& i∈I X i , (π i ) i∈I ) is the cartesian product of the X i 's in Nuts. This shows that the category Nuts has all countable products and hence is cartesian. Since it is * -autonomous, the category Nuts is also cocartesian, coproduct being given by as easily checked. Notice that the final object is ⊤ = (∅, {∅}) and that 0 = ⊤ ⊥ = (∅, ∅).
To prove that Nuts is a categorical model of LL, it suffices to show that the various relational morphisms defining the strong symmetric monoidal monadic structure of ! in Rel (see Section III-A) are actually morphisms in Nuts. This is essentially straightforward and based on Lemma 24.
Lemma 27. Equipped with der, dig, m 0 and m 2 defined as in Rel, ! is a symmetric monoidal comonad which turns Nuts into a Seely model of LL.

B. Variable non-uniform totality spaces (VNUTS)
Let E be a set, we use Tot(E) for the set of all totality candidates on E, that is, of all subsets T of P(E) such that T = T ⊥⊥ . In other words T ∈ Tot(E) means that T = ↑T by Lemma 17. Ordered by ⊆, this set Tot(E) is a complete lattice.
We need now to define a notion of strong functors X : Nuts n → Nuts for defining a model in the sense of Definition 7. One crucial feature of such a functor will be that |X ( X)| depends only on | X|. Definition 28. Let n ∈ N, an n-ary VNUTS is a pair X = (|X|, T (X)) where |X| : Rel n → Rel is a variable set |X| = (|X|, |X|) (see Section III-C2) and T (X) is an operation which with each n-tuple X of objects of Nuts associates an element T (X)( X) of Tot(|X|(| X|)) in such a way that 1 for any t ∈ Nuts n ( X, Y ), the element |X|( t) of Rel(|X|(| X|), |X|(| Y |)) belongs to Nuts(X( X), X( Y )) (where X( X) denotes the NUTS (|X|(| X|), T (X)( X)) 2 and for any Y ∈ Obj(Nuts n ) and any X ∈ Obj(Nuts) one has |X| |X|,| Y | ∈ Nuts(!X ⊗ X( Y ), X(!X ⊗ Y )). In other words, for an u ∈ T (X) and v ∈ Tot(X)( Y ), one has Lemma 29. Any VNUTS X : Nuts n → Nuts induces a strong functor X : Nuts n → Nuts which satisfies • and X X, Y = |X| |X|,| Y | and the correspondence X → X is injective.
Proof: It is clear that X so defined is a strong functor. Let us check that X can be retrieved from X . Given a set E, (E, P(E)) is a NUTS that we denote as p(E). Notice that p can be extended into a functor Rel → Nuts which acts as the identity on morphisms. There is also a forgetful functor u : Nuts → Rel which maps X to |X| and acts as the identity on morphisms (p is right adjoint to u). Let X be a unary VNUTS and let X : Nuts → Nuts be the associated strong functor. Then we have |X| = u • X • p and |X| E,F = X p(E),p(F ) for any sets E and F . Last, given a NUTS X, we have that T (X)(X) is just the totality component of the NUTS X (X). This shows that the VNUTS which induces X can be retrieved from X .
For this reason we use X to denote the functor X .
Remark 8. Another possibility would be to define a VNUTS at the first place as a strong functor X : Nuts n → Nuts satisfying additional properties whose purpose would be to make the definition of the underlying X possible. This option, suggested by the reviewers, will be explored further. It is crucial to notice that these additional properties (that is, the existence of X) are crucial in the proof of Theorem 30. In particular, it is essential that |X (X)| depends only on |X|.
Given n ∈ N let Vnuts n be the class of strong n-ary VNUTS. We identify Vnuts 0 with the class of objects of the Seely category Nuts. The following refers to Definition 7 Then we have Id ∈ Nuts((E, S 1 ), (E, S 2 )) and therefore, by Condition (1) satisfied by X, we have Id = |X|(Id) ∈ Nuts(X(E, S 1 ), X(E, S 2 )) = Nuts((E, Φ(S 1 )), (E, Φ(S 2 )) which means that Φ(S 1 ) ⊆ Φ(S 2 ). By the Knaster Tarski Theorem (remember that Tot(E) is a complete lattice), Φ has a greatest fixpoint T that we can describe as follows. Let (T α ) α∈O , where O is the class of ordinals, be defined by: T 0 = P(E) (the largest possible notion of totality on E), T α+1 = Φ(T α ) and T λ = α<λ T α when λ is a limit ordinal. This sequence is decreasing (easy induction on ordinals using the monotonicity of Φ) and there is an ordinal θ such that T θ+1 = T θ (by a cardinality argument; we can assume that θ is the least such ordinal). The greatest fixpoint of Φ is then T θ as easily checked. By construction ((E, T θ ), Id) is an object of Coalg Nuts (X), we prove that it is the final object. So let (Y, t) be another object of the same category. Since (|Y |, t) is an object of Coalg Rel (|X|) and since (E, Id) is the final object in that category, we know by Lemma 14 that there is exactly one e ∈ Rel(|Y |, E) such that |X|(e) t = e. We prove that actually e ∈ Nuts(Y, (E, T θ )) so let v ∈ T (Y ). We prove by induction on the ordinal α that e · v ∈ T α . For α = 0 it is obvious since T 0 = P(E). Assume that the property holds for α and let us prove it for α + 1. We have t·v ∈ T (X)(Y ) = T (X(Y )) since t ∈ Nuts(Y, X(Y )). Since X(e) ∈ Nuts(X(Y ), X(E, T α )) and X(E, T α ) = (E, T α+1 ) we have (X(e) t) · v ∈ T α+1 , that is e · v ∈ T α+1 . Last if λ is a limit ordinal and if we assume ∀α < λ e · v ∈ T α we have e · v ∈ α<λ T α = T λ . Therefore e · v ∈ T θ . We use νX to denote this final coalgebra (E, T θ ) (its definition depends only on X and does not involve the strength X).
So we have proven the first part of Condition (5) in the definition of a Seely model of µLL (see Section 7). As to the second part, let X be an n + 1-ary VNUTS. We know by the general Lemma 5 how to build a strong functor νX : Nuts n → Nuts with suitable properties. To end the proof, it suffices to exhibit an n-ary VNUTS Y = (|Y|, T (Y)) whose associated strong functor coincides with νX. The construction of Y is essentially straightforward, using the constructions available in Rel.
Remark 9. For any closed formula A, the web of its interpretation A Nuts in Nuts coincides with its interpretation A Rel in Rel. It is also easy to check that for any proof π of ⊢ A, one has π Nuts = π Rel (this can be formalized using the functor u : Nuts → Rel introduced in the proof of Lemma 29, which acts trivially on morphisms).
Remark 10. The same method can be applied in many contexts. For instance, we can replace Rel with the category of coherence spaces -where least and greatest fixpoints are interpreted in the same way -and Nuts with the category of coherence spaces with totality where the interpretations will be different. One of the reviewers suggested that this situation might be generalized using the concept of topological functors, this option will be explored in further work.
Using an additional notion of coherence (which can be fully compatible with Rel as in the non-uniform coherence space models of [13], [14]) we can also prove that π Rel has at most one element, and hence is a singleton {n}. This is a denotational version of normalization expressing that indeed π "has a value" (and actually exactly one, which expresses a weak form of confluence).

3) An empty type of streams of integers:
After reading [6], one could be tempted to define the type of streams of integers as σ 0 = νζ (ι ⊗ ζ). The variable set ι ⊗ ζ Rel ζ : Rel → Rel maps a set E to N × E. The least fixed point of this operation on sets is ∅ and hence | σ Nuts | = ∅ and notice that Tot(∅) = {∅, {∅}}. In that case, the operation Φ : Tot(∅) → Tot(∅) maps T to {u × v | v ∈ T and u ∈ P(N) \ {∅}} and hence {∅} to itself. It follows that T ( σ 0 Nuts ) = {∅} that is σ 0 Nuts = ⊤, the final object of Nuts. What is the meaning of this trivial interpretation? It simply reflects that, though σ 0 has a lot of non trivial proofs in µLL, it is impossible to extract any finite information from these proofs within µLL, and accordingly all these proofs are interpreted as ∅.
Theorem 32. In µLL, there is no proof of ⊢ σ ⊥ 0 , ι. In other words there is no proof of ⊢ σ 0 ⊸ ι in µLL; typically a function extracting the first element of a stream would be a proof of this type. . . if it would exist! Here is the argument: if π were a proof of ⊢ σ ⊥ 0 , ι, we would have π ∈ Nuts( σ 0 Nuts , ι Nuts ) and hence π · ∅ ∈ T ( ι Nuts ) which is not the case since π · ∅ = ∅. If types like σ 0 are meaningful in a proof-search perspective, their relevance as data-types in a Curry-Howard approach to µLL is dubious.

4) A non-empty type of streams of integers:
We set now σ = νζ (1 & (ι ⊗ ζ)). This type looks like the previous one, but the type 1 leaves space for partial empty streams. Warning: it is not a type of finite or infinite streams; the & means that this empty stream will not be a total element: it will have to be complemented by some total element from the right argument of the &. More precisely 1 & (N ⊗ ζ) Rel ζ : Rel → Rel is the variable set which maps a set E to {(1, * )} ∪ {2} × N × E so that up to renaming | σ Nuts | = N <ω (all finite sequences of integers). In this case, the operator Φ : where we use () for the empty sequence. So for instance Φ 0 (P(N <ω )) = P(N <ω ) Φ 1 (P(N <ω )) = u ∈ P(N <ω ) | () ∈ u Φ 3 (P(N <ω )) = u ∈ P(N <ω ) | ∃n 1 , n 2 (), (n 1 ), (n 1 , n 2 ) ∈ u .
The greatest fixed point is reached in ω steps: So a total subset of | σ Nuts | must contain (at least) an infinite stream of integer. For this type of streams σ it is easy to build a proof of ⊢ σ ⊥ , ι extracting the first element of a stream, interpreted as {((n), n) | n ∈ N}.

V. CONCLUSION AND FURTHER WORK
We will study next the semantics of infinite proofs of µLL (whose definition extends that of [6] for µMALL). A crucial step is to prove that these infinite proofs can be interpreted as total sets in Nuts, this will be presented in a further paper. This interpretation of proofs is based on the interpretation of their finite approximations in Rel (remember that the interpretations of a µLL proof in Nuts and in Rel are exactly the same set).
Our models will also serve as guidelines for the design of a functional language based on µLL, generalizing Gödel's System T in the spirit of [22] though, as explained in the Introduction, Loader's syntax is not fully compatible with LL as it is based on cocartesian cartesian closed categories. Our system will primarily implement Park's rule, but we will also consider other options based on polymorphism in the spirit of [38], [19] or [39], or general recursion with guardedness restrictions as in [25], [26], [27].
Its syntax will be based on the idea of representing datatypes as positive formulas of µLL interpreted in L ! and therefore equipped with morphisms implementing weakening, contraction and promotion: as noticed in [4], µζ is a positive operation whereas νζ is negative. In L ! , the ⊕ of LL is a coproduct and the ⊗ is a cartesian product as expected (and ⊗ distributes over ⊕). The targeted calculus will feature a notion of values (positive terms) accounting for the morphisms of L ! , substitution in terms being allowed only for values because only them can safely be discarded and duplicated. Thanks to this choice of design, weakening and contraction will remain implicit operations as in the usual λ-calculus. Our calculus will have explicit promotion and dereliction operations, allowing to implement both CBN and CBV in the same setting, just as in Levy's Call-by-push-value [40], [41].
We thank the reviewers of this paper for their careful reading and very useful suggestions. This work was partly funded by the ANR project PPS, ANR-19-CE48-0014. This paper is a preprint version of an article published at LICS'21.

B. Proof of Lemma 5
Proof: The part of the statement which concerns the functor νF is a direct application of Lemma 4 so we only have to deal with the strength. Let us prove naturality so let f ∈ L n ( X, X ′ ) and g ∈ L(Y, Y ′ ), we must prove that the following diagram commutes Let h 1 = νF Y ′ , X ′ (!g ⊗νF( f )) and h 2 = νF(!g ⊗ f ) νF Y, X be the two morphisms we must prove equal. We use Lemma 3, taking the following morphism l.

C. Proof of Lemma 9
Proof: Let a ∈ E, since (a, a) ∈ Id E = t s, there must exist b ∈ F such that (a, b) ∈ s and (b, a) ∈ t. If (a, b ′ ) ∈ s then (b, b ′ ) ∈ s t ⊆ Id F and hence b ′ = b. It follows that s is a total function E → F . Let (a, b) ∈ s (that is a ∈ E and b = s(a)). Since t s = Id E , we must have (b, a) ∈ t. Conversely let (b, a) ∈ t, we have (b, s(a)) ∈ s t and hence b = s(a). We have proven that t = {(s(a), a) | a ∈ E}. If a, a ′ ∈ satisfy s(a) = s(a ′ ) we have therefore (a, a ′ ) ∈ t s = Id E and hence a = a ′ ; this shows that s is injective.

D. Proof of Lemma 14
Proof: Let (E, t) be an F-coalgebra. We define a sequence e n ∈ Rel(E, σF) as follows: e 0 = ∅ and e n+1 = F(e n ) t. Then e n ⊆ e n+1 for all n by an easy induction, using the fact that F is locally continuous. Let e = ∞ n=0 e n ∈ Rel(E, σF), by local continuity of F we have F(e) t = ( ∞ n=0 F(e n )) t = ∞ n=0 (F(e n ) t) = ∞ n=0 e n+1 = e which means that e ∈ Coalg Rel (F)((E, t), (σF, Id)) .
We end the proof by showing that e is the unique such morphism, so let e ′ ∈ Coalg Rel (F)((E, t), (σF, Id)) which means that e ′ ∈ Rel(E, σF) and F(e ′ ) t = e ′ . Let i n ∈ Rel(σF, σF) be defined by induction by i 0 = ∅ and i n+1 = F(i n ). Then (i n ) n∈N is monotone and ∞ n=0 i n = Id by definition of σF. We prove by induction on n that ∀n ∈ N i n e ′ = i n e. Clearly i 0 e ′ = i 0 e = ∅. Next i n+1 e ′ = F(i n ) F(e ′ ) t = F(i n e ′ ) t = F(i n e) t by inductive hypothesis = i n+1 e . Therefore e ′ = n∈N i n e ′ = n∈N (i n e ′ ) = n∈N (i n e) = e.

E. Proof of Proposition 11
Proof: Let D be a directed set of sets and let H be a set. For each E ∈ D let s E ∈ Rel(F(E), H) so that (s E ) E∈D defines a cocone, that is, for each E, F ∈ D such that E ⊆ F , one has s E = s F F(η + E,F ). Let L = D. Let s ∈ Rel(F(L), H) be given by s = E∈D s E F(η − E,L ). Let E ∈ D, we have s F(η + E,L ) = F ∈D s F F(η − F,L η + E,L ) so that s E ⊆ s F(η + E,L ) (since s F F(η − F,L η + E,L ) = s E when F = E). We prove the converse inclusion. Let F ∈ D and let G ∈ D be such that E, F ⊆ G (remember that D is directed). We have where we have used the fact that η + F,G η − F,G ⊆ Id G and hence F(η + F,G η − F,G ) ⊆ Id F(G) by local continuity of F. So s F F(η − F,L η + E,L ) ⊆ s E for all F ∈ D and hence s F(η + E,L ) ⊆ s E as contended. Let now s ′ ∈ Rel(F(L), H) be such that s ′ F(η + E,L ) = s E for each E ∈ D, we show that s ′ = s thus proving the uniqueness part of the universal property. For E ∈ D, let θ E = η + E,L η − E,L ∈ Rel(L, L). Then (θ E ) E∈D is a directed family (for ⊆) and E∈D θ E = Id L . By local continuity of F, we have by our assumption on s ′ and by definition of s. This shows that the cocone (F(η + E,L )) E∈D on F η + is colimiting, thus proving that F η + is directed cocontinuous.

F. Proof of Lemma 15
Proof: As usual we assume that n = 1 to increase readability. We need to prove first that νF is monotone on morphisms, so let s, t ∈ Rel(E, F ) with s ⊆ t. We have νF(s) = n∈N s n and νF(t) = n∈N t n with s 0 = t 0 = ∅, s n+1 = F(s, s n ) and t n+1 = F(t, t n ) (we use the action of νF on morphisms resulting from Lemma 4 and from the characterization of the morphisms to the final object given in the proof of Lemma 14). By induction and hommonotonicity of F we have ∀n ∈ N s n ⊆ t n and hence νF(s) ⊆ νF(t). Let us prove now local continuity so let D ⊆ Rel(E, F ) be directed and let t = D, we prove that νF(t) = s∈D νF(s) ∈ Rel(νF(E), νF(F )) using Lemma 3 (with the notations of that lemma, we take l = F(t, νF(E))). We have  In the second equation, we used the facts that D is directed and the monotonicity of F and νF on morphisms.