Processing math: 100%
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 definitions 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 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 object 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
    • CommentTimeFeb 26th 2010

    Some reorganization and added material at type theory. In particular, I added some of the basic syntax of type theories, and also some comments about extensional vs. intensional type theories.

    • CommentRowNumber2.
    • CommentAuthorHarry Gindi
    • CommentTimeFeb 26th 2010
    • (edited Feb 26th 2010)

    I'm really bothered by the lack of a definition. Surely we can define it formally using a Hilbert-style proof calculus, no? I mean, this isn't often covered, but in Ch.1 section 1 of book 1 of Bourbaki, they actually give a rigorous definition of a "mathmatical theory". I believe that this is flexible enough to encode type theories as well as set theories.

    • CommentRowNumber3.
    • CommentAuthorEric
    • CommentTimeFeb 26th 2010

    Let me save Urs the trouble and suggest you add it yourself.

    • CommentRowNumber4.
    • CommentAuthorHarry Gindi
    • CommentTimeFeb 26th 2010

    I don't know anything about type theories. =(.

    • CommentRowNumber5.
    • CommentAuthorEric
    • CommentTimeFeb 26th 2010

    No worries :) You know a lot more about them than I do. You could always give it a shot and report back here, "I gave a shot at a definition for type theory. How is it? Did I completely mess up?"

    I do that kind of thing all the time. Nothing like getting attention to a page by putting something wrong on it. Then the experts come in full force :)

    • CommentRowNumber6.
    • CommentAuthorDavidRoberts
    • CommentTimeFeb 26th 2010

    Even better: put up a new page on the Bourbaki stuff, then waffle at type theory, and say it is something like the new page, only typey-er.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 26th 2010

    You can of course define any particular type theory formally. ButI've never seen a formal definition that includes all things called "type theories" and only things called "type theories." But I haven't tried very hard to produce one, either, so if you feel like trying, have a go, as long as you don't mind people coming along and poking holes in it. (-:

    • CommentRowNumber8.
    • CommentAuthorHarry Gindi
    • CommentTimeFeb 26th 2010

    I don't write things unless I'm sure that they're either right, or wrong in an interesting way.

    • CommentRowNumber9.
    • CommentAuthorSridharRamesh
    • CommentTimeFeb 26th 2010
    • (edited Feb 26th 2010)

    Then be interesting, and you won't have to worry about if you're right or wrong. :)

    Out of curiosity, when Bourbaki define "mathematical theories", what does it amount to? E.g., is it necessarily a theory in first-order classical logic? Is it more broadly just any recursively enumerable collection? Do they give a criterion for equality of theories, and if so, how "presentation-free" is it? Etc.

    • CommentRowNumber10.
    • CommentAuthorHarry Gindi
    • CommentTimeFeb 26th 2010

    It's just a language and a syntax in a very broad metamathematical sense. See here: http://books.google.com/books?id=IL-SI67hjI4C&lpg=PP1&ots=nahrxb7fLG&dq=theory%20of%20sets%20bourbaki&pg=PA15#v=onepage&q=&f=false

    • CommentRowNumber11.
    • CommentAuthorSridharRamesh
    • CommentTimeFeb 27th 2010
    • (edited Feb 27th 2010)
    Well, at a quick glance, that certainly seems to assume at least the language of classical first-order logic. Ah well; I was just curious if they gave a very broadly encompassing definition or a more narrow, specific framework to restrict the ordinary language word "theory" to.
    • CommentRowNumber12.
    • CommentAuthorHarry Gindi
    • CommentTimeFeb 27th 2010

    It doesn't assume any "logic" at all, at least in my understanding (it's certainly not classical, anyway). The logical axioms are only even defined in section 3 or 4. I'm pretty sure it's just a syntax with a few definitions.

    • CommentRowNumber13.
    • CommentAuthorSridharRamesh
    • CommentTimeFeb 27th 2010
    • (edited Feb 27th 2010)
    Well, the first thing they do is hardcode into the syntax "logical signs" (their term) clearly meant to be disjunction, negation, and quantification (by way of a choice operator; "any x such that..."); they come built-in, with apparently special status; accordingly, there is a restriction to a particular notion of language/syntax (one which deals with those signs). I call that "first-order" because they build in quantification, and I say "classical" because they explain the intended interpretation of these symbols in a classical way (e.g., intending implication to be represented as a combination of negation and disjunction, and so on). Anyway, it was just an idle curiosity to see what they did.
    • CommentRowNumber14.
    • CommentAuthorHarry Gindi
    • CommentTimeFeb 27th 2010

    True, but the next few sections don't attribute any meaning to the symbols, where they're really just defined syntactically.

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 27th 2010

    I rearranged the section syntax of type theory to make it look more like a definition. Does that make you any happier?

    • CommentRowNumber16.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 1st 2010

    Seeing the adjunction between semantics and syntax on the type theory page, reminded me of a comment of Lawvere's to the categories mailing list on 5 Jan 2010. What can we learn from this?:

    Actually, the term 'syntax' refers NOT to small categories such as algebraic theories or rings, but rather to their PRESENTATION by signatures or by polynomial generators, et cetera. The process of presentation is an adjoint pair quite distinct from the semantical adjoint pair: both adjoint pairs have a category of theories or of rings in common but are otherwise quite independent.

    In particular, syntax is NOT the adjoint of semantics. Cratylus, Chomsky, and their 21st century followers can be refuted by looking soberly at the actual practice of mathematics (wherein the construction of sequences of words and of diagrams is pursued with great care for the purpose of communication. That syntax is only remotely dependent on the structure of the content that is to be communicated).

    Both of the functors

    ?----Syntax---> theories ----Semantics--->Large categories

    are needed. The domain category of the first can be chosen in various useful ways: sketches or diagrams of signatures et cetera.

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeMar 1st 2010

    Hmm. I agree that "syntax" ideally refers not to small categories but to their presentations, which is of course the POV taken at type theory. However, I'm not sure it follows that syntax isn't the adjoint of semantics. I would tend to omit to write the inclusion of small categories in large ones, and consider as interesting the right adjoint of the functor from presentations to small categories.

    Actually, I'm not sure how much I believe that 'syntax' and 'semantics' are really functors at all. I would be more inclined, intuitively, to regard 'syntax' as just referring to the presentations themselves, prior to any relationship with categories, and 'semantics' as referring to the entire adjoint pair.

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeFeb 2nd 2012

    I have added a pointer to Bob Harper’s book to type theory. In the course of this I ended up re-ordering the list of references there by type to make it clearer what to read why.

    Experts please check and expand.

    • CommentRowNumber19.
    • CommentAuthorzskoda
    • CommentTimeFeb 2nd 2012
    • (edited Feb 2nd 2012)

    May I reiterate question on a related book: if somebody has a correct eletronic version of Taylor’s Practical foundations of mathematics (e.g. this does not render correctly, test case for your file will be lemma 6.5.3 and the text below). There are many electronic copies available online but neither of them renders typographically in formulas which are abundant.

    P.S. it seems there is one now.

    • CommentRowNumber20.
    • CommentAuthorfpaugam
    • CommentTimeFeb 2nd 2012
    • (edited Feb 2nd 2012)
    Sorry for interrupting with a very naive question, but how can i understand the type theory foundations basing myself on category theoretical foundations (a la Lawvere, using doctrines, say)?

    I have seen some cartesian closed categories somewhere here, but how may type theory be completely formulated in categorical logic terms?
    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 2nd 2012

    I think you can say that type theory is a precise syntactic language for describing theories (with “generators and relations”) in certain doctrines. It works better (or, at least, it is better known) for some doctrines than others. Theories in doctrines such as finite products, finite limits, regular categories, exact categories, coherent categories, Heyting categories, pretoposes, cartesian closed categories, elementary toposes, and locally cartesian closed categories are all well-described using type theories. With homotopy type theory, we can also handle locally cartesian closed (,1)-categories. Doctrines such as monoidal categories are not as well-described, although there exist type theories related to them such as “linear logic”.

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeFeb 2nd 2012
    • (edited Feb 2nd 2012)

    Some aspects of what Mike just said are scattered about in entries related to type theory. But it would be nice to have a more comprehensive remark as #21 in the entry “type theory” itself.

    Would you have time for that?

    • CommentRowNumber23.
    • CommentAuthorfpaugam
    • CommentTimeFeb 2nd 2012
    Thanks for the hints, Mike. May one formalize type theory itself by using things like sketches (more specifically, some classes of limit and colimit cones)? I see sketches as a kind of syntax (a la Ehresmann) for theories. In the examples you cite, you may describe the corresponding doctrines, as you know, as 2-categories of categories with given types of cones and cocones (that may or may not be limit and colimit cones).

    How do you describe, for example, finite product theories using type theory? I will look at the type theory page.
    • CommentRowNumber24.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 3rd 2012

    The usual notion of sketch doesn’t handle the doctrines of cartesian closed categories, locally cartesian closed categories, or elementary toposes. One might imagine a more general notion of sketch which does, but I don’t know if anyone has written one down.

    Type theory also goes beyond merely defining a theory, but additionally gives a syntactic and computational presentation of the classifying category of the theory (the category that it “presents”), hence of a reasoning that is valid for any model of that theory in any category.

    The pages internal logic and context have good descriptions of describing theories in type theory, such as the theory of groups.

    • CommentRowNumber25.
    • CommentAuthorfpaugam
    • CommentTimeFeb 3rd 2012
    • (edited Feb 3rd 2012)
    I see... Excellent! Thanks for the reference.
    • CommentRowNumber26.
    • CommentAuthorfpaugam
    • CommentTimeFeb 4th 2012
    • (edited Feb 4th 2012)
    I read the references.

    About topoi and cartesian closed categories, i have a remaining question. A cartesian closed category may be seen as a category with finite products that has internal homomorphisms. Being cartesian closed is thus a property here. One defines cartesian closed categories as a subdoctrine of cartesian categories (finite product) with an additional property. This is easy to explain in the metalanguage of categories, no?

    Also, topoi may be defined as sheaf categories, that are described as model categories for sketches (those given by nerves of coverings), or categories with an additional property (left exact localizations). So these are a subdoctrine of the doctrine of categories.

    I don't understand why one wants to have a more precise syntax for cartesian closed categories and topoi. Using sketches, we define the cartesian ones, and proceed with that. Sorry for being so naive, but why is it so important to define a syntax for these objects that are defined by taking known ones, and putting some ---properties--- on them.

    Another example i have in mind is the definition of k-monoidal $(\infty,n)$-categories, as $E_k$ higher categories, by induction: you first define monoidal $(\infty,1)$-categories as models of the theory of monoids in the finite product $(\infty,1)$-category of $(\infty,1)$-categories, and proceed to define higher ones by putting $k$ compatible monoidal structures using models of the theory of monoids in the monoidal (cartesian?) category of monoidal categories. This gives a definition, but to have a real syntax, one needs the theorem that says that these are the same as $E_k$ higher categories. We thus get this way the doctrine of monoidal categories.

    It is very easy to define theories by these kinds of inductive methods, and i would like to think of this method (in the metalanguage of n-categories) as the definition of a kind of generalized syntax for the doctrine to be constructed. Giving a true syntax in all the above example may be really very hard, and i tend to prefer the inductive definition of the doctrine, using subdoctrines given by properties, and inductive constructions (generalizing Lawvere tensor products of theories).

    Why is this approach to syntax not satisfactory from a ``foundational'' perspective?
    • CommentRowNumber27.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 5th 2012

    I wasn’t saying that “the theory of cartesian closed categories” can’t be defined in the doctrine of, say, (2,1)-categories with finite products and involution (it can’t be defined in the doctrine of 2-categories with finite products, since the internal-hom is contravariant). What I was saying is that theories in the doctrine of cartesian closed categories cannot be presented by the standard notion of sketch.

    • CommentRowNumber28.
    • CommentAuthorfpaugam
    • CommentTimeFeb 5th 2012
    Could you explain this with more details?

    Why do you need an involution?

    Is there a way to give a meaning to the notion of ``property''? For example, one defines cartesian closed categories as categories with finite products (the notion of Kan extension is given in the metalanguage, so we can discuss about limits) with the additional property that they have internal homomorphisms. It is not completely necessary to encode this in an additional syntax for the theories: this is a property.

    I saw in the section on internal logic that properties may be encoded by subobjects. So the doctrine of cartesian closed categories is a subdoctrine of that of categories with finite products. Why isn't this satisfactory? I guess it is because you want to give constraints on how you specify subdoctrines by some conditions... I am a bit lost.

    I tend to think that, if one wants to define theories using the metalanguage of higher categories, one needs at least to have a notion of limit (Kan extensions) given from the beginning in the metalanguage (to define theories using sketches), and that of sub-doctrine. For example, categories with finite products are just defined because we know what a finite product is (this is the sketchy approach) and then, cartesian closed categories are those that have internal hom. This is a subdoctrine defined by a categorical condition.

    What is the problem with what i say over here? Is there a foundational hole in this approach? One may probably be able to define the full metalanguage of higher categories using only that of categories. Why isn't it possible to ground mathematics on these kind of considerations?

    Sorry if my question is stupid. If this is the case, don't hesitate to show me why.
    • CommentRowNumber29.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 6th 2012

    The internal-hom of a cartesian closed category C is a functor Cop×CC, in the same way that the cartesian product is a functor C×CC. The doctrine in which a theory is described specifies the allowable “arities” of the “operations” in that doctrine. Thus, in order to have a doctrine of cartesian closed categories, there must be some sort of “arity” for “binary operations with one covariant and one contravariant input”. The obvious way to model contravariance is to have an involution CCop existing at the same level as the operation CC×C. Thus, the natural place in which to talk about “cartesian closed objects” is a 2-category with finite products and an involution — hence, the theory of cartesian closed categories lives in the doctrine of such 2-categories.

    Perhaps the point is that a “subdoctrine” of a doctrine D must also be itself a doctrine, not just an arbitrary subcategory of the category of theories in D?

    • CommentRowNumber30.
    • CommentAuthorDavidRoberts
    • CommentTimeFeb 6th 2012
    • (edited Jun 4th 2012)

    @Zoran

    P.S. it seems there is one now

    where? Email me if it shouldn’t be advertised on a public forum.

    I’ve always wanted to have a good browse, and the online version is so poor it isn’t worth trying.

    EDIT: I take this back.

    • CommentRowNumber31.
    • CommentAuthorfpaugam
    • CommentTimeFeb 6th 2012
    • (edited Feb 6th 2012)
    I see, so one wants also a ``generator and relation'' kind of look at theories of the subdoctrine, and this is why we need the involution.

    Defining cartesian categories as theories in the doctrine of cartesian 2-categories is not very useful, from my point of view, because we are eating our own functorial arm doing that, no? ;-)

    Ok. What i would like to know is when a subcategory of the theories of a given doctrine form a doctrine. What kind of condition can we impose? It seems to me that when one is able to write down a condition with finitely many words, this should give a subdoctrine, but perhaps i am too optimistic.

    I think it will be very hard to give a presentation of every concretely given doctrine (like cartesian closed categories) as given by a higher finitary monad with arities on n-Cat. On each case, it is at least a hard exercice, and potentially, a good thesis subject.

    If one takes the sketch viewpoint (that i prefer to work with higher doctrines), one can define categories with finite products from scratch as a subdoctrine of categories, given by those that have finite products, with morphisms that commute with products, and then impose the existence of inner homomorphisms also by a condition of commutation to a limit somewhere (representability condition for the inner hom). You only need the metalanguage of higher categories with limits to define these doctrines, as full subdoctrines of the (n+1)-category of n-categories (supposed to exist in the metalanguage).

    Isn't it ok? I guess the problem is that defining things this way, we don't really have a syntax in the classical sense... This is why you want the duality: to have a small syntax for the theories. Right?

    If i understand things well, it seems that giving a syntax is very similar to the delooping operation in topology, and this is exactly what i want to avoid doing each time, since we have already done that when defining higher categories from (model) categories with simplicial methods. I don't want to remake a delooping machine for each example, and prefer to use the universal one, that is given by (\infty,n)-categories.

    It seems to me that trying to give an explicit syntax for theories of a subdoctrine of n-Cat defined by limit and commuting diagram conditions (sketch approach) is like delooping the simple definition of the given theory (e.g. Cartesian closed category is easy to define) to get a definition where one knows everything about the diagrams in play. It is impossible to do when we work with homotopical theories like those given by (\infty,1)-doctrines.

    Did i miss the point? Sorry for being so curious... Don't hesitate to tell me if there is something i did not catch in the problematic of foundational mathematics. I really don't see where is the problem there. I know my questions are naive, but if they get an answer, it could help to understand what a doctrine is.
    • CommentRowNumber32.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 6th 2012

    Defining cartesian categories as theories in the doctrine of cartesian 2-categories is not very useful, from my point of view, because we are eating our own functorial arm doing that, no? ;-)

    You mean, because we used the word “cartesian” twice? I’m not sure what other doctrine you could define cartesian categories in. At some point, you’re going to need some input about what a “product” actually means. It doesn’t seem any better to me to define cartesian categories as a subcategory of Cat using “the metalanguage of higher categories with limits” as you say — in both cases we’re using a notion of limit to define the theory of products.

    What i would like to know is when a subcategory of the theories of a given doctrine form a doctrine. What kind of condition can we impose? It seems to me that when one is able to write down a condition with finitely many words, this should give a subdoctrine, but perhaps i am too optimistic.

    Well, first of all, whether a subcategory forms a doctrine is going to depend on what eka-doctrine you want it to be a doctrine in. (By “eka-doctrine” I mean doctrine at one higher level up.) For instance, to take the example we’ve been looking at, cartesian categories (or, more precisely, cartesian objects) are a doctrine in the eka-doctrine of cartesian 2-categories, while the subcategory of cartesian closed categories is not a doctrine in that eka-doctrine, but it is one in some larger eka-doctrine (cartesian 2-categories with duality involution). Similarly, Cat is the category of theories for the “doctrine of objects”, which exists in the simplest possible eka-doctrine, but if we want CartCat to be a sub-doctrine on Cat we have to expand the eka-doctrine to at least cartesian 2-categories.

    Since we know from experience that any condition we can write down in finitely many words can be described in first-order logic, it seems likely that if we are willing to expand the eka-doctrine to include all of first-order logic, then your guess would become correct.

    There’s also the question of whether our subcategories of theories are full. The 2-category of cartesian closed categories, for instance, is not a full sub-2-category of the category of cartesian categories, since we want to consider only the functors that preserve internal-homs as well as products.

    I think it will be very hard to give a presentation of every concretely given doctrine (like cartesian closed categories) as given by a higher finitary monad with arities on n-Cat.

    I don’t think it will be that hard, once we have good machinery in place. It’s easy when n=0 and n=1, where the machinery is pretty much already in place. People like Lurie have been working on the case n=(,1), and maybe the machinery is basically in place there too, I’m not sure.

    Also, beware that cartesian closed categories are not presented by a 2-monad on Cat, only on Catg (the (2,1)-category of categories, functors, and natural isomorphisms). This is due to contravariance again.

    It seems to me that trying to give an explicit syntax for theories of a subdoctrine of n-Cat defined by limit and commuting diagram conditions (sketch approach) is like delooping the simple definition of the given theory

    I don’t understand what it has to do with delooping. I see a sketch as basically an alternative way to describe the explicit syntax for a theory (in the case when the doctrine involves only limits and colimits). For instance, the explicit syntax of the theory of groups has one type G and a binary operation G×GG (and some other stuff). When we describe that theory with a sketch, the type G becomes an object of the sketch, and the operation becomes a morphism, with the arity of the morphism described by making its domain be an object stipulated to be the product G×G.

    • CommentRowNumber33.
    • CommentAuthorfpaugam
    • CommentTimeFeb 7th 2012
    • (edited Feb 7th 2012)

    The lego game of eka-doctrine looks quite interesting… I’m sure the situation is not far from being clarified by someone, about n-monads, and presentations of higher doctrines, but probably not by me, because this looks a bit hard.

    At some point, you’re going to need some input about what a “product” actually means. It doesn’t seem any better to me to define >cartesian categories as a subcategory of Cat using “the metalanguage of higher categories with limits” as you say — in both cases >we’re using a notion of limit to define the theory of products.

    I think your are touching exactly the point that is problematic in a foundational perspective on doctrines. I don’t have a clever answer to the question: what is a product?

    For me, a product is a universal cone for a finite discrete diagram: a limit. So categories with products are categories that have these kinds of limits for all finite diagrams. But i guess this is not foundational enough, and i understand that.

    What is your prefered definition of a product, from a foundational perspective? :-)

    • CommentRowNumber34.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 7th 2012

    For me, a product is a universal cone for a finite discrete diagram: a limit. So categories with products are categories that have these kinds of limits for all finite diagrams.

    That seems perfectly foundational to me.

    • CommentRowNumber35.
    • CommentAuthorUrs
    • CommentTimeMay 9th 2012
    • (edited May 9th 2012)

    Some editorial points at type theory:

    a)

    There is the following paragraph, which I guess contains a typo:

    The description given below is a somewhat simplified one, in that we identify objects of the category with single objects, rather than contexts. This is strictly speaking only okay in type theories with a dependent sum operation, which allows us to reinterpret every context as a single type.

    The highlighting is mine. And: the highlighted “objects” wants to by “types”, right?

    b)

    In the References-section I renamed “Jean-Yves Giraud” to “Jean-Yves Girard”

    c)

    The section An introduction to category theorists is pretty good.

    I am wondering about strengthening it in the following ways:

    1. Can we rename the section from “Introduction for category theorists” to something that more explicitly makes the point that type theory is not only something that category theorists can understand in their context, but that they also want to understand? Something like “Type theory as a formal language for category theory” or the like.

    2. What would be references to support this section? I have added a link to a page Category theory and type theory by Paul Taylor, but I would like to give the reader more pointers to the literature here.

      For instance that adjunction between type theories and categories: what is a reference, if any, that discusses this?

      [edit: I have found more on this in Taylor’s book here]

      Or, what’s a reference that discusses in detail the relation between type construction and universal properties in category theory? I would like to see an explicit discussion of the type-theoretic quadruple

      1. creation
      2. introduction
      3. elimination
      4. computation

      related to category theory.

    d)

    More on the first item in c): what I am after is more answers to those readers who may say the following:

    I don’t care about teaching mathematics to a computer, or related applications of type theory. I am a category theorist or at least in my work I make heavy use of category theory, and I want to know: what can type theory do for me? If anything.

    Maybe dependent type theory is telling me that I can prove better theorems about category theory or its applications if I emphasize the point of view of slice categories and base change between them over a more ’global’ point of view. But which theorems would that be? What do I gain, if anything, by reading your ’Introduction to type theory for category theorists’ if my motivation is not just to understand type theory for its own sake?

    This is roughly a question that I am personally being confronted with, and I think it is a good question. I know partial replies to this. But I feel I could improve on those. All help would be appreciated.

    For instance with the discussion at contractible type one can say to a higher category theorist: “Look, here is a neat way to reformulate (-1)-truncation in an -category which you had missed so far, because you didn’t systematically think in terms of (ff*f). Similarly for statements about weak equivalences etc. This actually helps seeing some little facts that you had missed so far, so it’s good to know”.

    Stuff like this. Eventually I would want a list or comprehensive account of answers to such “What can type theory actually do for (higher) category theory?” questions (as opposed to just: “Look, we can reformulate (higher) category theory. Isn’t this fun?”)

    • CommentRowNumber36.
    • CommentAuthorUrs
    • CommentTimeMay 9th 2012

    Re point d) above:

    for instance Paul Taylor here (scroll down to section 2.5) asserts:

    However, purely categorical textbooks cover many pages with diagrams expressing arguments that could be written much more briefly [in type theory].

    I am not sure if the text fully supports this claim at this point. But this would be what I am after here: to make explicit where using type theory is genuinely useful as a tool in category theory or the like, as something that gives you insight or increases clarity in a way that couldn’t be achieved without.

    • CommentRowNumber37.
    • CommentAuthorMike Shulman
    • CommentTimeMay 9th 2012

    a) yes, that’s a typo; I fixed it.

    c1) Sure, how about just “As a formal language for category theory”?

    c2) I would also like to see such an explicit discussion! Understanding introduction/elimination for positive/negative types quite generally in terms of universal properties for mapping out/in was a revelation to me precisely because I hadn’t read anyone explaining it well before. Which is to say, I don’t know good references. Bart Jacobs’ book is okay, but I find it too scattershot and doesn’t make the guiding principles explicit enough.

    d) Yes, we should start collecting lists of these. One classical example I am fond of, which I used in my talks at Swansea, is that the proof that inverses in a group are unique works quite well in type theory and therefore internalizes to any finite product category. But if you try to prove by manipulating elements that the antipode of a Hopf algebra is unique, you are in for a world of pain.

    There are some more classical examples in the Elephant, scattered throughout part D and a few places earlier as well.

    There was a case here on the Forum a while back where some question about (,1)-limits came up that I found it easier to prove using homotopy type theory, maybe we could find it and cite it or copy it?

    I also remember back when were discussing the pasting law for (,1)-pullbacks, you suggested that we could do it in homotopy type theory for an (,1)-topos, and then interpret it in any (,1)-category with pullbacks via the Yoneda embedding.

    • CommentRowNumber38.
    • CommentAuthorUrs
    • CommentTimeMay 10th 2012
    • (edited May 10th 2012)

    Thanks for these reactions!

    Okay, good. So let’s start collecting such a list.

    I did start such a page today, optimistically titled HoTT methods for homotopy theorists, but it is just a first rough place to contain some notes that I had time for today. I will try to expand on that tomorrow.

    I’ll look again at your argument about uniqueness of inverses, that sounds like a great example.

    Concerning that discussion of (,1)-limits you are alluding to, are you thinking of the discussion of stabilizer -groups about which you posted some impressive HoTT analysis here?

    The pasting law of pullbacks is also a good example. I’ll include that in the above page. Maybe I’ll make some section “Basic facts of homotopy theory made even simpler in HoTT” or the like. Because, while very nice, I would like to separate that from facts that a homotopy theorist might actually consider news.

    • CommentRowNumber39.
    • CommentAuthorUrs
    • CommentTimeMay 10th 2012

    Mike, I looked again at your notes but I don’t seem to find it: where do you have that discussion of inverses in groups that you are referring to?

    • CommentRowNumber40.
    • CommentAuthorUrs
    • CommentTimeMay 10th 2012

    I have considerably expanded the Idea-section at type theory.

    • CommentRowNumber41.
    • CommentAuthorMike Shulman
    • CommentTimeMay 10th 2012

    Hmm, maybe I only said it out loud. Anyway, what I said above is basically all there is.

    • CommentRowNumber42.
    • CommentAuthorMike Shulman
    • CommentTimeMay 10th 2012

    (And yes, the stabilizer -groups is what I was thinking of.)

  1. I have considerably expanded the Idea-section at type theory.

    Maybe from type theory there could be pointers to positive type / negative type since in Swansea I got the impression that it is (at least didactically) good to know them.

    • CommentRowNumber44.
    • CommentAuthorUrs
    • CommentTimeMay 10th 2012

    Go ahead, Stephan, and add those pointers where it makes sense!

  2. @Zoran

    P.S. it seems there is one now

    where? Email me if it shouldn’t be advertised on a public forum.

    I’ve always wanted to have a good browse, and the online version is so poor it isn’t worth trying.

    I am interested in this one, too.

  3. Maybe from type theory there could be pointers to positive type / negative type since in Swansea I got the impression that it is (at least didactically) good to know them.

    I linked the beginning of section As a formal language for category theory

    ”One way to look at type theory, from the point of view of a category theorist, is as a syntax for describing the construction of objects and morphisms in a category.”

    This non existing page should then remark that one way of classifying types is via their ”construction” - or more precisely via their constructors. However the beginnings of positive type/negative type do not indicate that eliminators are type constructors but somehow suggest that ”constructor” and ”eliminator” are thought of complementary notions.

    • CommentRowNumber47.
    • CommentAuthorMike Shulman
    • CommentTimeMay 11th 2012

    There is a potential confusion in that the word “constructor” can refer both to the formation rule by which we define new types (e.g. given types A and B there is a type A×B) and to the introduction rule by which we define terms belonging to those types (e.g. given a:A and b:B there is a term (a,b):A×B). The latter case is what is dual/complementary to the elimination rule. Perhaps this should be clarified somewhere (or everywhere).

    • CommentRowNumber48.
    • CommentAuthorMike Shulman
    • CommentTimeJun 2nd 2012

    I added a link to the types mailing list to the page type theory.