# For functions that are eq_dep equal, are their applications eq_dep equal without axioms?

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.

• Can you please include enough context that your code compiles? For example, what are you importing? Mar 18 at 11:32
• I would guess that it requires some sort of function extensionality. But I can't be sure without further info.
– Trebor
Mar 18 at 13:16

Assuming you're using EqDepFacts (https://coq.inria.fr/library/Coq.Logic.EqdepFacts.html).

You can prove some form of injectivity of of pi-types for propositional equality from your proposition.

From Coq Require Import EqdepFacts Utf8.

Theorem eq_dep_app :
∀ input (output1 output2 : input → Type) f1 f2,
eq_dep Type (λ x, x) (∀ i, output1 i) f1 (∀ i, output2 i) f2 →
∀ i, eq_dep Type (λ x, x) (output1 i) (f1 i) (output2 i) (f2 i).

Corollary foo :
@eq Type (nat → nat) (nat → bool) →
@eq Type nat bool.
Proof.
intro e.
pose (f := λ x : nat, x).
pose (g := @eq_rect Type (nat → nat) (λ x : Type, x) f (nat → bool) e).
assert (e' : eq_dep Type (λ x, x) (nat → bool) g (nat → nat) f).
{ apply eq_dep1_dep. exists e. reflexivity. }
apply eq_dep_app with (i := 0) in e'.
apply eq_dep_dep1 in e'.
destruct e'.
assumption.
Qed.


The cardinal model of type theory validates (nat → nat) = (nat → bool) but not nat = bool so your proposition is not provable.

• In the cardinal model your corollary is simply false, right? If so it is definitely not provable, and so the theorem also is. Mar 18 at 15:50
• Indeed, this is what I meant. Maybe I should say it more strongly. Mar 18 at 16:20