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 k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum 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 sheaves 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.
   • CommentAuthorDean
   • CommentTimeSep 10th 2020
   • (edited Sep 10th 2020)
   • PermaLink
   Author: Dean
   Format: MarkdownItexCan the nlab's articles take in Javascript or Java applets? I was thinking of making a simple type theory parser for nlab's pages with type theory (syntax much the same as type theory). For instance, I would make one to be embedded in the page on Lawvere's diagonal argument. I have the theory sorted out already, so it's just a matter of writing it up. I found an algorithm that simplifies triangle identities in worst case $O(\sum_{i = 1}^n m_i l)$ where $n$ is the number of counits in a diagram, $m_i$ is the number of units in a diagram adjacent to a given counit. On average, $m_i$ and $n$ will be small in proportion to $l$. (I'm interested to see if anyone can make a better triangle recognition algorithm for triangle identities in a strict $2$-category - it seems there are tons of tricks one can do).

   Can the nlab’s articles take in Javascript or Java applets? I was thinking of making a simple type theory parser for nlab’s pages with type theory (syntax much the same as type theory). For instance, I would make one to be embedded in the page on Lawvere’s diagonal argument. I have the theory sorted out already, so it’s just a matter of writing it up. I found an algorithm that simplifies triangle identities in worst case $O(\sum_{i = 1}^n m_i l)$ where $n$ is the number of counits in a diagram, $m_i$ is the number of units in a diagram adjacent to a given counit. On average, $m_i$ and $n$ will be small in proportion to $l$. (I’m interested to see if anyone can make a better triangle recognition algorithm for triangle identities in a strict $2$-category - it seems there are tons of tricks one can do).

2. • CommentRowNumber2.
   • CommentAuthorRichard Williamson
   • CommentTimeSep 10th 2020
   • PermaLink
   Author: Richard Williamson
   Format: MarkdownItexHi Dean, I can add probably add whatever you have in mind on a per request basis for now. I am not quite sure what you have in mind, but if you send me an example with instructions on what you wish to do with it, I can try to add it.

   Hi Dean, I can add probably add whatever you have in mind on a per request basis for now. I am not quite sure what you have in mind, but if you send me an example with instructions on what you wish to do with it, I can try to add it.

3. • CommentRowNumber3.
   • CommentAuthorDean
   • CommentTimeSep 10th 2020
   • PermaLink
   Author: Dean
   Format: MarkdownItexOk - I'll let you know in a few weeks when I've made the applet.

   Ok - I’ll let you know in a few weeks when I’ve made the applet.

4. • CommentRowNumber4.
   • CommentAuthorRichard Williamson
   • CommentTimeSep 10th 2020
   • PermaLink
   Author: Richard Williamson
   Format: MarkdownItexSounds good! I'd prefer Javascript to a Java applet if possible.

   Sounds good! I’d prefer Javascript to a Java applet if possible.

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeSep 11th 2020
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI don't really understand -- what are you envisioning this app would do?

   I don’t really understand – what are you envisioning this app would do?

6. • CommentRowNumber6.
   • CommentAuthorDean
   • CommentTimeSep 11th 2020
   • PermaLink
   Author: Dean
   Format: MarkdownItexIt's a small functional programming tool that uses the same notation as type theory. I was thinking of putting one here, for instance: https://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theorem#precise_statement (There's simple ways of preventing infinite regress.) There would be a feature where the program gives as an output each step in the argument. It contains the judgements of type theory as string rewrite rules (we supply which direction is "simpler"). The idea is based on interpreting type theory as rewrite rules for diagrams in a strict 2-category.

   It’s a small functional programming tool that uses the same notation as type theory. I was thinking of putting one here, for instance:

   https://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theorem#precise_statement

   (There’s simple ways of preventing infinite regress.) There would be a feature where the program gives as an output each step in the argument.

   It contains the judgements of type theory as string rewrite rules (we supply which direction is “simpler”). The idea is based on interpreting type theory as rewrite rules for diagrams in a strict 2-category.

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeSep 11th 2020
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexSorry, that's not enough explanation for me to understand. What is the overall goal? What are you expecting the user to see? What would they do to interact with it?

   Sorry, that’s not enough explanation for me to understand. What is the overall goal? What are you expecting the user to see? What would they do to interact with it?