Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
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\to U$, there exists an epi $p:V\twoheadrightarrow U$ and an epi $P\twoheadrightarrow p^*X$ such that $P$ is internally projective in $E/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”?
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).
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.)
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.
So if $p: B \to A$ is epic, then for any $f: P \to A$ as in Axiom 2.1, one can pull back the epi $p$ along $f$ to get an epi $q: X \to P$. This has a section $s: P \to X$. Compose this with the other projection $h: X \to B$ of the pullback to get the desired lift $g: P \to B$.
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.
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.
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 $A$ has a set $P$ and a split surjection $P \to A$ such that every split surjection into $P$ has a section, and is trivially true by definition of split surjection and by taking $P$ to be $A$ and the split surjection $P \to A$ to be the identity function on $A$.
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.
1 to 15 of 15