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.
added pointer to a reference: Borceux 94, Vol 1, section 4.4
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 taking to ), where is the smallest prime such that there is a prime with if such a exists, or else to . 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 such that blah blah. A subset of a set is just a way to associated a proposition to every element of , 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!
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 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 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 , 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!
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>
--^
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.
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.
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
class _NotAHeaderException(Exception):
pass
def _split_header(header_line):
split_at_header_beginning = header_line.split("<h", 1)
after_header_beginning = split_at_header_beginning[1]
try:
header_size = int(after_header_beginning[0])
except ValueError:
raise _NotAHeaderException()
if header_size > 5 or header_size < 2:
raise _NotAHeaderException()
split_at_id = after_header_beginning.split("id='", 1)
after_id = split_at_id[1]
href = after_id.split("'", 1)[0]
after_header_tag = after_header_beginning.split(">",1)[1]
header = after_header_tag.split("</h")[0]
return header_size, href, header
def _table_of_contents(page_content, placeholder):
page_lines = page_content.splitlines()
current_header_size = 1
header_sizes = []
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:
header_size, href, header = _split_header(stripped_line)
except _NotAHeaderException:
continue
if not header:
raise EmptyHeaderException()
header_contents_html = (
"<li>" +
"<a href='#" +
href +
"'>" +
header +
"</a>" +
"</li>" +
"\n")
if header_size == current_header_size:
table_of_contents_html += header_contents_html
elif header_size > current_header_size:
table_of_contents_html += "<ul>\n"
table_of_contents_html += header_contents_html
header_sizes.append(header_size)
current_header_size = header_size
else:
header_sizes.pop()
max_depth = len(header_sizes)
depth = 1
if depth == max_depth:
table_of_contents_html += "</ul>\n" * depth
table_of_contents_html += header_contents_html
current_header_size = 2
continue
while depth < max_depth:
previous_header_size = header_sizes.pop()
if previous_header_size <= header_size:
table_of_contents_html += "</ul>\n" * depth
table_of_contents_html += header_contents_html
if previous_header_size != header_size:
header_sizes.extend([previous_header_size, header_size])
else:
header_sizes.append(header_size)
current_header_size = header_size
break
if depth + 1 == max_depth:
table_of_contents_html += "</ul>\n" * (depth + 1)
table_of_contents_html += header_contents_html
current_header_size = 2
break
depth += 1
table_of_contents_html += "</ul>\n" * len(header_sizes)
table_of_contents_html += "</div>\n"
return table_of_contents_html
I’ll reply to #5 and #6 later, thanks for the interest!
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.
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.
Ditto
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!
1 to 12 of 12