Hi Sebastian
Sebastian Hanowski wrote:
( f : Fin (suc m) -> Fin (suc n) !
let !-----------------------------------!
! restrict _m _n f : Fin m -> Fin n )
Should you be able to write a function with this type? I can certainly
write a function from Fin 2 to Fin 1, but I shouldn't be able to extract
a function from Fin 1 to Fin 0. Unless my initial function is injective,
of course.
I fear max-or-weak may not be terribly helpful here: my suspicion (not
having prepared a solution) is that viewing things as i or (thin i j)
might help. It might also be useful to try to write down a datatype
capturing concretely only the injective functions, even if you make no
use of it.
I think I'll have a play with this.
All the best
Conor
