I think w/o proof irrelevance of equality in the type of the first argument, you will not be able to prove that the second projection is a "function" ...

Unfortunately, equality on the type Set is not provably irrelevant.