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 definitions 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 nlab noncommutative noncommutative-geometry number-theory object 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

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).

nLab > Latest Changes: effective epimorphism in homotopy type theory

Bottom of Page

1 to 5 of 5

  1.  

  1. Page created, but author did not leave any comments.

    Anonymous

    v1, current

  2. The definition given in the article is actually that of a surjection or surjective map, as defined in section 4.6 of the HoTT Book and in section 15.2 of Introduction to Homotopy Type Theory. I don’t know of any reference in the dependent type theory literature that calls these functions “effective epimorphisms”. Seeing as the surjection article already has a section titled dependent type theory containing the exact same definition as found in this article, I think this page can be deleted and its contents merged into the surjection article if necessary.

  3. Alternatively, we can try to adopt the definition of effective epimorphism in terms of its Čech nerve to the setting of homotopy type theory from Jacob Lurie’s HTT, but I’m not sure if such a colimit is even definable in vanilla homotopy type theory without additional ∞\infty-categorical machinery via two-level type theory or simplicial type theory.

  4. According to Mike Shulman, the Čech nerve is a simplicial type and so isn’t currently definable in homotopy type theory, since we don’t know how to define simplicial or semi-simplicial types. So I don’t think the Lurie definition of effective epimorphism is currently possible to formulate in homotopy type theory either.

  5. Replaced the material in the page which defined surjections with the correct definition of an effective epimorphism from Lurie using the Čech nerve, and added a paragraph explaining that we don’t actually know how to define an effective epimorphism in homotopy type theory yet since we don’t know how to construct semi-simplicial types and Čech nerves in homotopy type theory.

    diff, v2, current

1 to 5 of 5

  1.