## Not signed in

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

## Site Tag Cloud

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

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeJun 27th 2018
• (edited Jun 27th 2018)

added pointer to a reference: Borceux 94, Vol 1, section 4.4

• CommentRowNumber2.
• CommentAuthorMike Shulman
• CommentTimeAug 21st 2018

In another thread, the question was raised of how constructive the epi-mono factorization is, e.g. whether its construction in Set can be done “internally” to produce it in any topos. The answer to that particular question, as recorded there, is yes.

Richard also wrote:

I think it is fairly easy to give a standard kind of Brouwerian counter-example to epi/mono factorisations existing constructively. Just take for instance a map $\mathbb{N} \rightarrow \mathbb{N} \times \mathbb{N}$ taking $n$ to $(p_{0}, p_{1}$), where $p_{0}$ is the smallest prime such that there is a prime $p_{1}$ with $p_{0} + p_{1} = 2n$ if such a $p_{0}$ exists, or else to $(0,0)$. One cannot (today at least!) determine the image of this map constructively, which one would need to construct the usual epi/mono factorisation.

I agreed (after making a stupid error) that this map is well-defined, but that doesn’t make it a Brouwerian counterexample. I don’t see any constructive problem with having the set of all prime numbers $p_0$ such that blah blah. A subset of a set $A$ is just a way to associated a proposition to every element of $A$, it doesn’t have to be decidable or anything of course. Even in setoid/PER models where epi-mono factorizations don’t exist, it’s still true that every map has an “image” – indeed, the problem is rather that it has two different images depending on what kind of “proposition” and hence what kind of “subset” you are looking at!

• CommentRowNumber3.
• CommentAuthorRichard Williamson
• CommentTimeAug 21st 2018
• (edited Aug 21st 2018)

Thanks for the reply! It would be nice to summarise the discussion of in what contexts the epi/mono factorisation can be made constructively on the nLab page.

I don’t see any constructive problem with having the set of all prime numbers $p_0$ such that blah blah.

For me it is problematic, because I think that constructively to give a set should mean to give an algorithm which can be used to construct the set, and that is not possible for the image of the map i gave (because, for instance, we do not know whether or not $(0,0)$ belongs to the image). The difference from this point of view between the function and its image is that the latter is a totality; one has to consider all $n \in \mathbb{N}$, and here exhausting all possibilities is not acceptable.

But if this is not the mainstream interpretation, that is fine, and answers my question. Thanks very much!

• CommentRowNumber4.
• CommentAuthorDavidRoberts
• CommentTimeAug 21st 2018

I was, coincidentally, just looking at the page image and the construction there of the regular image and the regular coimage. When I tried to view the page after making a small edit (with no comment), it gives me an error:

XML Parsing Error: mismatched tag. Expected: </ul>. Location: https://ncatlab.org/nlab/show/image Line Number 614, Column 3:
</div>
--^

• CommentRowNumber5.
• CommentAuthorDavidRoberts
• CommentTimeAug 21st 2018

Re #3

so I guess you only want to think about constructively decidable subsets (those whose characteristic function lands in the booleans), rather than arbitrary subsets (whose characteristic function maps to the object of all truth values)? And presumably ’decidable’ would means computable or something with a realiser, for you, since you want an algorithm. (possibly with bounded search space?) This feels like a kind of predicativism, but possibly not.

• CommentRowNumber6.
• CommentAuthorMike Shulman
• CommentTimeAug 22nd 2018

I think there’s a potentially interesting logic that is the internal logic of the fibration of complemented subobjects in a non-Boolean category (maybe a pretopos). This logic is “constructive” in some sense, but it still satisfies LEM, while it doesn’t have all existential quantifications and here not all images. I haven’t investigated it very much, but when I was a grad student I had an interesting conversation with Damir Dzhafarov which made me think that this logic ought to be at least related to the subsystems of set theory used in classical reverse mathematics.

• CommentRowNumber7.
• CommentAuthorRichard Williamson
• CommentTimeAug 22nd 2018
• (edited Aug 22nd 2018)

Re #4: Thanks very much, David, for pointing this out. There was another small bug in the table of contents renderer. I have fixed it now; hopefully it does not break any other pages!

