4
$\begingroup$

What is the internal language of the category Cat of small categories?

I found an article by Glynn Winskel and his student Mario Jose Cáccamo about such calculus! However it is limited to a fragment of Cat. I wonder if there have been further work since the PhD thesis of Cáccamo.

http://www.brics.dk/RS/01/27/

Improve this question
$\endgroup$

1 Answer 1

Reset to default
6
$\begingroup$

You may be interested in Harper and Licata, 2-Dimensional Directed Dependent Type Theory, PDF. I did some abortive work on this myself as well.

Improve this answer
$\endgroup$
6
  • 1
    $\begingroup$ Thank you very much, @Mike. Could you please comment why you think your work on this was not successful? $\endgroup$
    – Bob
    Commented Jul 14, 2014 at 19:19
  • $\begingroup$ I wouldn't say it wasn't successful; I just never got around to finishing it. $\endgroup$
    – Mike Shulman
    Commented Jul 15, 2014 at 3:17
  • $\begingroup$ Sorry, Mike. I misunderstood the meaning of the word "abortive" that you used in your answer. $\endgroup$
    – Bob
    Commented Jul 16, 2014 at 20:36
  • $\begingroup$ @Bob: Well, according to dictionary.reference.com/browse/abortive, the first definition is "unsuccessful", whereas the closest definition to what I meant is the third one, "imperfectly developed". So your interpretation was quite reasonable and perhaps my word choice was poor. (-: $\endgroup$
    – Mike Shulman
    Commented Jul 17, 2014 at 5:40
  • $\begingroup$ This paper and your work are from the point of view of logic. But, from a computational point of view, if we see 0-cells as types and 1-cells as terms-in-context, then what are 2-cells and what are horizontal and vertical compositions of 2-cells? Thank you in advance for any light you can bring. $\endgroup$
    – Bob
    Commented Jul 30, 2014 at 12:08

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .