3
$\begingroup$

Hello,

I read the paper on groupoid interpretation of type theory by Hofmann and Streicher and I have a question. According to the authors $Tm([[\text{Set}\:[\Gamma]\: ]])$ is the same as $\text{Se}([[\Gamma]])$ but I don't understand because an element of $Tm([[\text{Set}\,[\Gamma]\:]])$ is a pseudo-fonctor (from $[[\Gamma]]$ to GPD) as said page 10 while an element of $\text{Se}([[\Gamma]])$ is a true fonctor (from $[[\Gamma]]$ to Gpd). Have you an idea ?

Best

P.S: I precise that the paper I mention is entitled The Groupoid Interpretation of Type Theory by Martin Hofmann and Thomas Streicher. You can find this article here http://www.mathematik.tu-darmstadt.de/~streicher/ Thanks

Improve this question
$\endgroup$
3
  • 5
    $\begingroup$ Asymptotik, you'll be more likely to get an answer if you give more details. Which paper of Hofmann and Streicher is this? Give a link if you can. Defining the notation would also increase your chances of getting an answer. $\endgroup$
    – Tom Leinster
    Commented Sep 16, 2012 at 18:25
  • 3
    $\begingroup$ Does "groupoid" really need a diaeresis over the "i"? $\endgroup$
    – Sridhar Ramesh
    Commented Sep 17, 2012 at 21:21
  • 1
    $\begingroup$ @Sridhar: I sort of wondered the same thing, but the poster lives in France, where this might be a more customary spelling. (My personal opinion is that diareses are never really needed in English, unless you are under contract with The New Yorker.) $\endgroup$
    – Todd Trimble
    Commented Sep 17, 2012 at 22:03

0

Reset to default

You must log in to answer this question.