ZFC image

Stream: maths

[Violeta Hernández]

I have two different questions, both regarding docs#Set.image

[Violeta Hernández]

First. What's the deal with the definable condition? I think we discussed it many months before but I don't remember what was said.

[Violeta Hernández]

I think the purpose of this is that declaring that this set exists is equivalent to replacement, but in practice nothing seems to come out of this.

[Violeta Hernández]

@Mario Carneiro probably has a good reason for this though.

[Violeta Hernández]

Second. I want to define an alternate version that takes in a general type (of the appropriate universe) instead of a set. What should it be called?

[Mario Carneiro]

The intention was to be able to construct choice-free proofs of sets in ZF, and prove instances of replacement without using lean's choice

[Violeta Hernández]

Ah I see, I can get behind that

[Mario Carneiro]

it wasn't critical for my goals though so I just made a classical instance and didn't worry too much about it

[Mario Carneiro]

I don't understand your second question

[Mario Carneiro]

what is in a general type here?

[Violeta Hernández]

The type signature would be this

def foo_image {\a : Type u} {f : \a -> Set.{max u v}} : Set.{max u v} := sorry

[Violeta Hernández]

This isn't trivial to construct, it's kind of a more general replacement

[Violeta Hernández]

I don't even have naming suggestions here. Anything is appreciated.

[Violeta Hernández]

I guess image' is the easy pic but I'm not a fan

[Mario Carneiro]

It looks like Set.range or Set.range' to me