functor universe

Stream: general

[Patrick Massot]

Is there any way to make the definition of functor more universe polymorphic? If I define

instance : functor topological_space :=
{ map := λ _ _ f, topological_space.coinduced f }

Then I think I can use f <*> T only if the source and target of f live in the same universe.

[Mario Carneiro]

unfortunately no

[Patrick Massot]

Is it a limitation of the underlying type theory?

[Mario Carneiro]

For it to be more universe polymorphic it has to be free-standing functions

[Mario Carneiro]

yes

[Patrick Massot]

What is a free-standing function?

[Mario Carneiro]

i.e. option.map instead of the map component of functor option

[Johan Commelin]

s/i.e./e.g./

[Mario Carneiro]

You can't hold a lemma that says that map is functorial as a hypothesis, because that statement involves quantifying over universes so it would be an existential universe variable if it was a hypothesis. But you can prove that every particular polymorphic map function is functorial polymorphically

[Patrick Massot]

Ok, this is what I observed, but I wanted to make sure. Too bad

[Patrick Massot]

Thanks!

[Simon Hudon]

Footnote: there is a way around this limitation but you need to formulate your functor as a relation between two functors e.g. option.{v} and option.{u}

[Simon Hudon]

When you need it, it works but you're better off avoiding it if you can

[Patrick Massot]

How would that look like in my example?