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.
Started writing regular and exact completion.
Mike has added many interesting properties of these completions now.
Do you know, I find myself thinking that an interesting argument against the powerset axiom is that unlike basically all the other logical/set-theoretic properties of categories, it is not preserved by the free ex/lex completion. Given that (in the absence of choice) is not necessarily a topos, and in fact isn't even well-powered relative to the original category Set, it becomes philosophically less self-evident to me that Set itself should be a topos. Especially since from the type-theoretic defined-equality point of view, Set is itself an ex/lex completion (of the category of presets).
Ha ha, we'll make a predicativist out of you yet!
I added some more properties of regular and exact completions, including that the ex/lex and reg/lex completions can never stabilize unless they do so in one step, and that they are Boolean if and only if the original category satisfies AC. I also added a higher-categorical perspective, and deleted the query box at regular category since its content was basically subsumed by my recent additions, and probably regular and exact completions would be a better place to continue it anyway.
I have some questions for Mike at regular and exact completions.
Good questions, I've answered them.
Thanks at regular and exact completions.
1 to 8 of 8