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 8th 2012
   • (edited May 9th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexat _[[locally cartesian closed category]]_ I have added a Properties-section _[Equivalent characterizations](http://ncatlab.org/nlab/show/locally+cartesian+closed+category#EquivalentCharacterizations)_ with details on how the slice-wise internal hom and the dependent product determine each other. This is intentionally written in, supposedly pedagogical, great detail, since I need it for certain discussion purposes. But looking back at it now, if you say it is _too_ much notational detail, I will understand that :-). But I think it's still readable.

   at locally cartesian closed category I have added a Properties-section Equivalent characterizations with details on how the slice-wise internal hom and the dependent product determine each other.

   This is intentionally written in, supposedly pedagogical, great detail, since I need it for certain discussion purposes. But looking back at it now, if you say it is too much notational detail, I will understand that :-). But I think it’s still readable.

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeMay 9th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI think this is great to have; thanks!

   I think this is great to have; thanks!

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeMay 19th 2012
   • (edited May 20th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexIn the section _[equivalent formulations](http://ncatlab.org/nlab/show/locally%20cartesian%20closed%20category#EquivalentCharacterizations)_ at _[[locally cartesian closed category]]_ I would like to accompany the statement that "the internal hom in the slice is given by pullback followed by dependent product" by the corresponding type theoretic formulation. I think I know essentially what I have to do, but somehow I am missing something about how to make this fully formal So I am starting with two display maps $$ \array{ X &&&& A \\ & {}_{\mathllap{\phi}}\searrow && \swarrow_{\mathrlap{c}} \\ && B } $$ and want to write down the formula for the internal hom in the slice $$ [X,A]_B = \prod_\phi \phi^* \langle A \to B\rangle $$ type theoretically. So let's see. I start with the dependent type $\langle A \to B \rangle$ $$ b : B \vdash A(b) : Type $$ Then the pullback $\phi^* \langle A \to B\rangle$ is expressed by substitution $$ x : X \vdash A(\phi(x)) : Type $$ and next the dependent product $\prod_\phi \phi^* \langle A \to B\rangle$ is $$ b : B \vdash \prod_{x \in \phi^{-1}(b)} A(\phi(x)) : Type \,. $$ Now I am not sure how to formally proceed. I want to claim that this is definitionally equal to $$ b : B \vdash \prod_{x \in X(b)} A(b) : Type \,. $$ If so, then I am done and get the expected expression: $$ b : B \vdash X(b) \to A(b) : Type \,. $$ That step where "I want to claim" clearly makes sense. But what is the formal justification? Which rule do I need to invoke here?

   In the section equivalent formulations at locally cartesian closed category I would like to accompany the statement that “the internal hom in the slice is given by pullback followed by dependent product” by the corresponding type theoretic formulation.

   I think I know essentially what I have to do, but somehow I am missing something about how to make this fully formal

   So I am starting with two display maps

   $$\array{ X &&&& A \\ & {}_{\mathllap{\phi}}\searrow && \swarrow_{\mathrlap{c}} \\ && B }$$

   and want to write down the formula for the internal hom in the slice

   $$[X,A]_B = \prod_\phi \phi^* \langle A \to B\rangle$$

   type theoretically. So let’s see. I start with the dependent type $\langle A \to B \rangle$

   $$b : B \vdash A(b) : Type$$

   Then the pullback $\phi^* \langle A \to B\rangle$ is expressed by substitution

   $$x : X \vdash A(\phi(x)) : Type$$

   and next the dependent product $\prod_\phi \phi^* \langle A \to B\rangle$ is

   $$b : B \vdash \prod_{x \in \phi^{-1}(b)} A(\phi(x)) : Type \,.$$

   Now I am not sure how to formally proceed. I want to claim that this is definitionally equal to

   $$b : B \vdash \prod_{x \in X(b)} A(b) : Type \,.$$

   If so, then I am done and get the expected expression:

   $$b : B \vdash X(b) \to A(b) : Type \,.$$

   That step where “I want to claim” clearly makes sense. But what is the formal justification? Which rule do I need to invoke here?

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeMay 20th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThe key is that the display map $\phi : X\to B$ has two different incarnations, once as a term $$ x:X \vdash \phi(x) : B$$ and once as a dependent type $$ b:B \vdash X(b) : Type$$ The connection between them is that the type "$X$" in the first incarnation is the dependent sum $\sum_{b:B} X(b)$ in the second incarnation, and the term $\phi(x)$ is $pr1(x)$. Now the type theory actually only allows us to apply $\prod$ along display maps, in which case what we may want to think of as $\prod_{x:\phi^{-1}(b)}$ is actually $\prod_{x: X(b)}$; the notation $\phi^{-1}(b)$ has no meaning in the type theory. (For a general morphism, we could define it to be the *homotopy* fiber, but that's not I think what we're doing here.) When you make this substitution, then your expressions do match up, since for $x:X(b)$ the corresponding inhabitant of $\sum_{b:B} X(b)$ is the pair $(b,x)$, and $\phi = pr1$ applied to this does yield $b$ definitionally.

   The key is that the display map $\phi : X\to B$ has two different incarnations, once as a term

   $$x:X \vdash \phi(x) : B$$

   and once as a dependent type

   $$b:B \vdash X(b) : Type$$

   The connection between them is that the type “$X$” in the first incarnation is the dependent sum $\sum_{b:B} X(b)$ in the second incarnation, and the term $\phi(x)$ is $pr1(x)$. Now the type theory actually only allows us to apply $\prod$ along display maps, in which case what we may want to think of as $\prod_{x:\phi^{-1}(b)}$ is actually $\prod_{x: X(b)}$; the notation $\phi^{-1}(b)$ has no meaning in the type theory. (For a general morphism, we could define it to be the homotopy fiber, but that’s not I think what we’re doing here.) When you make this substitution, then your expressions do match up, since for $x:X(b)$ the corresponding inhabitant of $\sum_{b:B} X(b)$ is the pair $(b,x)$, and $\phi = pr1$ applied to this does yield $b$ definitionally.

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeMay 20th 2012
   • (edited May 20th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks!! That helps. One thing I had missed was that dependent product is by definition only allowed along displays. I had invented that notation "$x : \phi^{-1}(b)$" precisely because I thought I couldn't write $x : X(b)$ in general. But now I see that by definition that's actually what I have to do. Good. I have tried to brush up the [discussion in the entry](http://ncatlab.org/nlab/show/locally+cartesian+closed+category#RelationCartesianClosureBaseChangeInTypeTheory) accordingly now. By the way, I was thinking about this because the type-theoretic formula for the slice hom gives a very beautiful way to expose [[twisted cohomology]]. In $$ b : B \vdash X(b) \to A(b) : Type \;\;\;\; = \;\;\; b : B \vdash \prod_{x : X(b)} A(\phi(x)) : Type $$ the left hand manifestly shows a bunch of classifying maps / cocycles parameterized over $B$, whereas the right hand manifestly shows that these are equivalently sections of the pullback of a twisting bundle $c : A \to B$. Of course this is already clear in the category-theoretic formula. But the type-theoretic formula makes it "even clearer", almost translates the plain English description of the situation verbatim into a theorem. Not a particularly deep theorem, of course, I am just enjoying to see type theory formulations give nicely clear expressins for situations that have been important outside of logic.

   Thanks!! That helps.

   One thing I had missed was that dependent product is by definition only allowed along displays. I had invented that notation “$x : \phi^{-1}(b)$” precisely because I thought I couldn’t write $x : X(b)$ in general. But now I see that by definition that’s actually what I have to do. Good.

   I have tried to brush up the discussion in the entry accordingly now.

   By the way, I was thinking about this because the type-theoretic formula for the slice hom gives a very beautiful way to expose twisted cohomology. In

   $$b : B \vdash X(b) \to A(b) : Type \;\;\;\; = \;\;\; b : B \vdash \prod_{x : X(b)} A(\phi(x)) : Type$$

   the left hand manifestly shows a bunch of classifying maps / cocycles parameterized over $B$, whereas the right hand manifestly shows that these are equivalently sections of the pullback of a twisting bundle $c : A \to B$.

   Of course this is already clear in the category-theoretic formula. But the type-theoretic formula makes it “even clearer”, almost translates the plain English description of the situation verbatim into a theorem. Not a particularly deep theorem, of course, I am just enjoying to see type theory formulations give nicely clear expressins for situations that have been important outside of logic.

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeMay 21st 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThat's nice!

   That’s nice!