MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top


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 ?


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 Thanks

share|cite|improve this question
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

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.