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.
   • CommentAuthorDean
   • CommentTimeAug 27th 2020
   • PermaLink
   Author: Dean
   Format: TextHas anyone thought about what geometric type theory would entail? I thought there might be something like this: we start with a dependent type theory. an infinitesimal extension object T(A) assigned to each A where A -> T(A) lifts against the smooth maps X -> Y, which play the role of fibrations. The infinitesimal interval plays the role of the path. An example would be sheaves over the big zariski site.

   Has anyone thought about what geometric type theory would entail?
   
   I thought there might be something like this: we start with a dependent type theory. an infinitesimal extension object T(A) assigned to each A where A -> T(A) lifts against the smooth maps X -> Y, which play the role of fibrations. The infinitesimal interval plays the role of the path.
   
   An example would be sheaves over the big zariski site.
2. • CommentRowNumber2.
   • CommentAuthorDavid_Corfield
   • CommentTimeAug 27th 2020
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexSomething along the lines of differential cohesion, see [[infinitesimal shape modality]] and further links such as Wellen's thesis there?

   Something along the lines of differential cohesion, see infinitesimal shape modality and further links such as Wellen’s thesis there?

3. • CommentRowNumber3.
   • CommentAuthorDean
   • CommentTimeAug 27th 2020
   • PermaLink
   Author: Dean
   Format: TextOh, yes, I’ll read this.

   Oh, yes, I’ll read this.
4. • CommentRowNumber4.
   • CommentAuthorDean
   • CommentTimeAug 30th 2020
   • (edited Aug 30th 2020)
   • PermaLink
   Author: Dean
   Format: MarkdownItexIn the article, he defines an infinitesimal identity type $x \sim y$ as $\iota_A(x) == \iota_A(y)$. A tweaking I like more is this. It constructs the infinitesimal path space when $F$ is etalification. Let $F$ be an idempotent monad (like etalification). We can construct the $F$-identity type $X^{I}_F$ of $X$ in the same way as with identity type, except replacing $X \times X$ with $X \times_{FX} X$. Here the pullback $X \times_{FX} X$ is over the unit of the idempotent monad $F$. We get a fibration $X^I_F \rightarrow X \times_{F X} X$ and a map $X \rightarrow X^I_F$ such that, for each fibraiton $Y \rightarrow X^I_F$ and each map $X \rightarrow Y$ making the evident diagram commute, there is a section $X^I_F \rightarrow Y$. This could then be called the $F$-path lifting property. In this way, each cohesion setup should give rise to a corresponding identity type. In particular, differential cohesion gives rise to an infinitesimal identity/path type.

   In the article, he defines an infinitesimal identity type $x \sim y$ as $\iota_A(x) == \iota_A(y)$.

   A tweaking I like more is this. It constructs the infinitesimal path space when $F$ is etalification.

   Let $F$ be an idempotent monad (like etalification). We can construct the $F$-identity type $X^{I}_F$ of $X$ in the same way as with identity type, except replacing $X \times X$ with $X \times_{FX} X$. Here the pullback $X \times_{FX} X$ is over the unit of the idempotent monad $F$. We get a fibration $X^I_F \rightarrow X \times_{F X} X$ and a map $X \rightarrow X^I_F$ such that, for each fibraiton $Y \rightarrow X^I_F$ and each map $X \rightarrow Y$ making the evident diagram commute, there is a section $X^I_F \rightarrow Y$. This could then be called the $F$-path lifting property.

   In this way, each cohesion setup should give rise to a corresponding identity type. In particular, differential cohesion gives rise to an infinitesimal identity/path type.

