Is it possible to prove the following theorem without axioms in Coq? Or is the following theorem equivalent to any well known axioms?
Theorem eq_dep_app: forall input (output1 output2: input -> Type) f1 f2,
eq_dep Type id (forall i, output1 i) f1 (forall i, output2 i) f2 ->
forall i, eq_dep Type id (output1 i) (f1 i) (output2 i) (f2 i).
I tried the following:
intros.
apply eq_dep_eq_sigT in H.
apply eq_sigT_eq_dep.
set (s1:= existT id (forall i : input, output1 i) f1) in *.
set (s2:= existT id (forall i : input, output2 i) f2) in *.
change f1 with (projT2 s1).
change f2 with (projT2 s2).
rewrite H.
However, the last rewrite tactic fails:
Abstracting over the term "s1" leads to a term
fun s0 : {x : Type & id x} =>
existT id (output1 i) (projT2 s0 i) = existT id (output2 i) (projT2 s2 i)
which is ill-typed.
Reason is: Illegal application (Non-functional construction):
The expression "projT2" of type
"forall (A : Type) (P : A -> Type) (x : {x : A & P x}), P (projT1 x)"
cannot be applied to the terms
"Type" : "Type"
"id" : "Type -> Type"
"s0" : "{x : Type & id x}"
"i" : "input"
I interpret the error message as meaning that as part of rewriting projT2 s1 i
(used to be f1 i
) to projT2 s2 i
(used to be f2 i
), the rewrite tactic has to generalize s1
along with its type. As part of generalizing s1
's type, it forgets that projT2 s1
is a function, which causes projT2 s1 i
to no longer type check.
I know that the rewrite would work if I could replace all of the goal's references to f1
and output1
with something projected from s1
, but I can't figure out a way to replace the references to output1
.