Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeMay 12th 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexWhile the lab is down, I'll collect some stuff here, also to discuss it. So I am trying to identify in the literature a precise and coherent statement of the supposed adjunction / partial equivalence between "type theories" and "categories". In section 8.4.C of [[Practical Foundations]] is announced the following, which would be part of that statement: * Every category with a rooted class of [[display maps]] is equivalent to a [[category of contexts]] of (and now I think it can read:) a [[dependent type theory]]. Unfortunately the online version of the book breaks off right after this announcement, and I don't have the paper version available at the moment. Also, that section 8.4.C starts with the word "Conversely". But where is the converse statement, actually?

   While the lab is down, I’ll collect some stuff here, also to discuss it.

   So I am trying to identify in the literature a precise and coherent statement of the supposed adjunction / partial equivalence between “type theories” and “categories”.

   In section 8.4.C of Practical Foundations is announced the following, which would be part of that statement:

   • Every category with a rooted class of display maps is equivalent to a category of contexts of (and now I think it can read:) a dependent type theory.

   Unfortunately the online version of the book breaks off right after this announcement, and I don’t have the paper version available at the moment.

   Also, that section 8.4.C starts with the word “Conversely”. But where is the converse statement, actually?

2. • CommentRowNumber2.
   • CommentAuthorTobyBartels
   • CommentTimeMay 13th 2012
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexThe converse is the construction of the category $Cn_L$ from a theory $L$.

   The converse is the construction of the category $Cn_L$ from a theory $L$.

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeMay 14th 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexBut what is the converse _statement_ about that?

   But what is the converse statement about that?

4. • CommentRowNumber4.
   • CommentAuthorzskoda
   • CommentTimeMay 14th 2012
   • PermaLink
   Author: zskoda
   Format: MarkdownItexAny qualifications on size issues here ?

   Any qualifications on size issues here ?

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeMay 15th 2012
   • (edited May 15th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexsorry for the multiplication of threads, but I decided to create the entry finally under the title _[[relation between type theory and category theory]]_. So there is now a [new thread](http://nforum.mathforge.org/discussion/3818/relation-between-type-theory-and-category-theory/#Item_1) on that.

   sorry for the multiplication of threads, but I decided to create the entry finally under the title relation between type theory and category theory. So there is now a new thread on that.

6. • CommentRowNumber6.
   • CommentAuthorTobyBartels
   • CommentTimeMay 16th 2012
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexAs I read it, Urs, the converse statement is simply that $Cl_L$ exists, perhaps the theorem that it has a rooted class of displays. Given a theory, we get such a category; conversely, every such category arises in this way.

   As I read it, Urs, the converse statement is simply that $Cl_L$ exists, perhaps the theorem that it has a rooted class of displays. Given a theory, we get such a category; conversely, every such category arises in this way.

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeMay 16th 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexToby, thanks. Okay, so originally I was hoping for a bit more. But meanwhile I saw that this more is discussed elsewhere, in the literature which I have now listed at [[relation between type theory and category theory]].

   Toby, thanks. Okay, so originally I was hoping for a bit more. But meanwhile I saw that this more is discussed elsewhere, in the literature which I have now listed at relation between type theory and category theory.