The logic is a bit subtle in the table of contents renderer. Actually, with so many bright sparks here, maybe I can post the code, and perhaps somebody would be kind enough to go through it? Here it is. I have extracted it from a larger file; I think one should just be able to use the code if you would like to do so, but if there is something missing, let me know, and I’ll add it. Also let me know if you are not familiar with Python and need to know something in order to understand the code.

The bugs have been to do with closing the <ul> tags, which is handled towards the end, in the while loop, and just before and after it. The bug I just fixed was that there previously was

table_of_contents_html += "</ul>\n" * depth


rather than

table_of_contents_html += "</ul>\n" * (depth + 1)


towards the end.

(The while loop by the way could just begin while True rather than while depth < max_depth but I am using the latter for additional safety, to avoid busy looping endlessly in case of a programming error which leads to not exiting the loop.)

class EmptyHeaderException(Exception):
pass

pass

try:
except ValueError:
after_id = split_at_id[1]
href = after_id.split("'", 1)[0]

def _table_of_contents(page_content, placeholder):
page_lines = page_content.splitlines()
table_of_contents_html = "<div class='maruku_toc'>\n"
after_table_of_contents = False
for line in page_lines:
if not after_table_of_contents:
if placeholder in line:
after_table_of_contents = True
else:
continue
stripped_line = line.strip()
if not "<h" in stripped_line:
continue
try:
continue
"<li>" +
"<a href='#" +
href +
"'>" +
"</a>" +
"</li>" +
"\n")
table_of_contents_html += "<ul>\n"
else:
depth = 1
if depth == max_depth:
table_of_contents_html += "</ul>\n" * depth
continue
while depth < max_depth:
table_of_contents_html += "</ul>\n" * depth
else:
break
if depth + 1 == max_depth:
table_of_contents_html += "</ul>\n" * (depth + 1)
break
depth += 1
table_of_contents_html += "</div>\n"
return table_of_contents_html

1. I’ll reply to #5 and #6 later, thanks for the interest!

2. Re #5:

so I guess you only want to think about constructively decidable subsets (those whose characteristic function lands in the booleans), rather than arbitrary subsets (whose characteristic function maps to the object of all truth values)? And presumably ’decidable’ would means computable or something with a realiser, for you, since you want an algorithm. (possibly with bounded search space?)

In general, I am just guided by attempting to have a valid semantics for the kind of constructivism I have in mind, which is at its heart very simple: that one should be able to actually construct the things one wishes to treat. I realise that I may be going one step further than in Martin-Löf’s type theory, because I do not think that he considers it necessary to, from the beginning, take the notion of type to be constructively meaningful.

I am reluctant to agree too strongly, because it might lead to confusion if some aspect of it disagrees with the more philosophical point of view I just described, which is the primary thing for me. However, with that caveat, what you wrote does seem accurate yes, if decidable is, as you say, given constructive meaning. Whilst I am sympathetic to ultrafinitism, I am typically fine with allowing algorithms that are able to be carried out in principle, so an infinite amount of steps is not permitted, but a finite number would be allowed.

This feels like a kind of predicativism, but possibly not.

Yes, interestingly, exactly the same thought occurred to me. I agree that it does share something with predicativism.

Re #6: this sounds interesting! Presumably a bit different from my way of thinking, but interesting nonetheless.

• CommentRowNumber10.
• CommentAuthorMike Shulman
• CommentTimeAug 26th 2018

Richard, it might be helpful if you come up with a name for your kind of constructivism. That way, when you object that what someone else is doing doesn’t seem “constructive” to you, you can say “This doesn’t seem Williamson-constructive” or something, and then at least they won’t be confused or spend time explaining to you why it is perfectly “constructive” the way most other mathematicians use the word.

• CommentRowNumber11.
• CommentAuthorDavidRoberts
• CommentTimeAug 27th 2018

Ditto

3. Sincere apologies for any wasted time! As mentioned in the thread where this discussion came from, my intentions were genuine, and were not to lead things into a discussion of my views on constructivism. Those views are not systematically worked out or sophisticated anyhow, they are just my attempt to work out what constructivism as I see it philosophically means in practise. But out of the discussion came the realisation I mentioned in #9, that my point of view actually differs, it seems, from Martin-Löf’s when it comes to the meaning of what a ’type’ is; this, I think, should stick in my mind, and help me remember that the way I think about constructivism differs from the norm!