2,110 reputation
517
bio website mimuw.edu.pl/~mrp
location Poland
age
visits member for 3 years, 5 months
seen yesterday

I eat vegetarians.

If you repeat ``p or not p'' often enough, it becomes the truth.


Aug
24
revised Continuous relations?
Fixed English
Aug
23
comment Time in Girard's Geometry of Interaction
Sometimes, some people say some things, not because the things are true, deep, or in any sense smart, but to make other people think. Such people, are usually called "controversial" (sometimes even "excentric") by the community. For sure, Y.J. Girard is one of the greatest logicians of our time; yet he is a bit "controversial" :-)
Aug
23
answered Continuous relations?
Aug
19
comment Explicit description of the oplax limit of a functor to Cat?
@JasonGross, this question was answered in more detail before (see Mike's answer and my explanation): mathoverflow.net/questions/164343/…
Aug
18
comment In the category of sets epimorphisms are surjective - Constructive Proof?
@AndreasCaicedo, I do not understand why you have removed tag "set-theory". As for me, the question is exactly about set theory (moreover, it is formulated in such a way, that it is about the standard set theory).
Aug
18
comment In the category of sets epimorphisms are surjective - Constructive Proof?
@ZhenLin, aws: yes, you're, of course, right --- it seems that I'm getting old and seeing things which are not :-) So, to conclude the series of comments: "surjection iff epi" holds in every pretopos.
Aug
18
comment In the category of sets epimorphisms are surjective - Constructive Proof?
(...) but I don't see any reason why every $\Pi \Sigma$-pretopos, or any other notion of a predicative universe should be balanced (of course, CZF is balanced, so technically your claim is correct, but I'd like to see the exact reason behind this fact).
Aug
18
comment In the category of sets epimorphisms are surjective - Constructive Proof?
Sorry, then I still don't understand your construction --- could you write it down in a bit more formal way? I don't claim that you're wrong, I just want to understand what exactly you are doing. I think your proof cannot be carried to a general predicative universe --- I claim that in any regular category the statement "epi iff surjection" is equivalent to "bimorphism iff iso" (i.e. to the statement that the category is balanced). Clearly, every topos is balanced (because $\Omega$ classifies morphism), (cont...)
Aug
18
comment In the category of sets epimorphisms are surjective - Constructive Proof?
Then, $f, g : B \rightarrow \Omega$ become predicates on $B$, where $f$ expresses the statement that $h$ is internally surjective, and $g := \top_B$. Therefore, $f = g$ says that "$h$ is internally injective" is true.
Aug
18
comment In the category of sets epimorphisms are surjective - Constructive Proof?
Actually, you need the power-set axiom to write your first definition. The second one, just says that $C := \mathcal{P}(\{0\}) = \Omega$, where $\Omega$ is the set of internal truth-values.
Aug
18
comment Notion of infinity in categories
@SamHopkins, if you impose a condition on all objects of a category, then it'll become a condition imposed on the category.
Aug
18
revised In the category of sets epimorphisms are surjective - Constructive Proof?
added 13 characters in body
Aug
18
comment Notion of infinity in categories
BTW, I think, Sanath's answer is really good --- I don't see any general constructions of a non-iso (endo-)monic that can be transferred from a subobject, except the case of Theorem 1.
Aug
18
comment Notion of infinity in categories
@AsafKaragila, no, his statement is not equivalent to yours (it would be equivalent if you replaced "which is not epic" with "which is not iso").
Aug
18
answered In the category of sets epimorphisms are surjective - Constructive Proof?
Aug
12
comment Category which has no non-trivial adjoint functors
But, what I really meant, is that when $\mathbb{C}$ is a $\mathbf{Set}$-internal category, then the category of large $\mathbb{C}$-internal sets is always closed under power objects. BTW, There is no concept like a "class" in ZFC (in contrast to NBG), so you have to formalize somehow what you mean. In my experience, when it comes to category theory, every formalization of the concept of class that does not satisfy the reflection principle does more harm than good, and only confuses people.
Aug
12
comment Category which has no non-trivial adjoint functors
@MikeShulman, Its not about the category of fibrations being closed under power objects (which is, of course, not), but about the category of discrete fibrations --- i.e. the question is whether $\mathbf{Set}^{\mathbb{C}^{op}}$ is closed under power objects, or not. This question, on the other hand, depends on the notion of $\mathbf{Set}$ and the size of $\mathbb{C}$, and is (almost) completely independent of the status of your meta-classes (i.e. whether they are closed under power-objects or not). (cont)
Aug
9
comment Category which has no non-trivial adjoint functors
@EricWofsey, this is the only reasonable concept for studying internal categories. On the other hand, I have never heard of any useful mathematical results concerning "large" categories, when you assume that the concept of "large" is not set-theoretic.
Aug
9
comment Category which has no non-trivial adjoint functors
If your concept of "large" is closed under power-objects, then in exactly the same way as for "small" categories.
Aug
9
comment Category which has no non-trivial adjoint functors
@EricWofsey, I don't think there are any reasonable set-theoretic issues. If you recall that (any) set theory is closed under set-theoretic operations, then it'll be obvious, that due to cardinality reasons, you may always find such $A$.