Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
David Corfield asked in another thread:
What is this ’focusing’?
Good question. It’s originally an idea for speeding up goal-directed proof search in the sequent calculus for linear logic, by restricting the application of rules based on observations about the polarity of connectives. I see that you’ve already added a few good references to focusing which explain this idea, including Andreoli’s original article and Rob Simmons’ Structural Focalization.
I’ve spent some time thinking about what focusing means from a categorical perspective, and this was one of the motivations for my ongoing collaboration with Paul-André Melliès on the categorical semantics of “type refinement systems”. That’s lead us in various directions and we’ve kind of put these proof-theoretic questions to the side for a while, but one of our early intuitions was that focusing has to do with taking a presheaf interpretation of formulas, and adding some kind of criterion of representability for those presheaves. This idea is developed to some extent in our paper An Isbell Duality Theorem for Type Refinement Systems – see in particular the high-level discussion in the (recently revised) introduction, although we don’t try to give a detailed analysis of focusing.
Thanks! I just looked at your other article A bifibrational reconstruction of Lawvere’s presheaf hyperdoctrine and see that Peirce’s existential graphs appear.
I’m always pleased to see them revived. I notice you refer to Mike’s ’Framed bicategories and monoidal fibrations’, but did you know that a development of Peirce’s graphs feature in ’Duality and traces in indexed monoidal categories’ with Kate Ponto, after a discussion here?
In A bifibrational reconstruction of Lawvere’s presheaf hyperdoctrine, one motivation is to understand why we have
when conjunction is a dependent sum and implication is a dependent product.
It is thus puzzling to see conjunction and implication directly coupled by an adjunction in (1) while they form in (2) a “ménage à trois” with the substitution functor as intermediate.
It is resolved (p. 7) by finding two forms of which allows the triple to be seen as two adjunctions between and .
Would it be useful to relate this to Wirthmüller context:
systems of Wirthmüller contexts are generalizations of categorical logic (hyperdoctrines) to non-cartesian contexts.
Thanks very much for your interest in our more recent paper on the presheaf hyperdoctrine.
Would it be useful to relate this to Wirthmüller context[?]
I think it would definitely be useful, and also to relate our approach to six operations. I know that Paul-André is interested in making such a comparison, though personally I am not yet familiar enough with the original context for these, so I am afraid of saying too much nonsense.
I could perhaps say a bit about the subtle relation between the approach in “a bifibrational reconstruction” and the idea of an indexed (closed) monoidal category, which is mentioned in the nlab article dependent linear type theory. The key models we consider in this paper ( and ) are not indexed (closed) monoidal categories in this sense, since the tensor product on the total categories does not preserve cartesian arrows. However, the usual (cartesian) closed monoidal structure on presheaves (and subsets) can instead be derived through a bifibrational version of the Day construction (p.17), using the fact that every category is a comonoid in and hence by the contravariant embedding functor induces a monoid in .
did you know that a development of Peirce’s graphs feature in ’Duality and traces in indexed monoidal categories’ with Kate Ponto, after a discussion here?
I’ve seen that paper mentioned on the nlab before but haven’t studied it carefully yet. I think that the “string diagrams for objects” are similar, except that we also include Peirce’s “sep” lines representing the dualization functors (coming from the structure of as a “bifibration chirality”), which is definitely inspired by Section 5 of Brady & Trimble’s “A string diagram calculus for predicate logic”.
Re: #4, I would have said the answer is that when and are considered as endofunctors, that means they’re actually composites of two functors, and .
Mike #6, of course one can prove that when is defined as and is defined as and . The sentence that David quoted above from the introduction of our article was pointing out a different, more philosophical question: why does the treatment of existential and universal quantification in a hyperdoctrine seem to require the “intermediary” of substitution, when conjunction is directly coupled to implication in a closed category? And the question is rhetorical in the sense that the point of the article is really to explore a more symmetric treatment of quantification – at least for the specific case of presheaves – by embedding the presheaf hyperdoctrine into the monoidal closed bifibration , which it turns out has a lot of interesting properties.
ok, sure
Noam, have you also looked to -ify things, i.e., ? We seem to persist in calling them ’profunctors’, even when going beyond as target.
Urs has been doing swathes of higher linear algebra in this setting, as at integral transforms on sheaves, but also in papers, such as Quantization via Linear homotopy types.
We have Pr(infinity,1)Cat as -analogue of . I can’t recall seeing what would be , though there’s plenty of uses of pointedness in all this higher linear algebra, linear homotopy type theory.
Noam, have you also looked to -ify things, i.e., ?
The short answer is no, we have not gone down that path yet. The longer answer is that we’re interested in higher dimensions, but the approach we’ve been developing for modelling type refinement systems is naturally oriented rather than groupoidal, so moving to higher dimensions requires some care. For example, Paul-André and I have previously explained how any type refinement system modelled as a functor induces a directed notion of subtyping that validates the subsumption rule
described at coercion, but rather taking an “à la Curry” interpretation of subtyping instead of the coercion view. You may also have noticed that the “bifibrational reconstruction” article introduces a directed notion of identity predicate in a monoidal closed bifibration, which reduces to in the presheaf hyperdoctrine. In fact, the presheaf hyperdoctrine is unusual from the perspective of traditional categorical logic (although it was introduced in Lawvere’s original articles) since it fails to satisfy the “necessary” Frobenius reciprocity and Beck-Chevalley conditions, yet we view the monoidal closed bifibration as a fundamental example of a type refinement system. So all of these points are slight departures from the usual story about dependent type theory and the more recent one about homotopy type theory, but we think they are well-motivated and would like to understand the practical consequences.
With some free time coming into view at last, I should look into this perspective. Zhaohui Luo, whose account of coercion is at coercion, is coming to Kent for a workshop in June, so interesting to contrast.
If only to remind myself, there’s something I’d like to understand about where Wirthmüller context meets Frobenius reciprocity, and then how that the latter fails in the presheaf hyperdoctrine.
By the way, are you related to Doron Zeilberger? We were at a Thales and Friends event together once.
If only to remind myself, there’s something I’d like to understand about where Wirthmüller context meets Frobenius reciprocity, and then how that the latter fails in the presheaf hyperdoctrine.
The point is that the canonical natural transformation
need not be an isomorphism, where here is a functor, are presheaves, the pullback functor is being interpreted as precomposition and as the cartesian closed structure on the presheaf categories and . Lawvere gives a counterexample on p.7 of (Lawvere 1970), for the constant functor into the interval category which sends the point to 1. (He then notes that Frobenius Reciprocity holds if one restricts to presheaves over groupoids, but the BC condition fails even in the groupoidal case (p.11).)
In our analysis of the presheaf hyperdoctrine via the monoidal closed bifibration , we view the cartesian closed structure on the fibers as a special case of the monoidal closed structure on which can be derived from any promonoidal structure on . In general, if is a homomorphism between two monoids in the base category of a monoidal closed bifibration , and are two objects lying over , then there is a canonical morphism
but it need not be an isomorphism.
By the way, are you related to Doron Zeilberger?
Yes, he is my uncle!
Thanks.
And also when I have a moment, is there a connection between the functors as type refinement systems idea, and the modal additions to HoTT we like around here, such as in real-cohesive homotopy type theory.
Just starting to look at the “bifibrational reconstruction” paper. I have not yet delved very deeply into it, but on first glance I wonder whether what you’re trying to do would be more naturally formulated in the language of proarrow equipments, since they (unlike ordinary bifibrations) are designed to deal with the “two-sidedness” of profunctors. Did you consider that?
I think you might get a better sense of what we’re trying to do after reading a bit more of the paper, because we do implicitly make great use of the structure of () as a proarrow equipment, in particular the fact that every functor (function) induces an adjoint pair of distributors (relations). The key insight of the paper is to consider the additional structure of a monoidal closed bifibration over (), which allows us to recover the ordinary Lawvere quantifiers (where is a functor/function) from more general “relational quantifiers” (where is a distributor/relation) directly corresponding to the push and pull operations of a bifibration.
I did see that. But I don’t think of those quantifiers as “extra structure” but as part of the equipment – aren’t they just composites and homs in the bicategory Dist? Maybe what I’m saying is just that it’s weird to me that the presence of the equipment is only implicit rather than explicit, since the equipment language seems to me to be the natural one in which to describe the relationship of composites and homs with restriction and extension. To me, the reason the ’presheaf hyperdoctrine’ looks weird from a hyperdoctrine perspective is that it’s really an equipment.
Relatedly, I’m not convinced by these “chiralities”. What good does it do to introduce another name for so you can use a misleading notation for the internal-hom that makes it look like a tensor product?
Sorry, that last sentence was too harshly worded. (-:O I do see the potential value in regarding the internal-hom as an “action” of on C; the part that seems misleading to me is to notate that action with an overloaded tensor or disjunction symbol.
But I don’t think of those quantifiers as “extra structure” but as part of the equipment – aren’t they just composites and homs in the bicategory Dist?
The pushforward and pullback operations for the bifibration indeed correspond to special cases of composition and right kan lifting in seen as a bicategory, but the point is that we can get a lot done simply by working with as a (monoidal closed) bifibration, without trying to axiomatize all the structure of the base as a bicategory. I already mentioned a couple examples of this (from the paper) which I think are nice, for instance, the fact that any promonoidal structure on a category induces a closed monoidal structure on can be derived as an instance of the more general fact that if is a monoid in the base of a monoidal closed bifibration , then its fiber is monoidal closed. Do you think there is a better way of explaining this fact?
Relatedly, I’m not convinced by these “chiralities”.
They definitely take some getting used to. One of Paul-André’s original motivations for the notion was to give a categorical explanation of polarized linear logic, which separates positive and negative formulas into two syntactic categories, and which can also initially feel like just a “misleading notation”. Chiralities entered into the story of this paper organically (to our surprise) in the form of “bifibration chiralities”, and I think that they are a quite natural way of describing the duality between and . The string diagram calculus à la Peirce basically fell out from this way of looking at co- and contravariant presheaves.
Okay, now I had a chance to look at this paper more carefully, and I see that there is neat stuff in it! If I may, let me rephrase what I got from the paper from my perspective and background, and you can tell me what I missed.
Firstly, one may observe that many fibrations are not just bifibrations but also what are sometimes called -fibrations, where the pullback functors have both left and right adjoints. Unfortunately, the right adjoints annoyingly don’t have as nice a fibrational representation as the left adjoints. But — as also appeared in the adjoint logic representation of cohesion — an adjoint triple is equivalently an adjoint pair of adjunctions, so we can represent such a “-bifibration” as a bifibration over a bicategory in which our original base category has been embedded with each morphism giving rise to an adjunction, such as Cat in Dist, or Set in Rel or Span.
I had forgotten, but now I remember noticing this back when I was mucking around with fibrations as a grad student, doing the stuff that eventually led to my paper on framed bicategories. It’s cute among other reasons because the Beck-Chevalley conditions that hold in the original fibration get encoded as commutativity relations between adjoints in the bicategorical version, e.g. the BC condition for all pullback squares is appropriate for Span, since composition there is by pullback, whereas the BC for comma squares that holds for presheaves is appropriate for Dist.
However, at the time I eventually dropped it for several reasons. One is that I couldn’t find a nice way of doing it for a general monoidal fibration, i.e. a canonical way of producing bicategories like Span and Dist to encode the adjoint triples as adjoint adjunctions. (I don’t suppose you have any thoughts about that?) Another is that it requires a bicategory to already be present, whereas at the time I was looking for a theory that would describe the construction of a bicategory. A third is that it requires a theory of “bifibrations over bicategories”, which would probably be technically messy, and which I’ve never seen actually written down — did you have some way of dealing with that in mind? You said in the paper that “we prefer to treat Dist as a category than a bicategory” but I’m not sure exactly what that means, since Dist is not actually a category.
Secondly, you noticed that in a closed monoidal fibration whose base is compact closed (or maybe just -autonomous?), you can induce useful stuff on the fibers by pulling and pushing along curried maps downstairs. This is very cool! The Day convolution you mentioned is one example of that — it can be described in terms of a closed monoidal equipment, but the purely fibrational version is perhaps cleaner. And the way of “fixing” Lawvere’s construction of equality is quite neat too. I wonder whether you can use constructions like that to generalize my construction of a bicategory from an indexed monoidal category? Of course, that wouldn’t be interesting applied to , since in that case we’d just be reconstructing the bicategory we started from, but there might be other examples where it’s less trivial.
Thirdly, there is this chirality thing. I still don’t like notating the internal-hom as a disjunction, but it’s neat that it gives a way to extend the Pierce-Trimble-Brady string diagrams to the general closed case. However, I don’t quite understand what’s going on there (related to my unease about notation): don’t you have to indicate somehow which of the juxtapositions are the “action” (internal-hom) and which of them are the tensor product (or its dual)? Also, the nLab page on string diagrams mentions that the merely-closed case can be done “involving boxes to separate parts of the diagram”, which sounds like what you’re doing, and points to John’s QG seminar and this paper on proof nets; are those related to your string diagrams?
Regarding chiralities, where can I read about their connection to polarized linear logic (and about PLL in general)? Mellies’ paper mentions such a connection, but seems to assume the reader already knows what PLL is.
(Apologies that this turned into a jumble of half thoughts.)
What of the ’philosophy’ of type refinement which lies behind this paper? I mean that’s a bold claim here:
something is conceptually missing in the standard categorical reading of type theory.
Could we say that HoTT is a paradigmatic case of the intrinsic type perspective? Or even there could one have a refinement system of slices over their objects?
I see that the ’ornaments’ of A Categorical Treatment of Ornaments are a kind of refinement and are shown to form a framed bicategory.
…also appeared in the adjoint logic representation of cohesion
So there might be something to my #13.
…the Pierce-Trimble-Brady string diagrams…
It’s ’Peirce’ remember :).
something is conceptually missing in the standard categorical reading of type theory.
I would say a little less boldly that the “standard categorical reading of type theory” should not be considered (and, to my knowledge, has never been claimed to be) an isomorphism of entire subjects, but a correspondence between certain aspects of certain categories with certain aspects of certain type theories. The standard categorical interpretation of HoTT does, indeed, use an intrinsic perspective, but one could certainly consider adding subtyping to it. But even before that, there are subtle questions related to their point that
the very idea of a typing judgment in some sense presupposes a domain of expressions which may be judged
which comes up, among other places, when constructing categorical models, in the guise of the question of how “raw” the syntax should be. As I said in that post,
whether we like it or not, what we write on paper when we do mathematics (and what we type into a proof assistant as well) does not consist of elements of a highly structured inductive-inductive system: it is a string of raw symbols.
and
I strongly suspect that in practice, we constantly identify terms that are “actually” coercions along different-looking judgmental equalities.
Mike #19:
Okay, now I had a chance to look at this paper more carefully, and I see that there is neat stuff in it! If I may, let me rephrase what I got from the paper from my perspective and background, and you can tell me what I missed.
Thanks for the positive words! I think your summary of what you got out of the article is a pretty close description of the ideas Paul-André and I tried to convey, and you raise some good questions. One small additional point we made in the article which I thought you might appreciate has to do with the definition of a “monoidal closed bifibration”. You can see that we basically take this to mean a strict monoidal closed functor which is also a bifibration, with no explicit requirement that the tensor and/or internal hom preserves cartesian/opcartesian morphisms. That’s the definition we eventually settled on in our previous work, motivated by formal considerations, but we were lacking concrete examples of monoidal closed bifibrations where the tensor product fails to preserve cartesian morphisms – and so we were reassured in working on this paper to realize that and do provide such concrete counterexamples.
However, at the time I eventually dropped it for several reasons. One is that I couldn’t find a nice way of doing it for a general monoidal fibration, i.e. a canonical way of producing bicategories like Span and Dist to encode the adjoint triples as adjoint adjunctions. (I don’t suppose you have any thoughts about that?)
This is indeed something we have in mind, to extract an axiomatic framework from the example of , but we have not tried to work this out yet.
Another is that it requires a bicategory to already be present, whereas at the time I was looking for a theory that would describe the construction of a bicategory. A third is that it requires a theory of “bifibrations over bicategories”, which would probably be technically messy, and which I’ve never seen actually written down — did you have some way of dealing with that in mind? You said in the paper that “we prefer to treat Dist as a category than a bicategory” but I’m not sure exactly what that means, since Dist is not actually a category.
It’s a subtle question, and as I mentioned above we do not yet have a completely clear picture of how the idea of viewing functors as type refinement systems should be interpreted in higher dimensions, so I’m not sure I can give you a completely satisfying answer. My intuition is that this question is related to the interpretation of the “conversion rule” (discussed in our POPL paper), which is valid for any refinement system modelled as a functor between 1-categories:
When is a bicategory one shouldn’t talk about equality of 1-cells, but we might nonetheless consider directed versions of this rule. In particular, the refinement system validates the conversion rule
where denotes a natural transformation between distributors. We can also think about this in terms of Bénabou’s idea that any functor induces a lax functor , with a fibration corresponding to a functor such that factors through . Then when and are bicategories rather than categories, a refinement systems validating the directed conversion rule above should correspond to a lax functor .
Secondly, you noticed that in a closed monoidal fibration whose base is compact closed (or maybe just * *-autonomous?), you can induce useful stuff on the fibers by pulling and pushing along curried maps downstairs.
This is really at the heart of ideas we’ve been exploring for a few years now. We’ve found that these kinds of patterns (of taking a tensor product/hom upstairs and then pushing/pulling along maps defined using the smc structure downstairs) show up in many places, and that they give a way of decomposing various semantic artifacts which show up in programming languages and proof theory (Section 6 of “functors are type refinement systems” has an extended example of this, and the “Isbell” paper discusses different kinds of examples).
Mike #19 & #20:
Thirdly, there is this chirality thing. I still don’t like notating the internal-hom as a disjunction, but it’s neat that it gives a way to extend the Pierce-Trimble-Brady string diagrams to the general closed case. However, I don’t quite understand what’s going on there (related to my unease about notation): don’t you have to indicate somehow which of the juxtapositions are the “action” (internal-hom) and which of them are the tensor product (or its dual)?
We can always interpret juxtaposition as one of the “conjunctions” , either as the tensor product or the left action or right action . Intuitively, the reason why we can always do this unambiguously (up to the equations of the tensor product and actions) is because we restrict to diagrams where there is exactly one negated blue region inside a red region. Of course, we should eventually prove some sort of coherence theorem…
Also, the nLab page on string diagrams mentions that the merely-closed case can be done “involving boxes to separate parts of the diagram”, which sounds like what you’re doing, and points to John’s QG seminar and this paper on proof nets; are those related to your string diagrams?
I think that the diagrams for monoidal closed categories you get out of the decomposition in terms of monoidal closed chiralities are essentially equivalent to the diagrams in John’s notes (and the “clasp” notation in his Rosetta Stone paper with Mike Stay). On the other hand, I am pretty sure that the “intuitionistic proofnets” in François Lamarche’s paper are based on an essentially different idea. I haven’t studied his diagrams in particular, but I’ve been working a lot lately with “proofnets for linear lambda calculus”, and in that case, rather than reading these as string diagrams for morphisms in smc categories, they should rather be interpreted as string diagrams for endomorphisms of a reflexive object in an smc (bi)category.
Regarding chiralities, where can I read about their connection to polarized linear logic (and about PLL in general)? Mellies’ paper mentions such a connection, but seems to assume the reader already knows what PLL is.
The situation is a bit embarrassing in that people use the phrase “polarized linear logic” to mean different things, and looking now in that paper I see Paul-André uses the phrase in a different sense than I was (he uses it to refer to a system introduced in Olivier Laurent’s thesis). In any case, though, the connection is to various systems which maintain a syntactic distinction between positive and negative formulas. You could have a look at section 3 of Resource modalities in tensor logic, which describes two different presentations of “tensor logic”. What I was referring to as “polarized linear logic” is basically what that paper refers to as the “one-sided presentation” of tensor logic (it also separately discusses Laurent’s system). (I also wrote some informal notes a couple years ago that you may or may not find helpful: section 5 includes a little focused sequent calculus for polarized linear logic in this sense, i.e., the “one-sided presentation” of tensor logic.) Tensor logic can be interpreted in any dialogue category (a symmetric monoidal category equipped with an object and the corresponding internal homs for all ), so of course you can do the same for the “one-sided presentation”/polarized linear logic, but the idea is that you can use (dialogue) chiralities to match the syntax a little more closely.
David #21:
I mean that’s a bold claim here[…]
Of course I think that the intrinsic/extrinsic distinction is important. The paper you quoted was the first one we wrote on these subjects, though, unpublished and pretty unfiltered. Most of the contents eventually made it into Functors are type refinement systems, which I think does a better job of presenting the issues, in particular by giving a detailed categorical explanation of Reynolds’ original paper.
One small additional point we made in the article which I thought you might appreciate has to do with the definition of a “monoidal closed bifibration”. You can see that we basically take this to mean a strict monoidal closed functor which is also a bifibration, with no explicit requirement that the tensor and/or internal hom preserves cartesian/opcartesian morphisms.
I think I have to say that I regard the non-preservation of cartesian arrows by the tensor product in as an argument against it (and in favor of other structures where the fibrational aspect applies only to functors rather than distributors), rather than an argument against including that as part of the definition of monoidal fibration. (-: Categorically speaking, when one object has two structures you almost always want them to be compatible in some way. I can accept monoidal fibrations whose tensor product doesn’t preserve opcartesian arrows (such as the fibration of set-indexed families of objects in a monoidal category whose tensor product doesn’t preserve colimits), but the reindexing functors of a fibration are supposed to preserve everything in sight; type-theoretically they are just substitution.
We can always interpret juxtaposition as one of the “conjunctions” … Intuitively, the reason why we can always do this unambiguously (up to the equations of the tensor product and actions) is because we restrict to diagrams where there is exactly one negated blue region inside a red region.
Okay, I guess with that restriction I can see it. Did you mention that restriction anywhere in the paper? I didn’t notice it.
Categorically speaking, when one object has two structures you almost always want them to be compatible in some way.
I don’t find that to be a very convincing argument. There are plenty of examples where one object has two structures but we don’t necessarily ask for them to be compatible, take “monoidal category with products” or “monoidal category with coproducts”: the tensor product might preserve products/coproducts in some situations (e.g., when it has a right or left adjoint), but it makes sense to consider the more general situation. In any case, we found that this particular preservation assumption is unnecessary for proving the theorems we want to prove, and we want to apply these theorems in situations such as the monoidal closed bifibration over Rel or over Dist where the assumption is violated.
Okay, I guess with that restriction I can see it. Did you mention that restriction anywhere in the paper? I didn’t notice it.
We described how to translate presheaves constructed in the language of monoidal closed bifibrations into diagrams, and the property that I mentioned is a property of the image of that translation.
Categorically speaking, when one object has two structures you almost always want them to be compatible in some way.
I don’t find that to be a very convincing argument.
To try to pin this down more positively, perhaps the difference is that we view being a fibration as a property of a functor (in the same way that the existence of limits is a property of a category), rather than as an algebraic structure. Type-theoretically, if we view functors as type refinement systems, then the property of being a fibration corresponds to whether or not a type system includes a particular class of refinement types, rather than to a primitive operation of substitution.
It’s true, I find my second argument about substitution much more convincing too. I suppose your point is that you’re using fibrations for something different than I’m used to.
Mike, looking at this conversion again, I see in #19 you say:
it requires a theory of “bifibrations over bicategories”, which would probably be technically messy, and which I’ve never seen actually written down
Is this not what’s referred to on slide 20 of his HoTTEST talk?
Perhaps something to add to bifibration.
Yes, that is what’s referred to there. I think that at the time I wrote #19, I was not aware of Mitchell Buckley’s paper Fibred 2-categories and bicategories, which develops all the basic theory or fibrations of bicategories that one would hope for. He doesn’t say anything explicit about opfibrations and bifibrations, but in private correspondence with him we decided that a “2-bifibration”, meaning a functor of bicategories that is both a 2-fibration and a 2-opfibration, should correspond to a pseudofunctor into , just as for 1-categories. The only sneaky thing is that although a 2-fibration (corresponding to a “doubly contravariant” pseudofunctor ) has both cartesian lifts of 2-cells and 1-cells, a 2-opfibration (corresponding to a totally covariant pseudofunctor ) has opcartesian lifts of 1-cells but still cartesian lifts of 2-cells.
I’ve added this into bifibration.
Where it has
a pseudofunctor into , just as for 1-categories
we need to explain this in the 1-category case. This paper, Categorical Foundations for K-Theory, talks about the 2-category of pseudo double functors into the double category of adjunctions.
1 to 32 of 32