# Groupoid interpretation of type theory

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

-
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. –  Tom Leinster Sep 16 '12 at 18:25
Does "groupoid" really need a diaeresis over the "i"? –  Sridhar Ramesh Sep 17 '12 at 21:21
@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.) –  Todd Trimble Sep 17 '12 at 22:03