Prove that a function's result cannot dependent on Prop-valued parameters in Coq

Question

Consider the following function elem and the lemma that the result of elem does not depend on the proof of l <> nil.

Program Definition elem {A: Type} (l: list A) (nn: l <> nil): A :=
  match l with
    | nil => _
    | (a::_) => a
  end.

Lemma elem_proof_irrelevant: forall A (l: list A) nn1 nn2, elem l nn1 = elem l nn2.
Proof.
  intros. destruct l; [congruence | now unfold elem].
Qed.

My understanding of universes is very limited, but I believe that, in Coq, you cannot define something in Set whose value depends on something in Prop. At least, I believe that the result of elem cannot depend on nn for universe-related reasons.

So is there a more general way to prove elem_proof_irrelevant - i.e. that elem only depends on its first parameter - that does not inspect elem and would work on arbitrary functions, without assuming proof_irrelevance or other axioms?

Answer 1

Short answer: no. More precisely, if you assume that any function from a proposition to a type does not depend on its arguments, then you can prove proof irrelevance:

Axiom fun_irrel : forall (P : Prop) (A : Type) (f : P -> A) (p q : P), f p = f q.

Lemma proof_irrel (P : Prop) (p q : P) : p = q.
Proof.
  apply (fun_irrel P P (fun x => x)). (* uses cumulativity Prop <= Type *)
Qed.

(* Let's start again, without using cumulativity this time *)

Inductive Box (P : Prop) : Type := | box : P -> Box P.

Arguments box {_} _.

Definition unbox {P} : Box P -> P := fun b => match b with box p => p end.

Lemma proof_irrel' (P : Prop) (p q : P) : p = q.
Proof.
  assert (box p = box q) as e by apply fun_irrel.
  change (unbox (box p) = unbox (box q)).
  now rewrite e.
Qed.

And conversely, proof irrelevance entails fun_irrel. Obviously, just like you can prove proof irrelevance for certain propositions, you can prove instances of fun_irrel for specific functions, as in your case. But it will not, in general, be possible.