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
   • CommentTimeDec 9th 2011
   • PermaLink
   Author: Urs
   Format: MarkdownItexI am working on an entry [[cohesive homotopy type theory]]. This started out as material split off from [[cohesive (infinity,1)-topos]], but is expanding now.

   I am working on an entry cohesive homotopy type theory.

   This started out as material split off from cohesive (infinity,1)-topos, but is expanding now.

2. • CommentRowNumber2.
   • CommentAuthorTobyBartels
   • CommentTimeDec 12th 2011
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexSomehow from here I got to the adjective entry [[cohesive]].

   Somehow from here I got to the adjective entry cohesive.

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeDec 12th 2011
   • PermaLink
   Author: Urs
   Format: MarkdownItexHm, thanks. I had entirely forgotten about that entry. But it is useful to have! :-)

   Hm, thanks. I had entirely forgotten about that entry. But it is useful to have! :-)

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeSep 2nd 2012
   • (edited Sep 2nd 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexTodd Trimble had kindly sent me a bunch of useful comments, by email, on the entry _[[cohesive homotopy type theory]]_. I have meanwhile replied by email, but I hope we will eventually move that discussion to here. Before we do so, maybe I should emphasize two points, so that you won't be wondering: 1. The entry is labeled "under construction" for good reason. It's a quick hack that I once wrote, somewhat hastily, for the sole purpose of having a way to point from various online discussions to a place where some ideas and in particular where the references listed there are collected. A more recent writeup of the same kind of ideas which is much better as far as readability and completeness go is what I wrote with Mike Shulman at [[schreiber:Quantum gauge field theory in Cohesive homotopy type theory]]. That is still a rather brief account (necessarily so, because we wrote it subject to tight size restrictions) but probably anyone who feels like working on improving the nLab entry should look at that first. 1. While I am excited about having Todd join forces on working out and writing out these matters, unfortunately right these days I won't be able to offer any substantial editing myself. For the next two months I'll be teaching a master course twice a week, will need to follow some invitations to some conferences, and will be advising a master student, all of which requires its preparation time. I will already be struggling with coping with these mandatory tasks. But after two months from right now, I should again be able to, and indeed be more than happy to, join forces on cohesive homotopy type theory again!

   Todd Trimble had kindly sent me a bunch of useful comments, by email, on the entry cohesive homotopy type theory. I have meanwhile replied by email, but I hope we will eventually move that discussion to here.

   Before we do so, maybe I should emphasize two points, so that you won’t be wondering:

   1. The entry is labeled “under construction” for good reason. It’s a quick hack that I once wrote, somewhat hastily, for the sole purpose of having a way to point from various online discussions to a place where some ideas and in particular where the references listed there are collected.

      A more recent writeup of the same kind of ideas which is much better as far as readability and completeness go is what I wrote with Mike Shulman at Quantum gauge field theory in Cohesive homotopy type theory (schreiber). That is still a rather brief account (necessarily so, because we wrote it subject to tight size restrictions) but probably anyone who feels like working on improving the nLab entry should look at that first.

   2. While I am excited about having Todd join forces on working out and writing out these matters, unfortunately right these days I won’t be able to offer any substantial editing myself. For the next two months I’ll be teaching a master course twice a week, will need to follow some invitations to some conferences, and will be advising a master student, all of which requires its preparation time. I will already be struggling with coping with these mandatory tasks. But after two months from right now, I should again be able to, and indeed be more than happy to, join forces on cohesive homotopy type theory again!

5. • CommentRowNumber5.
   • CommentAuthorTodd_Trimble
   • CommentTimeSep 2nd 2012
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexThanks, Urs. For anyone reading, I wrote Urs privately after reading the [interview](http://www.thereasoner.org/) between him and David Corfield. A terrific interview, by the way, since it gave Urs an opportunity to give rather more personal feelings about his research, and I could just hear the excitement in his voice, and that excitement began to rub off. It got me wanting to look a little more closely into what he and Mike have been up to, and since the interview pointed me to [[cohesive homotopy type theory]], I started there, and immediately had questions which I fired off to Urs, who answered very nicely. Some of his answers should appear shortly. He recommended to me particularly section 2 of his paper with Mike as something that might be helpful to me. I view my own role in this as something of "guinea pig" -- if I can understand this material, then so can a lot of people. Any active input from me would mostly come from selfish interest in trying to make things clear to myself, and leaving a record of any success I have. Anyone who would like to help (e.g., help me understand, help improve articles, etc.) is of course very welcome, although of course I understand that people are busy.

   Thanks, Urs. For anyone reading, I wrote Urs privately after reading the interview between him and David Corfield. A terrific interview, by the way, since it gave Urs an opportunity to give rather more personal feelings about his research, and I could just hear the excitement in his voice, and that excitement began to rub off. It got me wanting to look a little more closely into what he and Mike have been up to, and since the interview pointed me to cohesive homotopy type theory, I started there, and immediately had questions which I fired off to Urs, who answered very nicely. Some of his answers should appear shortly. He recommended to me particularly section 2 of his paper with Mike as something that might be helpful to me.

   I view my own role in this as something of “guinea pig” – if I can understand this material, then so can a lot of people. Any active input from me would mostly come from selfish interest in trying to make things clear to myself, and leaving a record of any success I have. Anyone who would like to help (e.g., help me understand, help improve articles, etc.) is of course very welcome, although of course I understand that people are busy.

6. • CommentRowNumber6.
   • CommentAuthorEric
   • CommentTimeSep 3rd 2012
   • PermaLink
   Author: Eric
   Format: MarkdownItexI read the interview and was also inspired to read some nLab pages and it became clear I'm not qualified to understand it. I still haven't mastered adjoint functors (!). Does that completely disqualify me from ever being able to understand cohesion? Could it be described for finite sets using even lower tech?

   I read the interview and was also inspired to read some nLab pages and it became clear I’m not qualified to understand it. I still haven’t mastered adjoint functors (!).

   Does that completely disqualify me from ever being able to understand cohesion? Could it be described for finite sets using even lower tech?

7. • CommentRowNumber7.
   • CommentAuthorDavid_Corfield
   • CommentTimeSep 3rd 2012
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexIt would fun to run an online seminar when people have time, with different levels of expertise. Eric, working through a 4-term chain of adjoints provides a good way to understand adjoint functors. If $U: Top \to Set$ is the forgetful functor from locally connected topological spaces to sets, there is a chain $$ (\pi_0, Dis, U, CoDis), $$ where $\pi_0$ sends a space to its set of components, $Dis$ sends a set to the space with those points and the discrete topology, and likewise $CoDis$ for the codiscrete topology. So starting along the chain, there is an equivalence between >set functions from (set of components of space $X$) to (set $A$) and >continuous functions from (space $X$) to (space $Dis A$). Putting it crudely, because $Dis A$ is so broken up, it's hard to find continuous maps to it. In fact you have to use maps which are locally constant, all points in the same component of $X$ are sent to a single element of $A$.

   It would fun to run an online seminar when people have time, with different levels of expertise.

   Eric, working through a 4-term chain of adjoints provides a good way to understand adjoint functors. If $U: Top \to Set$ is the forgetful functor from locally connected topological spaces to sets, there is a chain

   $$(\pi_0, Dis, U, CoDis),$$

   where $\pi_0$ sends a space to its set of components, $Dis$ sends a set to the space with those points and the discrete topology, and likewise $CoDis$ for the codiscrete topology.

   So starting along the chain, there is an equivalence between

   set functions from (set of components of space $X$) to (set $A$)

   and

   continuous functions from (space $X$) to (space $Dis A$).

   Putting it crudely, because $Dis A$ is so broken up, it’s hard to find continuous maps to it. In fact you have to use maps which are locally constant, all points in the same component of $X$ are sent to a single element of $A$.

8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeSep 3rd 2012
   • (edited Sep 3rd 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItex[ after posting I see that the following reply overlaps with David's reply above ] One does need to be familiar with adjoint functors and related concepts in order to get an accurate idea of the notion of cohesion, yes. But of course intuitive approximations to basic ideas can be given in words. That will give an idea of the motivations and make plausible the nature of the applications, at least. There is a bit of such a intuitive discussion in the [Idea-section](http://ncatlab.org/nlab/show/cohesive%20topos#Idea) at _[[cohesive topos]]_. But maybe we should break that further down to make it useful for laymen. I can add more to that Idea-section. Let me know if the following kind of text is helpful: *** A notion of _cohesion_ on a collection $\mathbf{H}$ of spaces is supposed to be a means to specify how points in any space $X \in \mathbf{H}$ "hang together" or "cohere", analogous to how water molecuses in a droplet of whater are held together by cohesion. A basic example arises for [[topological spaces]] or [[manifolds]]: here the "droplet of water" is an [[open ball]] of points. Indeed, one of the central examples of cohesive spaces is that of [[smooth spaces]] and these are spaces that can be _probed_ by smooth open balls, such that these smooth open balls are the elementary "cohesive droplets" out of which any smooth space is built. That intuition should be evident enough. The question is which formal axioms capture this droplet-intuition accurately and efficiently. The crucial insight of [[Bill Lawvere]] is that a rather minmalistic set of axioms already does the job: 1. there has to be an assignment $\Pi : \mathbf{H} \to Set$ that sends every cohesive space $X$ to its _set of cohesively connected components_. For instance a single open ball as above, an elementary droplet, is sent to the set $\{*\}$ with a single element. 1. We should be entitled to regard every set $S \in Set$ trivially as a cohesive space in two ways: * either we regard every element in $S$ as an atomic cohesive droplet itself, cohesively disconnected to any other point. Call the resulting cohesive space $Disc(X)$. For smooth cohection $Disc(X)$ is simply the [[discrete space|discrete manifold]] being the disjoint union of one point per element in $S$. * or, at the opposite extreme, we regard all the elements in $S$ as being cohesively connected, hence regard all of $S$ itself as one single big cohesive droplet. We write $coDisc(X)$ for $S$ regarded as a cohesive space this way, because in the context of topological cohesion this is the [[codiscrete space]] on the given set. 1. The collection of discrete and codiscrete cohesive spaces should sit nicely inside the collection of all cohesive spaces, essentially in just the obvious way that one intuitivey expects. For instance cohesive maps between two discretely cohesive spaces should be simply maps between the underlying sets, and so on. And the notion of "discrete" exhibited by the collection of discrete objects has indeed to be compatible with the notion of "cohesive" as seen by that map $\Pi$ above. This is just the evident consistency condition which you are probably assuming anyway: for instance if $Disc(S)$ is a set regarded as a discrete cohesive space, then $\Pi(Disc(S))$, which is supposed to be its set of cohesively connected points, should be just $S$ itself, since no point in $Disc(S)$ is supposed to be cohesively connected to any other. In particular $\Pi(Disc(*))$ should be the point again. That's essentially it, already. It sounds very simple (hopefully) and indeed it is very simple. Once you know the notion of an adjoint functor it is pretty straightforward to formalize the above text in terms of that notion. The interesting observation is that simple as this idea is, it has very powerful consequences ... once it is formalized not just with adjoint functors but with [[adjoint (infinity,1)-functors]].

   [ after posting I see that the following reply overlaps with David’s reply above ]

   One does need to be familiar with adjoint functors and related concepts in order to get an accurate idea of the notion of cohesion, yes.

   But of course intuitive approximations to basic ideas can be given in words. That will give an idea of the motivations and make plausible the nature of the applications, at least.

   There is a bit of such a intuitive discussion in the Idea-section at cohesive topos. But maybe we should break that further down to make it useful for laymen.

   I can add more to that Idea-section. Let me know if the following kind of text is helpful:

   ---

   A notion of cohesion on a collection $\mathbf{H}$ of spaces is supposed to be a means to specify how points in any space $X \in \mathbf{H}$ “hang together” or “cohere”, analogous to how water molecuses in a droplet of whater are held together by cohesion. A basic example arises for topological spaces or manifolds: here the “droplet of water” is an open ball of points. Indeed, one of the central examples of cohesive spaces is that of smooth spaces and these are spaces that can be probed by smooth open balls, such that these smooth open balls are the elementary “cohesive droplets” out of which any smooth space is built.

   That intuition should be evident enough. The question is which formal axioms capture this droplet-intuition accurately and efficiently. The crucial insight of Bill Lawvere is that a rather minmalistic set of axioms already does the job:

   1. there has to be an assignment $\Pi : \mathbf{H} \to Set$ that sends every cohesive space $X$ to its set of cohesively connected components. For instance a single open ball as above, an elementary droplet, is sent to the set $\{*\}$ with a single element.

   2. We should be entitled to regard every set $S \in Set$ trivially as a cohesive space in two ways:

      • either we regard every element in $S$ as an atomic cohesive droplet itself, cohesively disconnected to any other point. Call the resulting cohesive space $Disc(X)$. For smooth cohection $Disc(X)$ is simply the discrete manifold being the disjoint union of one point per element in $S$.

      • or, at the opposite extreme, we regard all the elements in $S$ as being cohesively connected, hence regard all of $S$ itself as one single big cohesive droplet. We write $coDisc(X)$ for $S$ regarded as a cohesive space this way, because in the context of topological cohesion this is the codiscrete space on the given set.

   3. The collection of discrete and codiscrete cohesive spaces should sit nicely inside the collection of all cohesive spaces, essentially in just the obvious way that one intuitivey expects. For instance cohesive maps between two discretely cohesive spaces should be simply maps between the underlying sets, and so on.

      And the notion of “discrete” exhibited by the collection of discrete objects has indeed to be compatible with the notion of “cohesive” as seen by that map $\Pi$ above. This is just the evident consistency condition which you are probably assuming anyway: for instance if $Disc(S)$ is a set regarded as a discrete cohesive space, then $\Pi(Disc(S))$, which is supposed to be its set of cohesively connected points, should be just $S$ itself, since no point in $Disc(S)$ is supposed to be cohesively connected to any other.

      In particular $\Pi(Disc(*))$ should be the point again.

   That’s essentially it, already. It sounds very simple (hopefully) and indeed it is very simple. Once you know the notion of an adjoint functor it is pretty straightforward to formalize the above text in terms of that notion.

   The interesting observation is that simple as this idea is, it has very powerful consequences … once it is formalized not just with adjoint functors but with adjoint (infinity,1)-functors.

9. • CommentRowNumber9.
   • CommentAuthorDavid_Corfield
   • CommentTimeSep 3rd 2012
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexCould this be material for one of your 'motivation' pages? I think they're a great idea, especially the [motivation for sheaves...](http://ncatlab.org/nlab/show/motivation+for+sheaves,+cohomology+and+higher+stacks).

   Could this be material for one of your ’motivation’ pages? I think they’re a great idea, especially the motivation for sheaves….

10. • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeSep 3rd 2012
    • (edited Sep 3rd 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItexOkay, good idea. I did so and created _[[motivation for cohesive toposes]]_. Let's move any further chat about this non-technical discussion to the [corresponding thread](http://nforum.mathforge.org/discussion/4154/motivation-for-cohesive-toposes/?Focus=33830#Comment_33830).

    Okay, good idea. I did so and created motivation for cohesive toposes. Let’s move any further chat about this non-technical discussion to the corresponding thread.

11. • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeSep 6th 2012
    • (edited Sep 6th 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItexIs the following roughly right: Since cohesion is axiomatized in terms of the two monads $\sharp : \mathbf{H} \to \mathbf{H}$ and $\flat : \mathbf{H} \to \mathbf{H}$... **Question**: once written in Coq, this is the same kind of monad construction that the Haskell community is all excited about. Right? The notoriously advertized monads in Haskell are just monoids in endomorphisms on the ambient type universe, right? To Bob Harper's _[Of course ML has monads!](http://existentialtype.wordpress.com/2011/05/01/of-course-ml-has-monads/)_ we can add **Of Course Coq has $\infty$-monads!**, and it's the same sense of "programming language has monads"-statement, right? I mean, I am guessing the answer is: Yes of course. I just want a sanity check, because I have trouble reading the online texts on the Haskell monads. I am a reader in the blind spot: these texts typically spend two pages telling the reader that he will find the notion of monad hard to understand, only to then plunge into Haskell code without any explanation of what _that_ means. For me it would have to be the other way around :-) Well, I am getting there. But any helpful comment would be appreciated anyway.

    Is the following roughly right:

    Since cohesion is axiomatized in terms of the two monads $\sharp : \mathbf{H} \to \mathbf{H}$ and $\flat : \mathbf{H} \to \mathbf{H}$…

    Question: once written in Coq, this is the same kind of monad construction that the Haskell community is all excited about. Right?

    The notoriously advertized monads in Haskell are just monoids in endomorphisms on the ambient type universe, right?

    To Bob Harper’s Of course ML has monads! we can add Of Course Coq has $\infty$-monads!, and it’s the same sense of “programming language has monads”-statement, right?

    I mean, I am guessing the answer is: Yes of course. I just want a sanity check, because I have trouble reading the online texts on the Haskell monads. I am a reader in the blind spot: these texts typically spend two pages telling the reader that he will find the notion of monad hard to understand, only to then plunge into Haskell code without any explanation of what that means. For me it would have to be the other way around :-)

    Well, I am getting there. But any helpful comment would be appreciated anyway.

12. • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeSep 6th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexYes, the reflections $\sharp$ and $\Pi$ are, in particular, monads on the type universe. They're fancier than Haskell monads, of course, since the type system of Coq has dependent types — which was what caused all the issues with reflective subfibrations etc. But when you restrict them down to the non-dependent world, they look like Haskell monads (albeit of a very special kind, namely idempotent monads). There's an important contrast in that most Haskell monads are *defined* in terms of the preexisting type theory, rather than *axiomatized* as $\sharp$ is. That isn't universally true, though, for instance the Haskell monad `IO` is basically a part of the type system put in axiomatically. (I've also speculated that it might be useful for a programming-language-like type theory to have a $\sharp$-like monad playing the role of the codiscrete objects in the effective topos, as an alternative way to deal with the computability issues that people often recourse to setoids for, but I've never gotten around to figuring out to what extent that might be true.) Additionally, a big part of the power of monads in Haskell is the language support for them. Any strongly typed language "has monads" in the sense that its type system admits some functors that are monads, like Haskell's Reader and Writer and State. If it has parametric polymorphism, then you can define each of those monads as a parametrized type family. The additional thing that languages like Haskell, ML, and Coq add is an ability to abstract out the structure of a monad (the multiplication and unit maps, and in Coq's case the axioms they satisfy) and describe it as part of the type. Haskell does it with type classes, ML with modules, while Coq has both type classes and modules (producing vast amounts of confusion for someone like me trying to figure out which one to use!). Haskell also has some special syntactic sugar for monads, which (with all due respect to Bob Harper) I personally think is kind of nice. And Coq's very flexible mixfix-notation-definition facility can more or less mimic what Haskell has built in.

    Yes, the reflections $\sharp$ and $\Pi$ are, in particular, monads on the type universe. They’re fancier than Haskell monads, of course, since the type system of Coq has dependent types — which was what caused all the issues with reflective subfibrations etc. But when you restrict them down to the non-dependent world, they look like Haskell monads (albeit of a very special kind, namely idempotent monads).

    There’s an important contrast in that most Haskell monads are defined in terms of the preexisting type theory, rather than axiomatized as $\sharp$ is. That isn’t universally true, though, for instance the Haskell monad IO is basically a part of the type system put in axiomatically. (I’ve also speculated that it might be useful for a programming-language-like type theory to have a $\sharp$-like monad playing the role of the codiscrete objects in the effective topos, as an alternative way to deal with the computability issues that people often recourse to setoids for, but I’ve never gotten around to figuring out to what extent that might be true.)

    Additionally, a big part of the power of monads in Haskell is the language support for them. Any strongly typed language “has monads” in the sense that its type system admits some functors that are monads, like Haskell’s Reader and Writer and State. If it has parametric polymorphism, then you can define each of those monads as a parametrized type family. The additional thing that languages like Haskell, ML, and Coq add is an ability to abstract out the structure of a monad (the multiplication and unit maps, and in Coq’s case the axioms they satisfy) and describe it as part of the type. Haskell does it with type classes, ML with modules, while Coq has both type classes and modules (producing vast amounts of confusion for someone like me trying to figure out which one to use!). Haskell also has some special syntactic sugar for monads, which (with all due respect to Bob Harper) I personally think is kind of nice. And Coq’s very flexible mixfix-notation-definition facility can more or less mimic what Haskell has built in.

13. • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeSep 6th 2012
    • (edited Sep 6th 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks! Great. One last question for tonight (local time): > Any strongly typed language "has monads" Hm, so in Coq, the way you coded it at least, the crucial bit is the Type classifier, the internal incarnation of the type universe, which allows to explicitly give the endomorphism of the monad $$ \sharp : Type \to Type \,. $$ Not all these languages will have such a type of types, right?

    Thanks! Great.

    One last question for tonight (local time):

    Any strongly typed language “has monads”

    Hm, so in Coq, the way you coded it at least, the crucial bit is the Type classifier, the internal incarnation of the type universe, which allows to explicitly give the endomorphism of the monad

    $$\sharp : Type \to Type \,.$$

    Not all these languages will have such a type of types, right?

14. • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeSep 6th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexYes, the existence of $Type$, or more particularly its consequence that we can talk about "functions from types to types", is what I referred to above as "parametric polymorphism". Haskell doesn't have a "type classifier" like Coq does, but we can still define a "function from types to types" by defining a "type that depends on a type variable" — this is how you do a monad. What I meant by "any strongly typed language has monads" was that even without such polymorphism, there still "exist" monads on the category of types, such as those one constructs in Haskell — it's just that you won't be able to define the monad as a single entity within the language syntax.

    Yes, the existence of $Type$, or more particularly its consequence that we can talk about “functions from types to types”, is what I referred to above as “parametric polymorphism”. Haskell doesn’t have a “type classifier” like Coq does, but we can still define a “function from types to types” by defining a “type that depends on a type variable” — this is how you do a monad. What I meant by “any strongly typed language has monads” was that even without such polymorphism, there still “exist” monads on the category of types, such as those one constructs in Haskell — it’s just that you won’t be able to define the monad as a single entity within the language syntax.

15. • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeSep 6th 2012
    • (edited Sep 6th 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItex> Yes, the existence of Type, or more particularly its consequence that we can talk about "functions from types to types", is what I referred to above as "parametric polymorphism". Ah, thanks, I never knew what that term meant. So "parametric" for "may vary/depend over the base/context" and "polymorphism" since there is more than one type? Is that just what it means? Maybe we can put a note into _[[parametric polymorphism]]_.

    Yes, the existence of Type, or more particularly its consequence that we can talk about “functions from types to types”, is what I referred to above as “parametric polymorphism”.

    Ah, thanks, I never knew what that term meant. So “parametric” for “may vary/depend over the base/context” and “polymorphism” since there is more than one type? Is that just what it means?

    Maybe we can put a note into parametric polymorphism.

16. • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeSep 6th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexDone.

    Done.

17. • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeSep 6th 2012
    • PermaLink
    Author: Urs
    Format: MarkdownItexAh, I see. Thanks.

    Ah, I see. Thanks.

18. • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeJan 25th 2014
    • PermaLink
    Author: Urs
    Format: MarkdownItexI have updated the links to Mike's code at _[[cohesive homotopy type theory]]_, alerted by [this discussion](https://groups.google.com/forum/#!topic/hott-amateurs/AEIjxgFHnIc)

    I have updated the links to Mike’s code at cohesive homotopy type theory, alerted by this discussion

19. • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeOct 13th 2014
    • (edited Oct 13th 2014)
    • PermaLink
    Author: Urs
    Format: MarkdownItex[[Alexander Berenbeim]] just started a [blog on cohesive homotopy type theory](http://topostheorist.wordpress.com)

    Alexander Berenbeim just started a blog on cohesive homotopy type theory

20. • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeOct 13th 2014
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexNice! I'm currently working on a bunch of redesigns of the HoTT/Coq library, part of my goal being to make it easier to redo the theory of modalities and cohesion therein. We already have some of it, but some is left to do, e.g. the theory of lex modalities. It'll have to be mostly rewritten from scratch, but it'll be better for that, and more usable in the future given all that we've learned in the current incarnation of the library.

    Nice!

    I’m currently working on a bunch of redesigns of the HoTT/Coq library, part of my goal being to make it easier to redo the theory of modalities and cohesion therein. We already have some of it, but some is left to do, e.g. the theory of lex modalities. It’ll have to be mostly rewritten from scratch, but it’ll be better for that, and more usable in the future given all that we’ve learned in the current incarnation of the library.

21. • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeOct 14th 2014
    • PermaLink
    Author: Urs
    Format: MarkdownItexInteresting. Do you also include aspects of weak Tarskian universes in the redesign? I suppose you did see the final version of Cesare Gallozzi's thesis recently? (I am asking because I only know that you were involved to some extent, but not how much exactly.)

    Interesting.

    Do you also include aspects of weak Tarskian universes in the redesign?

    I suppose you did see the final version of Cesare Gallozzi’s thesis recently? (I am asking because I only know that you were involved to some extent, but not how much exactly.)

22. • CommentRowNumber22.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 14th 2014
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItex@Urs is this thesis generally available? Googling Gallozzi's name didn't produce much of use.

    @Urs is this thesis generally available? Googling Gallozzi’s name didn’t produce much of use.

23. • CommentRowNumber23.
    • CommentAuthorMike Shulman
    • CommentTimeOct 14th 2014
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexNo, no weakly Tarski universes. I'm still hoping that we'll find a way to model honest universes in all toposes. Plus I have faith that most anything we do with honest universes could be done more tediously with weakly Tarski ones, and the library is intended to be usable. Right now I am wondering whether anything important would be lost by restricting attention to accessible modalities (those obtained by localization at some internal family of maps). All the modalities arising in topos models of cohesion are accessible, correct? The only inaccessible modality that I can think of is "double-negation in the absence of propositional resizing", and accessible ones have a number of advantages both actual and technical. (In particular, right now I think the theorem that the type of modal types for a lex modality is itself modal only works in the accessible case; I was too sloppy with universes when I proved it before using type-in-type). And no, I never heard any more from Gallozzi since June.

    No, no weakly Tarski universes. I’m still hoping that we’ll find a way to model honest universes in all toposes. Plus I have faith that most anything we do with honest universes could be done more tediously with weakly Tarski ones, and the library is intended to be usable.

    Right now I am wondering whether anything important would be lost by restricting attention to accessible modalities (those obtained by localization at some internal family of maps). All the modalities arising in topos models of cohesion are accessible, correct? The only inaccessible modality that I can think of is “double-negation in the absence of propositional resizing”, and accessible ones have a number of advantages both actual and technical. (In particular, right now I think the theorem that the type of modal types for a lex modality is itself modal only works in the accessible case; I was too sloppy with universes when I proved it before using type-in-type).

    And no, I never heard any more from Gallozzi since June.

24. • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeOct 14th 2014
    • PermaLink
    Author: Urs
    Format: MarkdownItex> All the modalities arising in topos models of cohesion are accessible, correct? You may have to help me, do you mean that the underlying $\infty$-functors are accessible? In that case the answer is yes. But you mention localization at an internal family of maps. This I don't know about. Could you give me some pointer to more details?

    All the modalities arising in topos models of cohesion are accessible, correct?

    You may have to help me, do you mean that the underlying $\infty$-functors are accessible? In that case the answer is yes.

    But you mention localization at an internal family of maps. This I don’t know about. Could you give me some pointer to more details?

25. • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeOct 14th 2014
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexSo [back here](https://golem.ph.utexas.edu/category/2011/12/reflective_subfibrations_facto.html) I argued that every exponential ideal is a localization at some class $S$ closed under finite products, and every reflective subcategory with stable units is a localization at some pullback-stable class $S$, but I ignored size issues. Is it true, if all the $\infty$-categories and functors involved are accessible, that these classes $S$ can be chosen to be small? (By an "internal family of maps" I mean rather than a set or class $S$ of maps in the external sense, we have an object $S$ of the topos and a map $X\to Y$ in $\mathbf{H}/S$. This is what the HIT construction of localization actually uses. But I'm pretty sure that this is strictly more general than a small external family, since we can always take $S$ to be a coproduct of copies of 1.)

    So back here I argued that every exponential ideal is a localization at some class $S$ closed under finite products, and every reflective subcategory with stable units is a localization at some pullback-stable class $S$, but I ignored size issues. Is it true, if all the $\infty$-categories and functors involved are accessible, that these classes $S$ can be chosen to be small?

    (By an “internal family of maps” I mean rather than a set or class $S$ of maps in the external sense, we have an object $S$ of the topos and a map $X\to Y$ in $\mathbf{H}/S$. This is what the HIT construction of localization actually uses. But I’m pretty sure that this is strictly more general than a small external family, since we can always take $S$ to be a coproduct of copies of 1.)

26. • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeOct 14th 2014
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks, I see. So I suppose you are well aware of [this proposition](http://ncatlab.org/nlab/show/reflective+sub-%28infinity%2C1%29-category#LocalizationAndAccessibility) which states that an accessible reflective sub-$\infty$-category of an accessible $\infty$-category is given by localization at a small set of morphisms. But I guess it may be nontrivial to combine this with pullback stability.

    Thanks, I see.

    So I suppose you are well aware of this proposition which states that an accessible reflective sub-$\infty$-category of an accessible $\infty$-category is given by localization at a small set of morphisms.

    But I guess it may be nontrivial to combine this with pullback stability.

27. • CommentRowNumber27.
    • CommentAuthorMike Shulman
    • CommentTimeOct 15th 2014
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI thought so when I wrote #25, but now I think maybe there is no problem. Of course a *small* set of morphisms can't be stable under pullback or products, so my question wasn't quite correctly phrased. The subtlety, IIRC, is that the "internal localization" at an arbitrary class $S$ is the "external localization" at the stabilization of $S$ under pullbacks or products, rather than $S$ itself. But if the external localization at a set $S$ is *known* to be an exponential ideal, then the class of morphisms that it inverts is necessarily stable under products; thus the internal localization agrees with the external one. Similarly, if the external localization is left exact, then the class of morphisms it inverts is pullback-stable. And I think we can play a similar game for subcategories with stable units, although in that case the class of *all* inverted morphisms may not be pullback-stable.

    I thought so when I wrote #25, but now I think maybe there is no problem. Of course a small set of morphisms can’t be stable under pullback or products, so my question wasn’t quite correctly phrased. The subtlety, IIRC, is that the “internal localization” at an arbitrary class $S$ is the “external localization” at the stabilization of $S$ under pullbacks or products, rather than $S$ itself. But if the external localization at a set $S$ is known to be an exponential ideal, then the class of morphisms that it inverts is necessarily stable under products; thus the internal localization agrees with the external one. Similarly, if the external localization is left exact, then the class of morphisms it inverts is pullback-stable. And I think we can play a similar game for subcategories with stable units, although in that case the class of all inverted morphisms may not be pullback-stable.

28. • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeJan 7th 2019
    • PermaLink
    Author: Urs
    Format: MarkdownItexadded full publication data for * [[Mike Shulman]], _Brouwer's fixed-point theorem in real-cohesive homotopy type theory_, Mathematical Structures in Computer Science Vol 28 (6) (2018): 856-941 ([arXiv:1509.07584](https://arxiv.org/abs/1509.07584), [doi:10.1017/S0960129517000147](https://doi.org/10.1017/S0960129517000147)) here and elsewhere <a href="https://ncatlab.org/nlab/revision/diff/cohesive+homotopy+type+theory/29">diff</a>, <a href="https://ncatlab.org/nlab/revision/cohesive+homotopy+type+theory/29">v29</a>, <a href="https://ncatlab.org/nlab/show/cohesive+homotopy+type+theory">current</a>

    added full publication data for

    • Mike Shulman, Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, Mathematical Structures in Computer Science Vol 28 (6) (2018): 856-941 (arXiv:1509.07584, doi:10.1017/S0960129517000147)

    here and elsewhere

    diff, v29, current

29. • CommentRowNumber29.
    • CommentAuthorUrs
    • CommentTimeMar 18th 2019
    • PermaLink
    Author: Urs
    Format: MarkdownItexadded pointer to * [[Mike Shulman]], _Comonadic modalities and cohesion_, talk at _[Geometry in Modal Homotopy Type Theory](http://www.andrew.cmu.edu/user/fwellen/modal-workshop.html)_, 2019 ([pdf slides](http://home.sandiego.edu/~shulman/papers/cmu2019a.pdf), [talk recording](https://youtu.be/GA93Hjh-Alk)) <a href="https://ncatlab.org/nlab/revision/diff/cohesive+homotopy+type+theory/30">diff</a>, <a href="https://ncatlab.org/nlab/revision/cohesive+homotopy+type+theory/30">v30</a>, <a href="https://ncatlab.org/nlab/show/cohesive+homotopy+type+theory">current</a>

    added pointer to

    • Mike Shulman, Comonadic modalities and cohesion, talk at Geometry in Modal Homotopy Type Theory, 2019 (pdf slides, talk recording)

    diff, v30, current

30. • CommentRowNumber30.
    • CommentAuthorUrs
    • CommentTimeFeb 1st 2023
    • PermaLink
    Author: Urs
    Format: MarkdownItexadded pointer to today's * [[David Jaz Myers]], [[Mitchell Riley]], *Commuting Cohesions* &lbrack;[arXiv:2301.13780](https://arxiv.org/abs/2301.13780)&rbrack; <a href="https://ncatlab.org/nlab/revision/diff/cohesive+homotopy+type+theory/41">diff</a>, <a href="https://ncatlab.org/nlab/revision/cohesive+homotopy+type+theory/41">v41</a>, <a href="https://ncatlab.org/nlab/show/cohesive+homotopy+type+theory">current</a>

    added pointer to today’s

    • David Jaz Myers, Mitchell Riley, Commuting Cohesions [arXiv:2301.13780]

    diff, v41, current

31. • CommentRowNumber31.
    • CommentAuthorUrs
    • CommentTimeFeb 1st 2023
    • PermaLink
    Author: Urs
    Format: MarkdownItexwhile I was at it, I have tried to bring the Idea-section and the References-section into better shape. The material in between these two seems somewhat random and may need attention. Good that the entry still carries the warning label "under construction". <a href="https://ncatlab.org/nlab/revision/diff/cohesive+homotopy+type+theory/42">diff</a>, <a href="https://ncatlab.org/nlab/revision/cohesive+homotopy+type+theory/42">v42</a>, <a href="https://ncatlab.org/nlab/show/cohesive+homotopy+type+theory">current</a>

    while I was at it, I have tried to bring the Idea-section and the References-section into better shape.

    The material in between these two seems somewhat random and may need attention. Good that the entry still carries the warning label “under construction”.

    diff, v42, current

32. • CommentRowNumber32.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 1st 2023
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexMorning thought. Re #30, I was reminded of our discussion of cohesive and equivariant modalities back [here](https://nforum.ncatlab.org/discussion/8915/orbifold-cohomology/?Focus=74379#Comment_74379): > they commute with each other. But currently they don’t communicate with each other. In the intro to the new paper they contrast commuting with nesting. Is there a communicating which isn't just a nesting?

    Morning thought.

    Re #30, I was reminded of our discussion of cohesive and equivariant modalities back here:

    they commute with each other. But currently they don’t communicate with each other.

    In the intro to the new paper they contrast commuting with nesting. Is there a communicating which isn’t just a nesting?

33. • CommentRowNumber33.
    • CommentAuthorUrs
    • CommentTimeFeb 1st 2023
    • (edited Feb 1st 2023)
    • PermaLink
    Author: Urs
    Format: MarkdownItexMaybe to amplify that they "they commute" but "don't communicate" may sound stronger than it is: In "commuting" orbisingular + real cohesion, the shape modality does *not* commute with the orbi-singular modality, and in this non-commutativity lies the distinction between geometric and homotopy fixed points and thus the whole content of equivariant homotopy theory.

    Maybe to amplify that they “they commute” but “don’t communicate” may sound stronger than it is: In “commuting” orbisingular + real cohesion, the shape modality does not commute with the orbi-singular modality, and in this non-commutativity lies the distinction between geometric and homotopy fixed points and thus the whole content of equivariant homotopy theory.

34. • CommentRowNumber34.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 2nd 2023
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexDoes any interesting non-commutativity appear elsewhere?

    Does any interesting non-commutativity appear elsewhere?

35. • CommentRowNumber35.
    • CommentAuthorUrs
    • CommentTimeFeb 2nd 2023
    • PermaLink
    Author: Urs
    Format: MarkdownItexDunno. The analogous pair for simplicial+smooth cohesion does commute (thm. 6.1.3 on [p. 30](https://arxiv.org/pdf/2301.13780.pdf#page=30) of Myers & Riley)

    Dunno. The analogous pair for simplicial+smooth cohesion does commute (thm. 6.1.3 on p. 30 of Myers & Riley)

36. • CommentRowNumber36.
    • CommentAuthorUrs
    • CommentTimeFeb 3rd 2023
    • PermaLink
    Author: Urs
    Format: MarkdownItexadded pointer also to this exposition: * [[David Jaz Myers]], *Simplicial, Differential, and Equivariant Homotopy Type Theory*, talk at [[CQTS]] (Jan 2023) &lbrack;video: [rec](https://nyu.zoom.us/rec/play/uk0LXy5ub2YUpJPhYq5p7GvpZ2I8_CZaWHSpWvZgwuUyHeWjXgUj2AQd21K1WSJo90V5DrE0BVhl7NuB.QbyHhtPHaJVQUj2A?continueMode=true&_x_zm_rtaid=Xyx9WZFLQzyRzu0Oh-2mNQ.1675318497581.13147cc7929a947e978b29124a207f98&_x_zm_rhtaid=938)&rbrack; <a href="https://ncatlab.org/nlab/revision/diff/cohesive+homotopy+type+theory/43">diff</a>, <a href="https://ncatlab.org/nlab/revision/cohesive+homotopy+type+theory/43">v43</a>, <a href="https://ncatlab.org/nlab/show/cohesive+homotopy+type+theory">current</a>

    added pointer also to this exposition:

    • David Jaz Myers, Simplicial, Differential, and Equivariant Homotopy Type Theory, talk at CQTS (Jan 2023) [video: rec]

    diff, v43, current

37. • CommentRowNumber37.
    • CommentAuthornLab edit announcer
    • CommentTimeJun 26th 2024
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexAdding reference * {#Aberle24} [[C.B. Aberlé]], *Parametricity via Cohesion* &lbrack;[arXiv:2404.03825](https://arxiv.org/abs/2404.03825)&rbrack; Anonymouse <a href="https://ncatlab.org/nlab/revision/diff/cohesive+homotopy+type+theory/48">diff</a>, <a href="https://ncatlab.org/nlab/revision/cohesive+homotopy+type+theory/48">v48</a>, <a href="https://ncatlab.org/nlab/show/cohesive+homotopy+type+theory">current</a>

    Adding reference

    • {#Aberle24} C.B. Aberlé, Parametricity via Cohesion [arXiv:2404.03825]

    Anonymouse

    diff, v48, current

38. • CommentRowNumber38.
    • CommentAuthornLab edit announcer
    • CommentTimeAug 9th 2024
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexAdded section on the mode theory of cohesive homotopy type theory Anonymouse <a href="https://ncatlab.org/nlab/revision/diff/cohesive+homotopy+type+theory/49">diff</a>, <a href="https://ncatlab.org/nlab/revision/cohesive+homotopy+type+theory/49">v49</a>, <a href="https://ncatlab.org/nlab/show/cohesive+homotopy+type+theory">current</a>

    Added section on the mode theory of cohesive homotopy type theory

    Anonymouse

    diff, v49, current