Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: Hyperdoctrine

Bottom of Page

1 to 42 of 42

  1.  
    • CommentRowNumber1.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 18th 2011

    Made a start – hyperdoctrine.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeApr 18th 2011
    • (edited Apr 18th 2011)

    just for the record, there is an entry titled first-order hyperdoctrine

    I have added preliminary links between the two entries. But I guess they should be merged or otherwise harmononized?

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 18th 2011

    I did link to that page from the ’classical’ in “Given any theory (several sorted, intuitionistic or classical) …”. But maybe it should be more apparent. Some commentary on whether the impression is correct that hyperdoctrines disappeared from view somewhat would be welcome.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeApr 18th 2011

    I did link to that page

    Oh, sorry. I didn’t see that.

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeApr 18th 2011

    I would be inclined to merge them.

    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 19th 2011

    Yes, they may as well be merged. Who knows about such things? I couldn’t even say how are the Beck-Chevalley and Frobenius conditions are related. Hmm, there’s a MO answer by Todd on this relation which he suggests might be incorporated into the nLab. And I dare say something from this thread could help give some more detail to the Beck-Chevalley condition.

    • CommentRowNumber7.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 19th 2011

    Another example to be included is again described by Todd here P:Grpd coop→CATP: Grpd^{co op} \to CAT.

    • CommentRowNumber8.
    • CommentAuthorFinnLawler
    • CommentTimeApr 19th 2011

    David said:

    I couldn’t even say how are the Beck-Chevalley and Frobenius conditions are related.

    I’m not sure they are, if by Frobenius condition you mean Frobenius reciprocity. There is another usage of the name of Frobenius, as in e.g. Walters and Wood’s paper Frobenius objects in cartesian bicategories, where an object AA is Frobenius if the Beck-Chevalley condition is satisfied for a certain ’product-absolute’ pullback square involving the diagonal Δ:A→A×A\Delta \colon A \to A \times A. I think the latter is what Todd’s MO answer refers to, but I for one don’t see a connection with Lawvere’s Frobenius condition. I’d love to be wrong about that, though.

    • CommentRowNumber9.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 19th 2011
    • (edited Apr 19th 2011)

    Todd puts the question here. Also at the MO answer

    …it is often the case (for example in certain simple type-theoretic contexts) where verification of the Beck-Chevalley condition boils down to Frobenius reciprocity.

    • CommentRowNumber10.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 19th 2011

    Also, see this paper for a situation where

    …one readily sees that the Frobenius Reciprocity Law is a particular case of the Beck-Chevalley Property.

    • CommentRowNumber11.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 19th 2011

    How should what is described at Ubiquity of the push-pull formula be characterized?

    • CommentRowNumber12.
    • CommentAuthorFinnLawler
    • CommentTimeApr 19th 2011

    What Todd calls Frobenius reciprocity is indeed a special case of Beck–Chevalley, but if you look at Equality in hyperdoctrines you’ll see that what Lawvere calls Frobenius reciprocity is what is described at the nLab page, and I can’t see that either has anything to do with the other.

    In the paper you cite by Clementino, Giuli and Tholen, their derivation of (Lawvere’s) Frobenius condition from Beck–Chevalley is, I think, specific to subobject fibrations, because it involves taking an arrow (in a pullback square in) the base category to be a subobject, i.e. an object in a fibre of the hyperdoctrine; but that obviously doesn’t make sense in an arbitrary hyperdoctrine.

    What Andrea Ferretti calls the push-pull formula in that MO question looks to be exactly Lawvere’s Frobenius condition (for monoidal bifibrations).

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeApr 19th 2011

    I think the Clementino-Giuli-Tholen observation will work whenever you have a hyperdoctrine equipped with a surjective map from the codomain fibration which preserves pullbacks, pushforwards, and fiberwise products. I’m not sure whether that’s noticeably more general than the context they’re actually in (fibrations of subobjects relative to a factorization system).

    • CommentRowNumber14.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 20th 2011

    Re 12, so there’s Frobenius Reciprocity as described by Todd (FR1) which is a consequence of Beck-C. Then there’s Lawvere’s FR2 which bears no relation to it, but FR2 is a consequence of Beck-C in some situations.

    I’m confused.

    • CommentRowNumber15.
    • CommentAuthorFinnLawler
    • CommentTimeApr 20th 2011

    Re 12, so there’s Frobenius Reciprocity as described by Todd (FR1) which is a consequence of Beck-C. Then there’s Lawvere’s FR2 which bears no relation to it, but FR2 is a consequence of Beck-C in some situations.

    Yes, that’s how it looks to me. The categories list might know more.

    I’m confused.

    I’m more or less permanently confused, so I can’t empathise, having forgotten what clarity feels like.

    • CommentRowNumber16.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 24th 2011
    • (edited Jun 24th 2011)

    Possibly I was misremembering or misusing some terms here, but let me try to guess what I was thinking. What follows will be a bit didactic, mainly just to jog my own memory.

    There is a Frobenius condition which occurs in, for example, Frobenius monoids or algebras, involving an equation relating a comultiplication δ\delta and a multiplication δ *\delta^*. It’s a pair of equations, one of which is

    δδ *=(δ *⊗1)(1⊗δ *)\delta \delta^* = (\delta^* \otimes 1)(1 \otimes \delta^*)

    More generally, there are Frobenius monads that arise from ambimorphic adjunctions F⊣GF \dashv G and G⊣FG \dashv F; the δ\delta would be the comultiplication of the comonad GFG F arising from G⊣FG \dashv F, and the δ *\delta^* would be the multiplication of the monad GFG F arising from F⊣GF \dashv G.

    There are categorified instances of this Frobenius condition which arise in bicategories of relations and in certain cartesian bicategories, as emphasized often by Walters. Here we have a canonical arrow

    δδ *→(δ *⊗1)(1⊗δ *)\delta \delta^* \to (\delta^* \otimes 1)(1 \otimes \delta^*)

    where we have an adjunction δ⊣δ *\delta \dashv \delta^* in a bicategory, and this arrow is mated to an coassociativity isomorphism for δ\delta. (A typical example is in the bicategory of sets and relations, where δ\delta is the functional relation given by a diagonal.) The Frobenius condition would assert that this (and a similar arrow) are isomorphisms; this can be exploited to show that bicategories of relations are compact closed and that each object cc is dual to itself, using a unit

    1→ε *c→δc⊗c1 \stackrel{\varepsilon^*}{\to} c \stackrel{\delta}{\to} c \otimes c

    and a counit

    c⊗c→δ *c→ε1c \otimes c \stackrel{\delta^*}{\to} c \stackrel{\varepsilon}{\to} 1

    As indicated in the MO answer mentioned above, this Frobenius condition holds for the bicategory of groupoids and profunctors between them, but does not hold for categories and profunctors. I think I managed to convince myself a few months ago that a form of it also holds for the tricategory of spans between groupoids.

    Then, we have what I think many people call Frobenius reciprocity, although it is called by other names too (e.g., ’projection formula’), and seems to occur all over mathematics. It has to do, more or less, with pullback functors f *f^* preserving internal homs (although it holds in other contexts too). Here we are dealing with an adjunction f !⊣f *f_! \dashv f^* or with an adjunction f *⊣f *f^* \dashv f_*, and the condition is basically an equation of the form

    f !S⊗T=f !(S⊗f *T)f_! S \otimes T = f_!(S \otimes f^* T)

    where S:W→XS: W \to X and T:W→YT: W \to Y are “arrows” (relations, correspondences, etc.), where ⊗\otimes refers to a local tensor living in local hom-categories like hom(W,Y)\hom(W, Y), and f !:X→Yf_!: X \to Y. This is well-known for bicategories of relations, and in the context of allegories is in fact generalized to Freyd’s modular law:

    RS∧T=R(S∧R opT)R S \wedge T = R(S \wedge R^{op}T)

    People around here have sometimes remarked that Freyd’s modular law is hard to really grok as a piece of categorical algebra (even though it has resonances elsewhere, as I tried to indicate once at the Café in the context of lattices of commuting equivalence relations). Walters makes this point too and shows how it follows in bicategories of relations from the other Frobenius condition, here.

    I think there’s probably more to say here on the connections between the two Frobenius conditions. I have to leave in a few minutes, but I hope to come back to this when I have some more time.

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeJun 25th 2011

    Thanks Todd! The modular law made a whole lot more sense to me once I realized that it’s just a version of the (second) Frobenius condition. I didn’t realize the connection to the other Frobenius condition, though; I look forward to hearing what more you have to say!

    • CommentRowNumber18.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 27th 2011

    Yes, thanks Todd. The mist is departing a little. I’m sure the nLab pages could use what you’ve written.

    • CommentRowNumber19.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 29th 2011

    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.

    • CommentRowNumber20.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 6th 2011
    • (edited Aug 6th 2011)

    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:

    • In a (locally posetal) cartesian bicategory, the Frobenius law implies Frobenius reciprocity.

    (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

    • In a (locally posetal) cartesian bicategory, Frobenius reciprocity implies the Frobenius law.

    (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 B\mathbf{B}, there is for each object cc a corresponding hyperdoctrine

    hom B(i−,c):Map(B) op→Cat\hom_{\mathbf{B}}(i-, c): Map(\mathbf{B})^{op} \to Cat

    where i:Map(B)↪Bi: Map(\mathbf{B}) \hookrightarrow \mathbf{B} is the inclusion. The idea is that each map f:a→bf: a \to b induces a substitution map f *:hom(b,c)→hom(a,c)f^\ast: \hom(b, c) \to \hom(a, c) on “relations” by pulling back along ff. If f †f^\dagger denotes the right adjoint of the map ff in B\mathbf{B}, then the corresponding existential quantification is defined by ∃ f=hom(f †,c):hom(a,c)→hom(b,c)\exists_f = \hom(f^\dagger, c): \hom(a, c) \to \hom(b, c).

    Frobenius reciprocity says that for each cc, the canonical map

    ∃ f(q∧f *r)→(∃ fq)∧r\exists_f(q \wedge f^\ast r) \to (\exists_f q) \wedge r

    is an isomorphism, for every map f:a→bf: a \to b and any “relations” q:a→cq: a \to c, r:b→cr: b \to c. (To repeat: I don’t think ’locally posetal’ is all that relevant, so that the conjunction ∧\wedge 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

    (q∧rf)f †→(qf †)∧r(q \wedge r f)f^\dagger \to (q f^\dagger) \wedge r

    is an isomorphism.

    Now let xx be any object, and consider the special case where f=δ=δ x:x→x⊗xf = \delta = \delta_x: x \to x \otimes x, where

    q=ε †⊗1 x:x→x⊗xq = \varepsilon^\dagger \otimes 1_x: x \to x \otimes x

    (i.e., q=ε x †⊗1 xq = \varepsilon_{x}^\dagger \otimes 1_x), and where

    r=ε⊗1 x⊗ε †:x⊗x→x⊗xr = \varepsilon \otimes 1_x \otimes \varepsilon^\dagger: x \otimes x \to x \otimes x

    (i.e., r=ε x⊗1 x⊗ε x †r = \varepsilon_{x} \otimes 1_x \otimes \varepsilon_{x}^\dagger).

    • Claim 1: (q∧rf)f †≅σδδ †(q \wedge r f)f^\dagger \cong \sigma \delta \delta^\dagger, where σ:x⊗x→x⊗x\sigma: x \otimes x \to x \otimes x is the symmetry.

    • Claim 2: (qf †)∧r≅σ(δ †⊗1 x)(1 x⊗δ)(q f^\dagger) \wedge r \cong \sigma (\delta^\dagger \otimes 1_x)(1_x \otimes \delta).

    Putting these two claims together with the Frobenius reciprocity isomorphism, we derive an isomorphism

    σδδ †≅σ(δ †⊗1 x)(1 x⊗δ)\sigma \delta \delta^\dagger \cong \sigma (\delta^\dagger \otimes 1_x)(1_x \otimes \delta)

    or, since σ\sigma is an isomorphism,

    δδ †≅(δ †⊗1 x)(1 x⊗δ)\delta \delta^\dagger \cong (\delta^\dagger \otimes 1_x)(1_x \otimes \delta)

    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

    q∧rδ=δ x⊗x †(q⊗rδ)δ xq \wedge r \delta = \delta_{x \otimes x}^\dagger (q \otimes r \delta) \delta_x

    Second, that rδ=(ε⊗1 x⊗ε †)δ=1 x⊗ε †r \delta = (\varepsilon \otimes 1_x \otimes \varepsilon^\dagger)\delta = 1_x \otimes \varepsilon^\dagger. This gives

    q⊗rδ=(x⊗x→ε †⊗1 x⊗1 x⊗ε †(x⊗x)⊗(x⊗x)).q \otimes r \delta = (x \otimes x \stackrel{\varepsilon^\dagger \otimes 1_x \otimes 1_x \otimes \varepsilon^\dagger}{\to} (x \otimes x) \otimes (x \otimes x)).

    Third, that δ x⊗x †=(x⊗x⊗x⊗x→1 x⊗σ⊗1 xx⊗x⊗x⊗x→δ †⊗δ †x⊗x)\delta_{x \otimes x}^\dagger = (x \otimes x \otimes x \otimes x \stackrel{1_x \otimes \sigma \otimes 1_x}{\to} x \otimes x \otimes x \otimes x \stackrel{\delta^\dagger \otimes \delta^\dagger}{\to} x \otimes x). Hence δ x⊗x †(q⊗rδ)\delta_{x \otimes x}^\dagger (q \otimes r \delta) becomes

    x⊗x→ε †⊗1 x⊗1 x⊗ε †x⊗x⊗x⊗x→1⊗σ⊗1x⊗x⊗x⊗x→δ †⊗δ †x⊗xx \otimes x \stackrel{\varepsilon^\dagger \otimes 1_x \otimes 1_x \otimes \varepsilon^\dagger}{\to} x \otimes x \otimes x \otimes x \stackrel{1 \otimes \sigma \otimes 1}{\to} x \otimes x \otimes x \otimes x \stackrel{\delta^\dagger \otimes \delta^\dagger}{\to} x \otimes x

    which can be rearranged to

    x⊗x→σx⊗x→ε †⊗1⊗1⊗ε †x⊗x⊗x⊗x→δ †⊗δ †x⊗xx \otimes x \stackrel{\sigma}{\to} x \otimes x \stackrel{\varepsilon^\dagger \otimes 1 \otimes 1 \otimes \varepsilon^\dagger}{\to} x \otimes x \otimes x \otimes x \stackrel{\delta^\dagger \otimes \delta^\dagger}{\to} x \otimes x

    which, up to isomorphism, collapses to just σ:x⊗x→x⊗x\sigma: x \otimes x \to x \otimes x. Therefore, we have q∧rδ≅σδq \wedge r \delta \cong \sigma \delta, so that

    (q∧rδ)δ †≅σδδ †(q \wedge r\delta)\delta^\dagger \cong \sigma \delta \delta^\dagger

    which is Claim 1.

    Whew.

    I’m petering out now, but Claim 2 is proved in a wholly similar way.

    • CommentRowNumber21.
    • CommentAuthorFinnLawler
    • CommentTimeAug 6th 2011

    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.

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeAug 8th 2011

    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.

    • CommentRowNumber23.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 9th 2011

    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.)

    • CommentRowNumber24.
    • CommentAuthorMike Shulman
    • CommentTimeAug 9th 2011

    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 “⊗\otimes 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.

    • CommentRowNumber25.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 9th 2011

    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 :-)

    • CommentRowNumber26.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 9th 2011

    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.

    • CommentRowNumber27.
    • CommentAuthorFinnLawler
    • CommentTimeAug 9th 2011
    • (edited Aug 9th 2011)

    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.

    • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeMar 1st 2012
    • (edited Mar 1st 2012)

    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 ;-)

    • CommentRowNumber29.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 1st 2012

    Lawvere defines a hyperdoctrine more generally to be a (pseudo)functor

    P:C op→CatP: C^{op} \to Cat

    (with adjoints on both sides, etc.), instead of restricting to just posets or lattices. And I agree with his decision.

    • CommentRowNumber30.
    • CommentAuthorUrs
    • CommentTimeMar 1st 2012
    • (edited Mar 1st 2012)

    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.

    • CommentRowNumber31.
    • CommentAuthorUrs
    • CommentTimeMar 1st 2012

    So I have made it now

    A hyperdoctrine for a given notion of logic LL is a functor P:T op→CP : T^{op} \to \mathbf{C} to some category or higher category C\mathbf{C} whose internal logic corresponds to LL, such that…

    But if you feel that this is not going in the right direction, please feel welcome to interfere.

    • CommentRowNumber32.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 1st 2012

    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 (P:C op→CatP: C^{op} \to Cat), and consider the example where CC is a model category, taking P(c)P(c) to be the category of fibrations over cc. (This is meant more as a pedagogical or expositional point.)

    • CommentRowNumber33.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 1st 2012

    Re #31: looks good to me so far. Not sure if I want to “interfere” (or tinker) with that.

    • CommentRowNumber34.
    • CommentAuthorUrs
    • CommentTimeMar 1st 2012
    • (edited Mar 1st 2012)

    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 = (0,1)(0,1)-categories.

    This changes as we pass to the internal logic of higher categories. In the context of (n,1)(n,1)-cartegories, logic is the theory (n−2)(n-2)-truncated morphisms. These form (n−1,1)(n-1,1)-categories, instead of just posets.

    So when Lawvere generalizes from hyperdoctrines with values in LatticeLattice to general ones with values in CatCat, he is essentially generalizing from 1-logic to 2-logic.

    As far as I can see.

    • CommentRowNumber35.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 1st 2012

    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).

    • CommentRowNumber36.
    • CommentAuthorMike Shulman
    • CommentTimeMar 1st 2012

    This is looking better. I rewrote the Idea section some more, to clarify that it is the objects of C\mathbf{C} whose internal logic is LL, not C\mathbf{C} itself.

    • CommentRowNumber37.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 1st 2012

    It is indeed looking better. Who are those quotations in the section on special cases attributed to? (They read a bit tentatively.)

    • CommentRowNumber38.
    • CommentAuthorFinnLawler
    • CommentTimeMar 1st 2012

    I think the quotations are from Lawvere’s Equality in hyperdoctrines.

    • CommentRowNumber39.
    • CommentAuthorUrs
    • CommentTimeMar 1st 2012

    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.

    • CommentRowNumber40.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 2nd 2012

    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?

    • CommentRowNumber41.
    • CommentAuthorUrs
    • CommentTimeNov 24th 2012
    • (edited Nov 24th 2012)

    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 TT 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.

    • CommentRowNumber42.
    • CommentAuthormaxsnew
    • CommentTimeJun 15th 2023

    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) C\mathbf{C}, whose objects are categories whose internal logic corresponds to LL. Thus, each object AA of TT is assigned an “LL-logic” (the internal logic of P(A)P(A)).

    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 PP sends A∈TA \in T to the poset of subobjects Sub T(A)Sub_T(A) of AA. The predicate logic we obtain in this way is the usual sort of internal logic of TT.

    Where internal logic of a category Tmeansthespecificconstructionofthehyperdoctrineofposetsof means the specific construction of the hyperdoctrine of posets of T$.

    And the link to internal logic is talking about the latter sense. How do you think we should clarify this situation?

1 to 42 of 42

  1.