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 19th 2012
   • (edited May 19th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexHere is a kind of summary of the little fact that Mike and I have been discussing in another thread [here](http://nforum.mathforge.org/discussion/3048/stack-semantics/?Focus=31533#Comment_31533). I tought this is nice and we should discuss this a bit more, it feels like there might be some nice implications here, at least conceptually. So I am probably going to post this to the $n$Café in a little while. For them moment, I post a preliminary version here. [edit: I have now posted this to the $n$Café [here](http://golem.ph.utexas.edu/category/2012/05/segalcompleteness_and_univalen.html)] --- Here is a charming statement: * _[Univalence](http://ncatlab.org/nlab/show/complete%20Segal%20space#CompleteSegalSpaces) in [homotopy type theory](http://ncatlab.org/nlab/show/homotopy%20type%20theory) is a special case of the [Segal-completeness condition](http://ncatlab.org/nlab/show/complete%20Segal%20space#CompleteSegalSpaces) in [internal (∞,1)-category theory](http://ncatlab.org/nlab/show/category+object+in+an+%28infinity%2C1%29-category) ._ Do you see it? Once you know what these terms mean this is pretty obvious, once stated. But it seems not to have been stated before. I now briefly spell this out and give further pointers. This might be the beginning of a nice story. I am posting this here in the hope of discussing it a bit more. Consider some ambient [(∞,1)-topos](http://ncatlab.org/nlab/show/%28infinity,1%29-topos) and inside it an [internal (∞,1)-category](http://ncatlab.org/nlab/show/category+object+in+an+%28infinity%2C1%29-category), hence a [complete Segal space object](http://ncatlab.org/nlab/show/complete%20Segal%20space) $X_\bullet$. Its [1-skeleton](http://ncatlab.org/nlab/show/simplicial%20skeleton), on which I will focus attention here, looks as follows (in this and the following formulas I display on the left the [syntax](http://ncatlab.org/nlab/show/type%20theory) and on the right its [semantics](http://ncatlab.org/nlab/show/categorical%20semantics), see _[HoTT methods for homotopy theorists](http://ncatlab.org/nlab/show/HoTT%20methods%20for%20homotopy%20theorists)_ if you are a homotopy theorist and need more background): the object of morphisms $X_1$ sits by the source-and-target map $(d_0,d_1)$ over the object of objects $X_0$ $$ [x,y : X_0 \vdash X_1(x,y) : Type] \;\;\;\;\;\;\;\;\;\;\; \left[ \array{ X_1 \\ \downarrow^{\mathrlap{(d_0, d_1)}} \\ X_0 \times X_0 } \;\;\;\;\; \right] $$ and the identity-assigning map $s_0$ is a diagonal section $$ [ x : X_0 \vdash s_0(x) : X_1(x,x)] \;\;\;\;\;\;\;\;\; \left[ \array{ X_0 &&\stackrel{s_0}{\to}&& X_1 \\ & {}_{\mathllap{\Delta}}\searrow && \swarrow_{\mathrlap{(d_0,d_1)}} \\ && X_0 \times X_0 } \right] \,. $$ Syntactically, the [recursion principle / simple elimination rule](http://ncatlab.org/nlab/show/inductive+type#RecursionRules) for the [inductive](http://ncatlab.org/nlab/show/inductive+type) [identity types](http://ncatlab.org/nlab/show/identity%20type), and semantically the ([acyclic](http://ncatlab.org/nlab/show/acyclic+fibration) [cofibrations](http://ncatlab.org/nlab/show/cofibration) $\perp$ [fibrations](http://ncatlab.org/nlab/show/fibration))-[weak factorization system](http://ncatlab.org/nlab/show/weak%20factorization%20system), says that this section factors through the [identity type](http://ncatlab.org/nlab/show/identity%20type) $[x,y : X_0 \vdash (x = y) : Type]$ (syntactically) respectively the [path space object](http://ncatlab.org/nlab/show/path%20space%20object) $X_0^I \to X_0 \times X_0$ (semantically): $$ [ x,y : X_0 \vdash \hat s_0(x,y) : (x = y) \to X_1(x,y)] \;\;\;\;\;\;\; \left[ \array{ X_0 &\stackrel{s_0}{\to}& X_1 \\ \downarrow &\nearrow_{\mathrlap{\hat s_0}}& \downarrow \\ X_0^I &\to& X_0 \times X_0 } \right] \,. $$ Now, [Segal-completeness](http://ncatlab.org/nlab/show/complete%20Segal%20space) of $X_\bullet$ is the statement that this $\hat s_0$ exhibits the inclusion of the [core](http://ncatlab.org/nlab/show/core), hence of those morphisms $f \in X_1$ that are equivalences under the composition operation of $X_\bullet$. Specifically, consider the case that $X_\bullet$ is the _universal_ small internal category object, equivalently the small reflection of the ambient $(\infty,1)$-topos into itself, equivalently the classfier of the small [codomain fibration](http://ncatlab.org/nlab/show/codomain%20fibration), equivalently its [stack semantics](http://ncatlab.org/nlab/show/stack%20semantics), or whatever you want to call it, that whose 1-skeleton is $$ \array{ [A,B : Type \vdash A \to B : Type] \\ {}^{\mathllap{d_0}}\downarrow \uparrow^{\mathrlap{s_0}} \downarrow^{\mathrlap{d_1}} \\ Type } \,, $$ where "$Type$" denotes the small [universe](http://ncatlab.org/nlab/show/universe%20in%20a%20topos) / small [object classifier](http://ncatlab.org/nlab/show/object%20classifier%20in%20an%20%28infinity,1%29-topos). Then the Segal-completeness condition of this internal category object is the [univalence](http://ncatlab.org/nlab/show/univalence) condition on $\widetilde Type \to Type$.

   Here is a kind of summary of the little fact that Mike and I have been discussing in another thread here. I tought this is nice and we should discuss this a bit more, it feels like there might be some nice implications here, at least conceptually. So I am probably going to post this to the $n$Café in a little while. For them moment, I post a preliminary version here.

   [edit: I have now posted this to the $n$Café here]

   ---

   Here is a charming statement:

   • Univalence in homotopy type theory is a special case of the Segal-completeness condition in internal (∞,1)-category theory .

   Do you see it? Once you know what these terms mean this is pretty obvious, once stated. But it seems not to have been stated before.

   I now briefly spell this out and give further pointers. This might be the beginning of a nice story. I am posting this here in the hope of discussing it a bit more.

   Consider some ambient (∞,1)-topos and inside it an internal (∞,1)-category, hence a complete Segal space object $X_\bullet$. Its 1-skeleton, on which I will focus attention here, looks as follows (in this and the following formulas I display on the left the syntax and on the right its semantics, see HoTT methods for homotopy theorists if you are a homotopy theorist and need more background):

   the object of morphisms $X_1$ sits by the source-and-target map $(d_0,d_1)$ over the object of objects $X_0$

   $$[x,y : X_0 \vdash X_1(x,y) : Type] \;\;\;\;\;\;\;\;\;\;\; \left[ \array{ X_1 \\ \downarrow^{\mathrlap{(d_0, d_1)}} \\ X_0 \times X_0 } \;\;\;\;\; \right]$$

   and the identity-assigning map $s_0$ is a diagonal section

   $$[ x : X_0 \vdash s_0(x) : X_1(x,x)] \;\;\;\;\;\;\;\;\; \left[ \array{ X_0 &&\stackrel{s_0}{\to}&& X_1 \\ & {}_{\mathllap{\Delta}}\searrow && \swarrow_{\mathrlap{(d_0,d_1)}} \\ && X_0 \times X_0 } \right] \,.$$

   Syntactically, the recursion principle / simple elimination rule for the inductive identity types, and semantically the (acyclic cofibrations $\perp$ fibrations)-weak factorization system, says that this section factors through the identity type $[x,y : X_0 \vdash (x = y) : Type]$ (syntactically) respectively the path space object $X_0^I \to X_0 \times X_0$ (semantically):

   $$[ x,y : X_0 \vdash \hat s_0(x,y) : (x = y) \to X_1(x,y)] \;\;\;\;\;\;\; \left[ \array{ X_0 &\stackrel{s_0}{\to}& X_1 \\ \downarrow &\nearrow_{\mathrlap{\hat s_0}}& \downarrow \\ X_0^I &\to& X_0 \times X_0 } \right] \,.$$

   Now, Segal-completeness of $X_\bullet$ is the statement that this $\hat s_0$ exhibits the inclusion of the core, hence of those morphisms $f \in X_1$ that are equivalences under the composition operation of $X_\bullet$.

   Specifically, consider the case that $X_\bullet$ is the universal small internal category object, equivalently the small reflection of the ambient $(\infty,1)$-topos into itself, equivalently the classfier of the small codomain fibration, equivalently its stack semantics, or whatever you want to call it, that whose 1-skeleton is

   $$\array{ [A,B : Type \vdash A \to B : Type] \\ {}^{\mathllap{d_0}}\downarrow \uparrow^{\mathrlap{s_0}} \downarrow^{\mathrlap{d_1}} \\ Type } \,,$$

   where “$Type$” denotes the small universe / small object classifier.

   Then the Segal-completeness condition of this internal category object is the univalence condition on $\widetilde Type \to Type$.