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.
   • CommentAuthorDavid_Corfield
   • CommentTimeJan 17th 2013
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexSay we follow the coalgebraic community's treatment of modality, where we begin with a Stone duality situation relating the algebra generated by syntax to the semantic space of models (e.g., Boolean algebras and Stone spaces). Then on each side of the duality we have an endofunctor, allowing us to lift the Stone duality to a duality between algebras on one side and colagebras on the other, as in eq (3) of [this](http://arxiv.org/pdf/cs/0605128v1.pdf). E.g., we have a [duality](http://www.cs.le.ac.uk/people/akurz/Papers/StoneCoalgebras/kkv.pdf) between modal algebras and general descriptive frames. Now, if HoTT [participates](http://nforum.mathforge.org/discussion/4623/duality-for-homotopy-type-theories/?Focus=37603#Comment_37603) in a Stone-like duality, can we see Mike's work on [Modal type theory](http://uf-ias-2012.wikispaces.com/file/view/modalitt.pdf/376001920/modalitt.pdf) in a coalgebraic light? What kind of 'spatial' collection would be formed of models for a dependent type theory, and how would the modal operator dualise to glue the models together? If sheaves provide semantics for first-order modal logic (Awodey-Kishida), wouldn't you expect [[infinity-stacks]] to feature?

   Say we follow the coalgebraic community’s treatment of modality, where we begin with a Stone duality situation relating the algebra generated by syntax to the semantic space of models (e.g., Boolean algebras and Stone spaces). Then on each side of the duality we have an endofunctor, allowing us to lift the Stone duality to a duality between algebras on one side and colagebras on the other, as in eq (3) of this. E.g., we have a duality between modal algebras and general descriptive frames.

   Now, if HoTT participates in a Stone-like duality, can we see Mike’s work on Modal type theory in a coalgebraic light?

   What kind of ’spatial’ collection would be formed of models for a dependent type theory, and how would the modal operator dualise to glue the models together?

   If sheaves provide semantics for first-order modal logic (Awodey-Kishida), wouldn’t you expect infinity-stacks to feature?

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeJan 22nd 2013
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexHow do you derive the notion of Stone space from the notion of Boolean algebra? What is the corresponding thing for e.g. Heyting algebras?

   How do you derive the notion of Stone space from the notion of Boolean algebra? What is the corresponding thing for e.g. Heyting algebras?

3. • CommentRowNumber3.
   • CommentAuthorDavid_Corfield
   • CommentTimeJan 22nd 2013
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexWhat kind of questions are these? In the Baezian kindly teacher showing first steps mode? Or the 'something important you haven't thought about' mode? You can't just mean the usual account of Stone duality for the first question. Is there something in that word 'notion'? I'd never heard of [Esakia duality](http://en.wikipedia.org/wiki/Esakia_duality) before. Is that a standard name?

   What kind of questions are these? In the Baezian kindly teacher showing first steps mode? Or the ’something important you haven’t thought about’ mode? You can’t just mean the usual account of Stone duality for the first question. Is there something in that word ’notion’?

   I’d never heard of Esakia duality before. Is that a standard name?

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeJan 23rd 2013
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexHey, cool, I've never heard of Esakia spaces either! I guess what I was wondering was whether there is some abstract machine into which you could plug the notion of Boolean algebra and it would spit out the notion of Stone space, since then we could try to (categorify it and) apply it to type theories. I mean, of course there is the Stone duality argument $FinBool \simeq FinSet^{op}$, hence $$Bool \simeq Ind(FinBool) \simeq Ind(FinSet^{op}) \simeq Pro(FinSet)^{op}$$ but the part that's always been a bit mysterious to me is why pro-(finite sets) can be identified with certain topological spaces. Does that categorify? Does $FinBool\simeq FinSet^{op}$ categorify? Is there something obvious I'm forgetting?

   Hey, cool, I’ve never heard of Esakia spaces either!

   I guess what I was wondering was whether there is some abstract machine into which you could plug the notion of Boolean algebra and it would spit out the notion of Stone space, since then we could try to (categorify it and) apply it to type theories. I mean, of course there is the Stone duality argument $FinBool \simeq FinSet^{op}$, hence

   $$Bool \simeq Ind(FinBool) \simeq Ind(FinSet^{op}) \simeq Pro(FinSet)^{op}$$

   but the part that’s always been a bit mysterious to me is why pro-(finite sets) can be identified with certain topological spaces. Does that categorify? Does $FinBool\simeq FinSet^{op}$ categorify? Is there something obvious I’m forgetting?

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeJan 23rd 2013
   • (edited Jan 23rd 2013)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI went to check what our entry _[[Stone duality]]_ has to say about this and found that it curretly it doesn't have to say much at all. While I was at it, I at least copied Mike's line of equivalences above to _[Stone duality -- Stone spaces and Boolean algebras](http://ncatlab.org/nlab/show/Stone+duality#StoneSpacesAndBooleanAlgebras)_ and added a brief explanation.

   I went to check what our entry Stone duality has to say about this and found that it curretly it doesn’t have to say much at all.

   While I was at it, I at least copied Mike’s line of equivalences above to Stone duality – Stone spaces and Boolean algebras and added a brief explanation.

6. • CommentRowNumber6.
   • CommentAuthorTodd_Trimble
   • CommentTimeJan 23rd 2013
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexRather more work remains to be done on Stone duality. For example, I saw no mention of ambimorphic or dualizing objects, which is obviously a central idea.

   Rather more work remains to be done on Stone duality. For example, I saw no mention of ambimorphic or dualizing objects, which is obviously a central idea.

7. • CommentRowNumber7.
   • CommentAuthorZhen Lin
   • CommentTimeJan 23rd 2013
   • PermaLink
   Author: Zhen Lin
   Format: MarkdownItex@Mike If I had to guess, I would look at something like "take the frame completion of (the distributivisation of) the lattice of quotients". Or probably equivalently, look at the topos of canonical sheaves on the lattice of quotients. (This hopefully also recovers the notion of Zariski spectrum.) Then the categorification would be "take the Grothendieck topos completion". But maybe I've been reading too much of Olivia Caramello's work...

   @Mike If I had to guess, I would look at something like “take the frame completion of (the distributivisation of) the lattice of quotients”. Or probably equivalently, look at the topos of canonical sheaves on the lattice of quotients. (This hopefully also recovers the notion of Zariski spectrum.) Then the categorification would be “take the Grothendieck topos completion”. But maybe I’ve been reading too much of Olivia Caramello’s work…

8. • CommentRowNumber8.
   • CommentAuthorDavid_Corfield
   • CommentTimeJan 23rd 2013
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexWe have some clues as to what happens when dualising up the ladder, if we take predicate logic to be a rung up from propositional logic. On the one hand, there's the Boolean coherent category (algebra/syntax) - Stone groupoid (topology/semantics) [duality](http://golem.ph.utexas.edu/category/2009/03/firstorder_logical_duality.html) of Forssell and Awodey. On the other, there's the hyperdoctrine - indexed Stone spaces [duality](http://www.math.ru.nl/~coumans/talkmlnl.pdf) of Coumans. So there should be a way to understand Stone groupoids as indexed Stone spaces, I guess. Or at least with the indexing over general types.

   We have some clues as to what happens when dualising up the ladder, if we take predicate logic to be a rung up from propositional logic. On the one hand, there’s the Boolean coherent category (algebra/syntax) - Stone groupoid (topology/semantics) duality of Forssell and Awodey. On the other, there’s the hyperdoctrine - indexed Stone spaces duality of Coumans.

   So there should be a way to understand Stone groupoids as indexed Stone spaces, I guess. Or at least with the indexing over general types.