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

Question

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.

Answer 1

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).
Admitted.

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.