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.
   • CommentAuthorAli Caglayan
   • CommentTimeSep 4th 2018
   • (edited Sep 4th 2018)
   • PermaLink
   Author: Ali Caglayan
   Format: TextI have created a page for pointed types as these will be referenced alot. I have also added some nonsense of this being a modality? If there is anybody who knows what they are talking about could they confirm this, otherwise I shall remove it. [[homotopytypetheory:pointed type]]

   I have created a page for pointed types as these will be referenced alot. I have also added some nonsense of this being a modality? If there is anybody who knows what they are talking about could they confirm this, otherwise I shall remove it. pointed type (homotopytypetheory)
2. • CommentRowNumber2.
   • CommentAuthorDavid_Corfield
   • CommentTimeSep 4th 2018
   • PermaLink
   Author: David_Corfield
   Format: TextThere's the [[maybe monad]], which isn't idempotent, so not a modality (if that condition was included).

   There's the maybe monad, which isn't idempotent, so not a modality (if that condition was included).
3. • CommentRowNumber3.
   • CommentAuthorDavid_Corfield
   • CommentTimeSep 4th 2018
   • PermaLink
   Author: David_Corfield
   Format: TextI guess the question needs to be addressed of the optimal level of cross-referencing. On the nLab there is [[pointed object]] and [[pointed type]] (the latter minimal). Ideally would people want the HoTT wiki to give just a HoTT description of a term with references to relevant nLab entries? And with anything like the density of links in nLab pages? Similarly in reverse.

   I guess the question needs to be addressed of the optimal level of cross-referencing. On the nLab there is pointed object and pointed type (the latter minimal).
   
   Ideally would people want the HoTT wiki to give just a HoTT description of a term with references to relevant nLab entries? And with anything like the density of links in nLab pages? Similarly in reverse.
4. • CommentRowNumber4.
   • CommentAuthorAli Caglayan
   • CommentTimeSep 4th 2018
   • (edited Sep 4th 2018)
   • PermaLink
   Author: Ali Caglayan
   Format: MarkdownItexActually checking the definition of reflective subuniverse from the HoTT book it says that a type $X\to X+1$ is an equivalence iff $X$ is pointed which is of course complete nonsense. I shall clean up the pointed type page.

   Actually checking the definition of reflective subuniverse from the HoTT book it says that a type $X\to X+1$ is an equivalence iff $X$ is pointed which is of course complete nonsense. I shall clean up the pointed type page.

5. • CommentRowNumber5.
   • CommentAuthorAli Caglayan
   • CommentTimeSep 4th 2018
   • PermaLink
   Author: Ali Caglayan
   Format: MarkdownItexI think we are sticking with a HoTT wiki capable of supporting itself and lots of 'see also' to the nlab. Part of the appeal of HoTT is that it should be better for doing mathematics than current ways so part of that appeal should be simplicity. I fear that the mere sight of an (oo,1) will scare many people away. Essentially HoTT Wiki would detail how to do anything in HoTT.

   I think we are sticking with a HoTT wiki capable of supporting itself and lots of ’see also’ to the nlab. Part of the appeal of HoTT is that it should be better for doing mathematics than current ways so part of that appeal should be simplicity. I fear that the mere sight of an (oo,1) will scare many people away. Essentially HoTT Wiki would detail how to do anything in HoTT.