Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeMay 3rd 2014
   • (edited May 3rd 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexMike kindly wrote _[[homotopytypetheory:model of type theory in an (infinity,1)-topos]]_ with an explicit statement of how univalent Tarskian types-of-types have semantics by object classifiers in general $\infty$-toposes. I have added a brief pointer to this to some relevant $n$Lab entries: to _[[homotopy type theory]]_, to _[[relation between category theory and type theory]]_, to _[[(infinity,1)-topos]]_ and to _[[elementary (infinity,1)-topos]]_.

   Mike kindly wrote model of type theory in an (infinity,1)-topos (homotopytypetheory) with an explicit statement of how univalent Tarskian types-of-types have semantics by object classifiers in general $\infty$-toposes.

   I have added a brief pointer to this to some relevant $n$Lab entries: to homotopy type theory, to relation between category theory and type theory, to (infinity,1)-topos and to elementary (infinity,1)-topos.