10
$\begingroup$

As I’m being introduced and learning about these theories, I wanted to ask your help in putting things in perspective.

My impression at the moment is that Type is a more abstract theory than Category and that Topos is a more specific theory than Category.

And when I say abstract, I’m getting the impression that I could phrase that as a theory with many axioms and few derivations where when I say specific I’m getting the impression that I could phrase that to mean few axioms and many derivations

Are these impressions accurate?

If so, where does Homotopy Type Theory fit on this scale; does it make sense as in the title (more abstract than Category but more specific than Type?)

(EDIT: any commentary or discussion on how you personally view these theories along any metric would be very welcome and useful to me.)

$\endgroup$
9
  • $\begingroup$ This seems too subjective. Try to make your question more precise. $\endgroup$
    – Pedro ♦
    Aug 5, 2016 at 16:52
  • $\begingroup$ I've listed my definitions for "abstract" and "specific" in terms of judging these theories. What might I be more precise with that would help make this question less subjective to you? $\endgroup$
    – Ricardo J Rademacher
    Aug 5, 2016 at 17:02
  • $\begingroup$ The things I think make this unclear are A) type theories are formal systems akin to first order logic, while categories are a kind of structure, and B) the same deductive systems can often be phrased in equivalent "more axioms, fewer rules" and "more rules, fewer axioms" ways, making it a rather poor criterion for "abstractness". $\endgroup$
    – Malice Vidrine
    Aug 5, 2016 at 17:12
  • $\begingroup$ "type theories are formal systems akin to first order logic, while categories are a kind of structure," what is the difference between a formal system and a structure? At the moment, I see them as equivalent. $\endgroup$
    – Ricardo J Rademacher
    Aug 5, 2016 at 17:17
  • $\begingroup$ @RicardoJRademacher you said "when I say specific I’m getting the impression that I could phrase that to mean few axioms and many derivations... Topos is a more specific theory than Category" so how could Topos theory be more specific (according with your definition) when topos theory provide a lot of additional axioms with respect to Category theory? $\endgroup$
    – Giorgio Mossa
    Aug 5, 2016 at 17:17

1 Answer 1

Reset to default
11
$\begingroup$

I believe you are trying to approach the Type Theory-Category Theory duality from the wrong perspective.

Note: In what follows I'll assume that by Category Theory you are referring to the formal system (i.e. axiomatic theory) for categories, not to theory that studies categories a relations between them.

Both Type Theory (TT from here on) and Category Theory (CT) can be thought as abstract theories of functions. Nonetheless they are very different in their spirit: while TT tries to capture function application CT is interested in function composition. This difference produce two very different kind of theories that in my personal opinion can hardly being compared.

Of course there are relation between these two kind of theories: to every type systems (a model of some theory of types) you can associate a category whose objects are contexts while morphisms are terms (i.e. functions in type theoretic language). Composition of morphisms is build through the function application more or less how it is done with set theoretic functions.

On the other hand you can build from any category a type systems whose types are basically the objects of the category and terms are build out of morphisms.

Going to deep in these two construction would require to much space so I suggest you to read this link and some book in categorical logic (I believe that every basic text book treat this kind of stuff).

Hope this helps.

$\endgroup$
5
  • 2
    $\begingroup$ As additional comment: you could reguard Category Theory as more abstract than Topos Theory (since Topos Theory is obtained adding axioms to the ones for categories) and in a very similar way you can reguard (Dependent) Type Theory as more abstract than HoTT (since HoTT is a DTT with more inference rules-axioms), nonetheless I don't think you could compare in a similar manner Category Theory and Type Theory (<irony>more or less because abstractness is not a linear order :D</irony>). $\endgroup$
    – Giorgio Mossa
    Aug 5, 2016 at 18:54
  • 3
    $\begingroup$ Big ups! You captured the spirit of what I was trying to get at without getting bogged down in the semantics: a hierarchical comparison and contrast of these theories and comments like these "TT tries to capture function application CT is interested in function composition." are a HUGE help $\endgroup$
    – Ricardo J Rademacher
    Aug 5, 2016 at 19:21
  • $\begingroup$ And as I told another commentator above, I have a specific problem I need to address and all of these are candidate theories. As such, I want to know which one will give me the more "bang for my buck" by pursuing. So far HoTT is in the lead as a good mix of categorical abstraction but with homotopical specifics while topos for some reason is not resonating with me as a complete theory... category theory with subobject qualifiers sure, but an entire branch? I don't know. $\endgroup$
    – Ricardo J Rademacher
    Aug 5, 2016 at 19:26
  • $\begingroup$ @RicardoJRademacher If you give some details on your specific problems it could help others helping you to find the best suited theory for your applications (apologize for the word game). $\endgroup$
    – Giorgio Mossa
    Aug 6, 2016 at 16:59
  • $\begingroup$ I'm writing up a paper for it right now: 1drv.ms/w/s!ApL4eAFes69nrCgUgcD7OakOK3-Z $\endgroup$
    – Ricardo J Rademacher
    Aug 6, 2016 at 17:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.