5. • CommentRowNumber5.
   • CommentAuthorDavid_Corfield
   • CommentTimeAug 30th 2020
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexSounds like you're getting close to Urs's [[jet comonad]] idea. See also his paper with Khavkine there.

   Sounds like you’re getting close to Urs’s jet comonad idea. See also his paper with Khavkine there.

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeAug 30th 2020
   • PermaLink
   Author: Urs
   Format: MarkdownItexYes, the $X \times_{F X} X $ in [#4](https://nforum.ncatlab.org/discussion/11662/type-theoretic-geometry/?Focus=86535#Comment_86535) is the "formal disk bundle" in Def. 3.8 [here](https://arxiv.org/pdf/1701.06238.pdf#page=22).

   Yes, the $X \times_{F X} X$ in #4 is the “formal disk bundle” in Def. 3.8 here.

7. • CommentRowNumber7.
   • CommentAuthorDean
   • CommentTimeAug 30th 2020
   • PermaLink
   Author: Dean
   Format: MarkdownItexThanks for the references, Urs. I really admire the view of geometry you’ve built here. Here’s a bit of a basic question- does flat modality turn objects into formally smooth objects?

   Thanks for the references, Urs. I really admire the view of geometry you’ve built here.

   Here’s a bit of a basic question- does flat modality turn objects into formally smooth objects?

8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeAug 30th 2020
   • PermaLink
   Author: Urs
   Format: MarkdownItexYes, we have $\Im \circ \flat \simeq \flat$ (since flat types are discrete and discrete types are infinitesimally discrete -- you can see this transparently from the system of adjoints as in (153) of [2008.01101](https://arxiv.org/abs/2008.01101)). So for a $\flat$-modal $X$ we have that $X\to \Im X$ is an equivalence, hence is, in particular, $n$-epi for all $n$.

   Yes, we have $\Im \circ \flat \simeq \flat$ (since flat types are discrete and discrete types are infinitesimally discrete – you can see this transparently from the system of adjoints as in (153) of 2008.01101).

   So for a $\flat$-modal $X$ we have that $X\to \Im X$ is an equivalence, hence is, in particular, $n$-epi for all $n$.

9. • CommentRowNumber9.
   • CommentAuthorDean
   • CommentTimeSep 3rd 2020
   • (edited Sep 3rd 2020)
   • PermaLink
   Author: Dean
   Format: MarkdownItexUrs has (patiently) explained to me how $[D, X]$ does not have two projection maps into $X$, like the path space object $[I, X]$ does. His fix - the natural one - is to consider $[D, X] \times D$ instead. One projection is the counit of the hom-product adjunction, and the other is the composition $[D, X] \times D \rightarrow [D, X] \rightarrow [*, X]$, where the first is the projection map and the other is $[-, X]$ applied to the (single) inclusion $* \rightarrow D$. We then realize that this choice is redundant, in that, intuitively, $(fa, x) \sim (f, ax)$ for any element of the ring object $R$ (suppose we are in the setup of synthetic geometry). The multiplication from $R$ on $D$ and $[D, X]$ is provided in that setup. So we take the coequilizer of the two maps $[D, X] \times R \times D \rightarrow [D, X] \times D$, the maps being $\mu \times 1$ and $1 \times \mu$. We then call this $[D, X] \otimes D$, an object which genuinely has two maps into $X$. I am still gunning for a definition of infinitesimal path space object in the type theoretic setting; Wellen's thesis hints at this with $x \sim y : \equiv \iota_A (x) = \iota_A (y)$, but as mentioned there this is not a proposition. My question is whether Urs's definition in the synthetic approach coincides with the definition in #4 in the type theoretic approach. Does anyone know if $X^I_F$ in #4 (modified to be type theoretical) above the same as $[D, X] \otimes D$ in the context of synthetic differential geometry?

   Urs has (patiently) explained to me how $[D, X]$ does not have two projection maps into $X$, like the path space object $[I, X]$ does. His fix - the natural one - is to consider $[D, X] \times D$ instead. One projection is the counit of the hom-product adjunction, and the other is the composition $[D, X] \times D \rightarrow [D, X] \rightarrow [*, X]$, where the first is the projection map and the other is $[-, X]$ applied to the (single) inclusion $* \rightarrow D$. We then realize that this choice is redundant, in that, intuitively, $(fa, x) \sim (f, ax)$ for any element of the ring object $R$ (suppose we are in the setup of synthetic geometry). The multiplication from $R$ on $D$ and $[D, X]$ is provided in that setup. So we take the coequilizer of the two maps $[D, X] \times R \times D \rightarrow [D, X] \times D$, the maps being $\mu \times 1$ and $1 \times \mu$. We then call this $[D, X] \otimes D$, an object which genuinely has two maps into $X$.

   I am still gunning for a definition of infinitesimal path space object in the type theoretic setting; Wellen’s thesis hints at this with $x \sim y : \equiv \iota_A (x) = \iota_A (y)$, but as mentioned there this is not a proposition.

   My question is whether Urs’s definition in the synthetic approach coincides with the definition in #4 in the type theoretic approach. Does anyone know if $X^I_F$ in #4 (modified to be type theoretical) above the same as $[D, X] \otimes D$ in the context of synthetic differential geometry?

10. • CommentRowNumber10.
    • CommentAuthorDean
    • CommentTimeSep 3rd 2020
    • (edited Sep 4th 2020)
    • PermaLink
    Author: Dean
    Format: MarkdownItexActually, I notice that Urs’s construction does paths starting at the origin of the tangent space, and after some more reading, that we use two of these constructions $[D, X ] \otimes D$ to get two endpoints of an interval? Is this correct? And any two points in the tangent space are connectible by a ‘path‘? I am beginning to think that, with T the coreduction for the square-zero killing function in #4, we get the same construction Kock and Urs give up to equivalence. Please excuse me if any of this is naive.

    Actually, I notice that Urs’s construction does paths starting at the origin of the tangent space, and after some more reading, that we use two of these constructions $[D, X ] \otimes D$ to get two endpoints of an interval? Is this correct? And any two points in the tangent space are connectible by a ‘path‘? I am beginning to think that, with T the coreduction for the square-zero killing function in #4, we get the same construction Kock and Urs give up to equivalence.

    Please excuse me if any of this is naive.

11. • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeSep 4th 2020
    • (edited Sep 4th 2020)
    • PermaLink
    Author: Urs
    Format: MarkdownItexIs your question whether the [[infinitesimal singular simplicial complex]] construction models the [[infinitesimal shape modality]] (both for given order of infinitesimality? It ought to, but I don't have proof. I know I once tried to prove this and then abandoned the question, but now I forget what I concluded, if anything. Notice that this is the direct analogue of the question whether the smooth singular simplicial complex construction models the [[shape modality]]. This was eventually proven to be the case by Dmitri Pavlov, pointers are at _[[shape via cohesive path ∞-groupoid]]_. This statement is most useful in practice. If you can prove the infinitesimal analogue, it should also be very useful. But it must be essentially the statement of crystalline cohomology, as in Lurie's note on crystals ([pdf](https://ncatlab.org/nlab/files/LurieCrystals.pdf)). Up to notation, you see that there he first considers the infinitesimal singular simplicial complex, and then the infinitesimal shape modality, in the algebraic category.

    Is your question whether the infinitesimal singular simplicial complex construction models the infinitesimal shape modality (both for given order of infinitesimality?

    It ought to, but I don’t have proof. I know I once tried to prove this and then abandoned the question, but now I forget what I concluded, if anything.

    Notice that this is the direct analogue of the question whether the smooth singular simplicial complex construction models the shape modality. This was eventually proven to be the case by Dmitri Pavlov, pointers are at shape via cohesive path ∞-groupoid. This statement is most useful in practice.

    If you can prove the infinitesimal analogue, it should also be very useful. But it must be essentially the statement of crystalline cohomology, as in Lurie’s note on crystals (pdf). Up to notation, you see that there he first considers the infinitesimal singular simplicial complex, and then the infinitesimal shape modality, in the algebraic category.

12. • CommentRowNumber12.
    • CommentAuthorDean
    • CommentTimeSep 4th 2020
    • (edited Sep 4th 2020)
    • PermaLink
    Author: Dean
    Format: MarkdownItexThis sounds like a project that I’d like to take on. But I don’t entirely understand what you mean by models. Can you explain a bit more? Oh, and my question is related, but I was looking for a definition of infinitesimal path space type in type theory that matched the infinitesimal path object in synthetic differential geometry. I suspect that the definition is the universal triangle $X \rightarrow Path(X) \rightarrow X \times_{T(X)} X$ with the second map being a fibration. That can be expressed by a lifting property, the same as the one for identity type. Or maybe path(X) is the same as the pullback since all infinitesimal paths starting at the origin are connected? I thought this manifests as your construction $[D, X] \otimes D$ in synthetic differential geometry.

    This sounds like a project that I’d like to take on. But I don’t entirely understand what you mean by models. Can you explain a bit more?

    Oh, and my question is related, but I was looking for a definition of infinitesimal path space type in type theory that matched the infinitesimal path object in synthetic differential geometry.

    I suspect that the definition is the universal triangle $X \rightarrow Path(X) \rightarrow X \times_{T(X)} X$ with the second map being a fibration. That can be expressed by a lifting property, the same as the one for identity type. Or maybe path(X) is the same as the pullback since all infinitesimal paths starting at the origin are connected?

    I thought this manifests as your construction $[D, X] \otimes D$ in synthetic differential geometry.

13. • CommentRowNumber13.
    • CommentAuthorDean
    • CommentTimeSep 4th 2020
    • (edited Sep 4th 2020)
    • PermaLink
    Author: Dean
    Format: MarkdownItexThat construction shows how a modality induces a path space type. Conversely, a path space type induces a connected components modality with possible adjoint modalities; it is the coequilizer of the two maps $X^I \rightarrow X$.

    That construction shows how a modality induces a path space type. Conversely, a path space type induces a connected components modality with possible adjoint modalities; it is the coequilizer of the two maps $X^I \rightarrow X$.

14. • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeSep 4th 2020
    • PermaLink
    Author: Urs
    Format: MarkdownItexAh, I said "model" just because I am thinking of the infinitesimal shape modality $\Im$ as being "abtractly defined" (i.e. by a universal property, either it being adjoint to something else, or it being a localization at/nullification of some objects) while the infinitesimal singular simplicial complex is "concretely defined" by an explicit construction. So if we prove both functors to be equivalent, then, to my mind, that then makes the latter be a "model" or "realization" of the former. That's all I meant. Concerning your other questions, I am not sure what I can say. It sounds like you are wondering about technical fine-print in coding the infinitesimal singular simplicial complex. I admit that I feel too busy with other things to dive into that detail now. But if you are indeed going to look into the proof, do have a close look at Lurie's _Notes on Crystals_ [here](https://ncatlab.org/nlab/show/crystalline+cohomology#LurieCrystals) (it's just a few pages) for, I think, some version of this proof, to some degree, is actually in there.

    Ah, I said “model” just because I am thinking of the infinitesimal shape modality $\Im$ as being “abtractly defined” (i.e. by a universal property, either it being adjoint to something else, or it being a localization at/nullification of some objects) while the infinitesimal singular simplicial complex is “concretely defined” by an explicit construction.

    So if we prove both functors to be equivalent, then, to my mind, that then makes the latter be a “model” or “realization” of the former. That’s all I meant.

    Concerning your other questions, I am not sure what I can say. It sounds like you are wondering about technical fine-print in coding the infinitesimal singular simplicial complex. I admit that I feel too busy with other things to dive into that detail now.

    But if you are indeed going to look into the proof, do have a close look at Lurie’s Notes on Crystals here (it’s just a few pages) for, I think, some version of this proof, to some degree, is actually in there.

15. • CommentRowNumber15.
    • CommentAuthorDean
    • CommentTimeSep 4th 2020
    • PermaLink
    Author: Dean
    Format: MarkdownItexOk- thanks very much for all your help. One more thing: won’t I have to tweak the infinitesimal singular complexes from using first order infinitesimals to using jets for this to work?

    Ok- thanks very much for all your help. One more thing: won’t I have to tweak the infinitesimal singular complexes from using first order infinitesimals to using jets for this to work?

16. • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeSep 4th 2020
    • (edited Sep 4th 2020)
    • PermaLink
    Author: Urs
    Format: MarkdownItexBoth sides of the construction are parametrized by a choice of order of infintiesimality in $\mathbb{N} \sqcup \{\infty\}$. (The infinitesimal shape modality can be defined with nullification of order-$n$ infinitesimal disks, too.) I expect that for all $n \in \mathbb{N} \sqcup \{\infty\}$ one version of the theorem applies.

    Both sides of the construction are parametrized by a choice of order of infintiesimality in $\mathbb{N} \sqcup \{\infty\}$. (The infinitesimal shape modality can be defined with nullification of order-$n$ infinitesimal disks, too.)

    I expect that for all $n \in \mathbb{N} \sqcup \{\infty\}$ one version of the theorem applies.