Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

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

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 29th 2017

    Since we know of A string diagram calculus for predicate logic, what prospects are there for HoTT? If there is a useful such notation, can we imagine what it might look like? I guess there are many aspects to include – (,1)(\infty, 1), cartesian, closed, object classifier, …

    But perhaps advances by Mike on this front might be useful first:

    In categorical semantics a context is interpreted by the same object as its dependent sum, but in the type theoretic syntax the distinction matters a lot. This is hard to understand from a categorical perspective, but I’m gradually putting together a way to see it from that point of view too. The short answer is that it has to do with the difference between monoidal categories and multicategories.

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeMar 29th 2017

    Generally I think of string diagrams and type theory as parallel. They serve the same general purpose — a syntactic presentation of free categories that simplifies proofs internal to some kind of structured category — but in very different ways.

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 30th 2017
    • (edited Mar 30th 2017)

    Yes, you stressed the free category aspect in your recent paper. So are there rules of thumb to say which aspects are most efficiently represented by string diagrams and by type theories?

    Perhaps string diagrams serve well the monoidal aspect and indexing. Being monoidal closed without duals seems less straightforward, as in John Baez’s bubble diagrams.

    Could there be a best of both worlds approach?

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeMar 30th 2017


    • CommentRowNumber5.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 31st 2017
    • (edited Feb 11th 2018)

    Strange how two early pioneers of predicate logic, Peirce and Frege, each adopted 2-dimensional notations which relate to the different notation styles – string diagram and type theory (well at least aspects of type theory are drawn from Frege).