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 comma 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 finite 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 k-theory lie-theory limits linear linear-algebra locale localization logic mathematics 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).
    • CommentRowNumber1.
    • CommentAuthorMike Shulman
    • CommentTimeDec 4th 2014

    I am currently experimenting with a new way to code comodalities such as \flat in Coq. The problem, as we know, is that semantically the coreflector is not an indexed functor, and hence cannot be represented internally as an operation TypeTypeType \to Type since such an operation would be applicable in any context. Previously our only method was to represent \flat as an endomorphism of Type\sharp Type, thinking of the latter as the “external” universe of “internal” types. But recently I have realized that Coq actually already has a way to talk about things in the empty context, namely “modules”. This gives another way to axiomatize \flat: rather than acting on “external” types in Type\sharp Type, we restrict it to act only on types in the empty context.

    Some code is here (link probably not long-term stable). So far I’ve managed to prove that XX is comodal as soon as XX\flat X \to X admits a section, and conclude that \emptyset is comodal. This gives at least some evidence that this approach may actually be feasible. The syntax for modules is rather verbose, requiring a fair amount of boilerplate in order to do anything with: the first proof is 3-4 times as long as the analogous proof for modalities (XX is modal as soon as XXX\to \sharp X admits a retraction). I don’t know how this will compare to the Type\sharp Type method, which will also be more verbose than a direct internal axiomatization; I haven’t yet tried to redevelop that theory in the new Coq library (I just finished the proof that Type Type_\sharp is modal when \sharp is lex).

    However, using modules has one potentially significant advantage over Type\sharp Type, namely, the types we work with are real types, and so all the machinery of the rest of the library can be applied to them directly. For instance, if we have some pointed connected type BGBG, then we need to jump through some module hoops in order to construct BG\flat BG, but once we have it, we really have BG:Type\flat BG : Type, and so we can (say) define dRBG\flat_{dR} BG directly as the fiber of the map BGBG\flat BG \to BG, where “fiber” has the same meaning as it does anywhere else in the library. Thus we can go on to apply all the theorems about fibrations, fibers, fiber sequences, and so on. With Type\sharp Type we would first have to manually “externalize” all of those theorems, because BG\flat BG would not be a type but only an element of Type\sharp Type. So in the long run, this may be a big win.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeDec 4th 2014

    Interesting, thanks for the message.

    What is the “theoretical” status of “modules” in Coq? From what you say it sounds like some feature that Coq happens to have, which is however outside of the “specification” (or whatever it is called) of HoTT.

    Or maybe asked differently: what is the categorical semantics for the type theory expressed by Coq+Modules? Do you think this is clear enough such that when you now prove anything via modules, one still knows that the result translates to a proof in some infinity-topos? Or rather, since that’s what it seems you are thinking, could you maybe exand a bit on the type theoretical status of this “modules” feature?

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeDec 4th 2014

    That was my first question too. (-: I haven’t heard anything from Bob Harper yet (I plan to ask him about it in person the next time I see him), but Jason says

    It is commonly believed that turning a parameterized module definition into a lambda abstration is impossible (though I know of no attempt at a formal proof), and my understanding of the universe algorithm is that such a transformation unsound, given how universes are implemented. (Of course, there could be a bug somewhere, given how complicated the implementation of modules and functors is.)

    Obviously the categorical semantics of modules ought to be studied, if it hasn’t been! However, even if it hasn’t, I don’t think I would feel worse about using them for this than I do about, say, using the private-types hack for HITs. In both cases we don’t know for absolute sure that the hack is sound, and in fact in the latter case people have occasionally uncovered bugs or subtleties forcing us to modify how we do the hack or in some cases fix the underlying proof assistant. However, if we keep in mind the categorical situation we’re intending to model, I think there’s not much danger of “accidentally” using such a bug and proving something invalid.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeDec 4th 2014
    • (edited Dec 4th 2014)

    Thanks. Well,it certainly sounds exciting. It sounds like it might be yet another instance of computer scientists considering a structure for computer-scientific reasons only which then turns out to mean something profound when thought of in terms of categorical semantics.

    What are these “modules” intended for, or designed for, from the point of view of the Coq-programmer? Which problem do they solve for them?

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeDec 4th 2014

    I don’t really know. (-:

    One thing they do is namespace control. You put a bunch of definitions in a module, and then somewhere else you can either import that module to get its definitions in your namespace, or you can refer to them qualified as Module.name and avoid polluting your own namespace. In fact, every file in Coq is automatically a module, and when you load other files you’re technically importing their modules. However, namespace control requires only a tiny fraction of what modules can do.

    In ML, which Coq’s modules are based on, I think modules are used to solve problems that arise in most real-world programming languages coming from the absence of dependent types, analogously to how typeclasses are used in Haskell. Coq also has typeclasses based on Haskell’s, but they are not as fundamental an innovation, because in a dependently typed language a typeclass can just be defined as a dependent record. Coq’s typeclasses add an automatic inference algorithm, which makes them easier to use, but they don’t add any fundamental expressivity to a language that already has dependent types (in fact, I believe they’re implemented entirely outside the kernel). ML uses modules in some of the same ways that Haskell uses typeclasses (e.g. Bob Harper wrote a blog post pointing out that monads, which Haskell implements with typeclasses and some extra syntactic sugar, can equally well be implemented with ML’s modules). But I don’t know what a traditional Coq programmer would use modules for that they couldn’t do just as well with dependent records.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeDec 4th 2014

    BTW, we are already using modules in two other places in the HoTT library. Their namespace control feature, combined with private types, is how we implement HITs. And they allow us to hypothesize a universe-polymorphic object, which turns out to be useful for modalities, as we want “a modality” to act on all universes at once “in the same way”.

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeJan 6th 2015

    Hi Mike, just out of interest: any news regarding your experiment here?

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeJan 7th 2015

    No, I’ve been busy with other things and haven’t had the chance to push it any further.

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeJan 7th 2015

    You know, what would help, when I get back to it, would be to have a concrete goal to formalize. Can you suggest a theorem that’s interesting and not too difficult, but uses \flat and its universal property in a nontrivial way?

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeJan 7th 2015
    • (edited Jan 7th 2015)

    One simple statement that is nevertheless of actual interest is the one we recently discussed in what I had managed to make a wild goose-chase towards a cohesive axiomatization of the Penrose-Ward transform:

    Theorem: Given a cohesive \infty-group GG, then the Maurer-Cartan form θ G:G dRBG\theta_G \colon G \to \flat_{dR}\mathbf{B}G carries an essentially unique GG-equivariant structure, intertwining the right action of GG on itself with the gauge action of GG on its flat differential forms.

    If this is too simple, let me know and I’ll think of something else.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeJan 9th 2015

    That’s a good start, thanks.

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 11th 2015

    In thinking about this some more I have realized that the two ways to axiomatize \flat are closely related.

    The version with modules works even in the absence of \sharp, of course. But as long as the discrete types are closed under finite limits (such as if ʃʃ exists), it follows that there is a way to internalize \flat as a map TypeType\flat Type \to \flat Type. Namely, the counit TypeType\flat Type \to Type induces a fibration over Type\flat Type, and if we apply \flat to its domain we get another fibration that is classified by another map TypeType\flat Type \to Type; now factor this through the counit to get :TypeType\flat_\flat :\flat Type \to \flat Type. Then if we do have \sharp, this is equivalent to a map :TypeType\flat_\sharp : \sharp Type \to \sharp Type, and I expect that the rest of the original axiomatization follows. The only snag I expect is that without a resizing axiom, the codomain of \flat_\flat will be a larger universe than its domain.

    In the opposite direction, I think if we start from the original axiomatization in terms of Type\sharp Type and add (using modules) the single rule that any element a:Aa:\sharp A in the empty context is of the form η(a)\eta(a') for some a:Aa':A, then we can recover all the benefits of the full axiomatization with modules. For instance, a type AA in the empty context yields an element of Type\sharp Type in the empty context, to which we can apply :TypeType\flat_\sharp : \sharp Type \to \sharp Type, and then (by our rule) deduce A:Type\flat A : Type. And so on. Semantically, I think what’s happening is that Type\sharp Type induces an indexed category over the topos of codiscrete types, and the axiomatization of \flat_\sharp asserts that the self-indexing of the codiscrete types is a coreflective sub-indexed-category of this; but without a rule like the one above, we can’t identify this indexed category with the one induced as usual by a ΔΓ\Delta\dashv\Gamma geometric morphism (i.e. whose fiber over UU is the slice over ΔU\Delta U).

    So now I am starting to think that maybe the best thing to do is add this single rule to the \flat_\sharp version, since the two are basically equivalent but this one doesn’t have a problem of universes. (This would also remedy a defect with the pure-modules axiomatization, namely that we can’t actually assert the full universal property of A\flat A since it would require infinitely many axioms, and there is no way to “apap” a module function to get them all from a finite number the way we can internally.) But I’ll need to experiment with it to see how well it works… and I don’t know when I’ll have time for that…

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeFeb 12th 2015
    • (edited Feb 12th 2015)

    Just to check if I am following: you are saying at the end that you now tend to not use modules after all, but to rather add that extra rule to sharp?

    While I have no sense of what goes into the details of coding with those modules, I have some gut feelings (which may or may not be of interest, but which I’ll communicate anyway):

    – Using modules seems to require expanding the underlying meta-theory more than I would have hoped to be necessary. I would have hoped that it has been settled what HoTT is and based on that safe foundation we now proceed to interesting applications on that basis. Changing the foundations as the applications change may at times be necessary, but here it seems to defeat the purpose a bit.

    – One aspect of the axiom system of cohesion that makes it attractive is that it is so simple and elegant and yet so expressive (in the homotopy theoretic context at least). Speaking externally it is super-simple. Speaking internally we may expect some extra care to be necessary, as indeed is the case, but it would seem disappointing if the internal formalization ends up looking contrived or inelegant. Optimally, the internal formulation would superficially look a little more subtle than the external formulation, but would on reflection reveal some further intrinsic elegance.

    – In this vein, I had very much enjoyed the fact that your original HoTT-formalization of cohesion gave \sharp the special role of laying the ground on which the others stand. This feels right in a philosophical way. (If we further assume that \sharp \emptyset \simeq \emptyset, i.e. that falsefalse\sharp false \simeq false, i.e. if \sharp “resolves the absolute contradiction” falsetruefalse \dashv true, then other people had suggested before that this \sharp is the ground of everything else…)

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeFeb 26th 2015

    Hi Mike,

    please ignore the whimsical bits in #13, if they are off-putting. I’d just enjoy if you could get back to me on the question:

    Just to check if I am following: you are saying at the end that you now tend to not use modules after all, but to rather add that extra rule to sharp?

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 26th 2015

    Sorry, somehow I missed seeing #13 entirely. Thanks for the bump.

    The extra rule for \sharp would itself have to be done using modules, since it’s only valid in the empty context and modules are the only way we have to say that. But that would be the only use of a module. I haven’t actually tried this way of formalizing anything yet, though, so I can’t say for sure how well it will work. In particular, I don’t know how often one would want to actually use that module. There might be different choices to be made about how often to use it, and I don’t know yet which would be best.

    Regarding the rest, I share most of your feelings, but right now I’m not sure which approach I would consider more elegant. Also I do think it is a bit early to want the foundations of HoTT to be completely settled; the whole field is only a few years old.

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeFeb 26th 2015

    I see, thanks. Hm, interesting.

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeFeb 26th 2015

    Do you have a (higher-)topos-theoretic picture of this situation?

    I mean something like: suppose you didn’t know type theory, would there be anything in topos theory that would have the kind of feeling to it of invoking this single use of “module”?