I think there’s an unfortunate overloading of the phrase “internal logic” in the intro here. It’s used twice:
to some 2-category (or even higher category) , whose objects are categories whose internal logic corresponds to . Thus, each object of is assigned an “-logic” (the internal logic of ).
To mean something like “typed lambda calculus is the internal language/logic of cartesian closed categories”. I.e., that a model of lambda calculus is a CCC or equivalently that lambda calculus is a construction of a free CCC.
The second one says
A canonical class of examples of this case is where sends to the poset of subobjects of . The predicate logic we obtain in this way is the usual sort of internal logic of .
Where internal logic of a category TT$.
And the link to internal logic is talking about the latter sense. How do you think we should clarify this situation?
]]>Promted by discussion in another thread I have expanded the Idea-section at hyperdoctrine to now start as follows:
]]>The notion of a hyperdoctrine is essentially an axiomatization of the collection of slices of a locally cartesian closed category (or something similar): a category together with a functorial assignment of “slice-like”-categories to each of its objects, satisfying some conditions.
In its use in mathematical logic a hyperdoctrine is thought of (under categorical semantics of logic/type theory) as a collection of contexts together with the operations of context extension/substitution and quantification on the categories of propositions or types in each context. Therefore specifying the structure of a hyperdoctrine over a given category is a way of equipping that with a given kind of logic.
That’s exactly what I was doing.
Now people are looking at hyperdoctrine, was I right in the modal logic post to think there could be a modal hyperdoctrine? Was Neel onto something here?
Then there’s the question of the relationship between the hyperdoctrine approach and the syntactic category approach. Is there a good way to pass between them?
]]>They read a bit tentatively.
Yes, these are remnants of the original form of the entry by, I think, David Corfield, which was all tentative by design. I think David was hoping one of us would pick up this thread and flesh out the entry. Which is what we are doing now.
]]>I think the quotations are from Lawvere’s Equality in hyperdoctrines.
]]>It is indeed looking better. Who are those quotations in the section on special cases attributed to? (They read a bit tentatively.)
]]>This is looking better. I rewrote the Idea section some more, to clarify that it is the objects of whose internal logic is , not itself.
]]>I follow that much better now – thanks for explaining. I don’t disagree with it in spirit (and I like the idea of keeping options open in the Idea section, as you have it now).
]]>Lawvere is amplifying on his insight that quantifiers in ordinary logic are examples of adjoints, and he wants to emphasize here that adjoints, not ordinary logical quantifiers, are really the more basic foundational concept.
Okay, I see.
I’m not sure what you mean by your second sentence in #30.
Right, I didn’t say that well. What I am thinking is this:
Ordinary logic, interpreted in category theory, is the theory of monomorphisms. These form posets. That’s why a hyperdoctrine that expresses some ordinary theory will take values not in arbitrary categories, put in posets = -categories.
This changes as we pass to the internal logic of higher categories. In the context of -cartegories, logic is the theory -truncated morphisms. These form -categories, instead of just posets.
So when Lawvere generalizes from hyperdoctrines with values in to general ones with values in , he is essentially generalizing from 1-logic to 2-logic.
As far as I can see.
]]>Re #31: looks good to me so far. Not sure if I want to “interfere” (or tinker) with that.
]]>I’m not sure what you mean by your second sentence in #30. But it seems to me that Lawvere is amplifying on his insight that quantifiers in ordinary logic are examples of adjoints, and he wants to emphasize here that adjoints, not ordinary logical quantifiers, are really the more basic foundational concept. (And I guess he would like to redefine “logic” in such a more general way, in terms of systems of adjoints between categories.)
Obviously the concept of hyperdoctrine is so plastic that you could generalize/specialize in all sorts of directions, such as the one you mention. But if I were to try to write something on “HTT for dummies”, my inclination would be to use Lawvere’s more vanilla definition at the outset (), and consider the example where is a model category, taking to be the category of fibrations over . (This is meant more as a pedagogical or expositional point.)
]]>So I have made it now
A hyperdoctrine for a given notion of logic is a functor to some category or higher category whose internal logic corresponds to , such that…
But if you feel that this is not going in the right direction, please feel welcome to interfere.
]]>Okay, sure, I’ll change the entry accordingly.
As far as I can see, this is the natural categorification of the logic, isn’t it? In view of (directed) homotopy type theory we’d allow ourselves to take values in more general higher categories, I suppose.
]]>Lawvere defines a hyperdoctrine more generally to be a (pseudo)functor
(with adjoints on both sides, etc.), instead of restricting to just posets or lattices. And I agree with his decision.
]]>I have tried to brush-up the entry hyperdoctrine a little.
In particular I have tried to write a more informative Idea-section.
Would be glad if an expert found a minute to look over this. Despite its name, which suggests quite otherwise, the notion of hyperdoctrine is quite simple, and I hope we can get the entry to the point that it reflects this :-) (Why on earth was that name “hyperdoctrine” chosen?)
If you had to give the idea of hyperdoctrines in one short sentence, what would you do? How about
A hyperdoctrine is a collection of propositions in various contexts, together with a rule for how to change the context by substitution/introduction of variables and by applying quantifiers.
?
Isn’t it as simple as that?
Next, a hyper-cyber-multi-ultra-doctrine is… But let’s leave that for later ;-)
]]>Mike #22: Oh, OK. I hadn’t realised that Frobenius was needed to pass from a monoidal fibration to a framed bicategory. Thanks for the clarification.
]]>I’ll mail them to both of you, a little later today. I might even be able to construct a .pdf of the thing.
David: thank you for the very kind offer! The biggest benefit to me would be to learn from what you did.
]]>I’d be happy to make (mock?) up some graphics from a hand-drawn version. Clearly mailing them to Mike to scan is quicker than mailing them to me :-)
]]>What about mailing photocopies to someone else who could scan them in? I’d be happy to do the scanning… (-:
Actually, I don’t think this correspondence even requires cartesianness; it should work in the more general context of monoidal fibrations and monoidal (framed?) bicategories. The construction of a monoidal bicategory from a monoidal fibration is in my paper “Framed bicategories and monoidal fibrations,” and I believe it specializes to the construction of a cartesian bicategory from a hyperdoctrine in the cartesian case. It uses both the Beck-Chevalley condition and Frobenius reciprocity (which I prefer, in that context, to call “ preserves indexed coproducts”). The other direction is more interesting and I’m not quite sure how it will go, but I think you’d need to use a framed bicategory as given rather than constructing the framing out of left adjoints the way you do in a cartesian bicategory.
]]>I’ll see if I can scan something in, but even doing that tests my limits…
My memory (and this is from maybe more than 10 years ago) is that indeed both Frobenius reciprocity and Beck-Chevalley get used to obtain a cartesian bicategory from a hyperdoctrine. I’ll have to review what the deal is, and then I should write it up over at cartesian bicategory. (Actually, I have begun muttering stuff about hyperdoctrines over there already, but it’s somewhat preliminary. I do feel that these back and forth relationships between the Frobenius law and Frobenius reciprocity belong in the more general cartesian bicategory context, which would include Span.)
]]>This is great! I haven’t read the proof yet, though; I’d be much happier to see the string diagrams. Even scanned handwritten ones would be better than nothing.
In reply to Finn, I’m not sure it means that Lawvere’s Frobenius axiom is a consequence of the Beck-Chevalley condition. I think you need Lawvere’s Frobenius condition (in addition to Beck-Chevalley) in order to construct a bicategory of relations from a hyperdoctrine, which is the context that Todd’s working in.
]]>Great stuff, Todd; very interesting! So it seems that Lawvere’s Frobenius reciprocity is indeed a consequence of the Beck–Chevalley condition for pullback squares. That’s a surprising result in itself.
]]>Okay, I think I now have something new to add now, and in some sense it’s actually pretty cool.
First, I’ve done some cleaning up in Frobenius reciprocity, in the section where I showed that Frobenius reciprocity holds in a bicategory of relations. (Recall that a bicategory of relations, in the sense of Walters or Carboni-Walters, is a locally posetal cartesian bicategory in which the so-called Frobenius laws hold. These are the laws similar to the key axioms of a Frobenius algebra, and which famously hold in the symmetric monoidal category of 2-cobordisms.)
What I labbified over a month ago (see comment 19) could be summarized as follows:
(I actually don’t think we need the ’locally posetal’ clause, but I’ll let that stand for the moment.) That’s the old news.
The new news is that I think we can also say
(Again, I doubt ’locally posetal’ plays much of a role.) I’ll sketch the proof here in old-fashioned notation, although it’s best comprehended with the aid of string diagrams, which I really don’t know how to display graphically – I’m no good at computer graphics stuff. At some point I’ll try to write up the proof at Frobenius reciprocity, but I want to run through it here first.
Recall what ’Frobenius reciprocity’ means in this context. Given a cartesian bicategory , there is for each object a corresponding hyperdoctrine
where is the inclusion. The idea is that each map induces a substitution map on “relations” by pulling back along . If denotes the right adjoint of the map in , then the corresponding existential quantification is defined by .
Frobenius reciprocity says that for each , the canonical map
is an isomorphism, for every map and any “relations” , . (To repeat: I don’t think ’locally posetal’ is all that relevant, so that the conjunction here probably can and should be replaced by a local cartesian product in a general cartesian bicategory. I’ll continue with this notation anyway.) In our case, this is the same as saying that the canonical map
is an isomorphism.
Now let be any object, and consider the special case where , where
(i.e., ), and where
(i.e., ).
Claim 1: , where is the symmetry.
Claim 2: .
Putting these two claims together with the Frobenius reciprocity isomorphism, we derive an isomorphism
or, since is an isomorphism,
which is the Frobenius law.
The full details of these claims are a little involved, and possibly boring, but easy via string diagrams. One needs a few ancillary results: first that
Second, that . This gives
Third, that . Hence becomes
which can be rearranged to
which, up to isomorphism, collapses to just . Therefore, we have , so that
which is Claim 1.
Whew.
I’m petering out now, but Claim 2 is proved in a wholly similar way.
]]>I tried labbifying the argument I gave at Frobenius reciprocity. There may be more to add, but I’m having trouble thinking of exactly what.
]]>