HInv?

Stream: new members

[Ben Selfridge]

Is there a heterogeneous inverse type? I expected to find HInv along with HPow, but I could not find one.

[Yakov Pechersky]

How would that work, given that inv is a unary function? What would be heterogenous about it?

[Aaron Liu]

Takes an α, returns a β

[Yakov Pechersky]

And the return type would be inferred from the context? I think even for HFoo binary functions, the return type is usually constrained by the two input types.

[Ben Selfridge]

Ah, that makes sense. I figured if it didn't exist, there would have to be a reason.

[Ben Selfridge]

It could work if there were a way to encode functional dependencies or open type families in Lean, but I'm not sure if there is.

[Yakov Pechersky]

Functional dependencies is approximated by outParam

[Yakov Pechersky]

but then you might as well have a plain Inv X and then Coe X Y

[Ben Selfridge]

Oh, maybe I will try that then. I just want nice notation for the inverse of an isomorphism.

[Ben Selfridge]

(with an isomorphism type i'm custom defining for my own purposes)

[Eric Wieser]

That's a nice example where a Coe wouldn't work

[Ben Selfridge]

Why wouldn't that work?