Conor McBride wrote:
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.
Just for the record: I suggested to show:
f : Fin (suc m) -> Fin (suc n); Injective f
------------------------------------------------------------
restrict f : (f' : Fin m -> Fin n; Injective f')
in freely invented syntax.
T.
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
This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.
