I was trying something that was a little complicated and couldn't get it to go through. I asked someone and they suggested it might not be possible to define such a function because -> isn't injective?

```
Inductive Foo (g : Type -> Type) : Type -> Type :=
foo : forall a b, (g a -> g b) -> Foo g (a -> b).
Definition run {a b g} (f : Foo g (a -> b)) : g a -> g b :=
match f with
| foo _ _ _ f' => f'
end.
```

Indeed `Foo g T`

is equivalent to `{ a & { b & ((g a -> g b) * (T = (a -> b))) } }`

(in case that's easier to read, if it was in Prop that would be `exists (a b : Type) (_ : g a -> g b), T = (a -> b)`

)

Last updated: Jan 28 2023 at 05:02 UTC