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

nLab > Latest Changes: presentation axiom

Bottom of Page

1 to 15 of 15

  1.  
    • CommentRowNumber1.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 10th 2012

    A number of examples and counterexamples have been firmed up at presentation axiom. Some of them devolve on an observation made by Jonas Frey a few days ago at internally projective object, for which I added a simple proof. There are still some points that needed to be clarified regarding the internalization of the presentation axiom, but for now the discussion is concentrated on relations between externally projeective and internally projective objects.

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeOct 10th 2012

    Very nice, thanks! Proposition 1 at internally projective object is very clarifying.

    There is however another notion of “internal presentation axiom”, namely

    for every morphism X→UX\to U, there exists an epi p:V↠Up:V\twoheadrightarrow U and an epi P↠p *XP\twoheadrightarrow p^*X such that PP is internally projective in E/VE/V.

    I think that’s what you would get by directly interpreting “every object is covered by a projective” in the stack semantics — and in particular, that’s what I would expect to need in order to directly internalize the proof that “1 is projective ⇒\Rightarrow CC”. Do you know anything about how this version is related to “every object is covered by an internally projective object”?

    • CommentRowNumber3.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 10th 2012

    Thanks for responding, Mike! I don’t know about this yet, and was actually hoping you’d have time to weigh in on this (no worries if you don’t).

    Let me think about it a tad more myself; I had been looking at a discussion between you and Jonas from about a year ago which seems related. I could follow some but not all that discussion (I did follow it completely up through where Jonas points out the flaw in Johnstone’s argument), but I had some trouble after that).

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeOct 12th 2012

    I don’t really have time to think about this deeply right now, unfortunately, although I would like to understand it better. Is it mainly my comment #4 from that other discussion that wasn’t clear? (I haven’t looked at it carefully; it could be that I was completely wrong.)

    • CommentRowNumber5.
    • CommentAuthorNikolajK
    • CommentTimeJun 8th 2020

    In the idea section it says that CoSHEP is itself the presentation axiom, but “Axiom (CoSHEP) 2.1.” strikes me as a bit short. It reads

    “For every set A, there exists a set P and a surjection P→A, such that every surjection X↠P has a section.”

    while I would expect something like

    “For every set A, there exists a set P and a surjection P→A, such that P is projective. The latter means that for any f:P→C and epi p:B→C, there is a lift from P into B.”

    If it’s just “every surjection X↠P has a section” then I seem to miss the whole triangle in the definition right below.

    Either the axiom isn’t right, or there’s two axioms, or somehow the letters can all come together (in particular, I’m not sure if the “A” is the same in the axiom and the definition) and I don’t see that this axiom statement already gives the definition property.

    • CommentRowNumber6.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 8th 2020
    • (edited Jun 8th 2020)

    So if p:B→Ap: B \to A is epic, then for any f:P→Af: P \to A as in Axiom 2.1, one can pull back the epi pp along ff to get an epi q:X→Pq: X \to P. This has a section s:P→Xs: P \to X. Compose this with the other projection h:X→Bh: X \to B of the pullback to get the desired lift g:P→Bg: P \to B.

    • CommentRowNumber7.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 30th 2020

    Added full references and links Palmgren and Rathjen papers.

    diff, v46, current

    • CommentRowNumber8.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 5th 2022

    Added example

    diff, v49, current

  9. started section on relation between CoSHEP and sets cover

    Vladimir Rostov

    diff, v51, current

    • CommentRowNumber10.
    • CommentAuthorShamrock
    • CommentTimeFeb 23rd 2024
    > This argument can be made precise in many forms of type theory (including those of Martin-Löf and Thierry Coquand), which thus justify CoSHEP, much as they are widely known to justify dependent choice.

    Can someone elaborate on this, or give a reference?

  11. Toby Bartels probably has some references considering that he was the one to add the justification section and that particular sentence when he created the article back in 2009: https://ncatlab.org/nlab/revision/presentation+axiom/1.

    • CommentRowNumber12.
    • CommentAuthorMadeleine Birchfield
    • CommentTimeFeb 23rd 2024
    • (edited Feb 23rd 2024)

    Note that the sentence was written before Vladimir Voevodsky defined propositions and h-levels and others defined higher inductive types, and before the general trend towards viewing types as general ∞\infty-groupoids rather than sets or propositions in Martin-Löf type theory and Coq, all which only happened in the 2010s.

    These days, I’m not sure if there is anything special about type theory in particular. Using the propositional truncation, defined as a higher inductive type or impredicatively from a type of all propositions, one has a ready made predicate logic inside of Martin-Löf type theory or Coq itself, and one can add a model of IZF or IETCS with the presentation axiom to the type theory and simply work inside of the model of IZF or IETCS. The justification for the presentation axiom there should be the same as the justification for adding the presentation axiom to any other universe in the type theory.

    • CommentRowNumber13.
    • CommentAuthorMadeleine Birchfield
    • CommentTimeFeb 23rd 2024
    • (edited Feb 23rd 2024)

    Also, without propositional truncations, one can’t even define surjections in Martin-Löf type theory, so one can’t even formulate the presentation axiom in the first place. One can only define split surjections, and the untruncated version of the presentation axiom (which may be what Toby Bartels is referring to when he is referencing the BHK interpretation of logic) says that every set AA has a set PP and a split surjection P→AP \to A such that every split surjection into PP has a section, and is trivially true by definition of split surjection and by taking PP to be AA and the split surjection P→AP \to A to be the identity function on AA.

    Personally for me, if you are using the untruncated versions of axioms to justify the truncated versions of axioms, then you can use the same reasoning to justify global choice operators.

  14. Added a section on the presentation axiom in dependent type theory

    Anonymouse

    diff, v52, current

  15. The new section is really about how the BHK interpretation interacts with the presentation axiom, and can be made in any foundations, not just dependent type theory

    Anonymouse

    diff, v52, current

1 to 15 of 15

  1.