Admissibility of strong projections

proj.v

(*
  Prove that, due to the free theorem for impredicative sigma types, strong
  projection is a valid extension. Based on Dan Doel's Agda version:
    https://hub.darcs.net/dolio/agda-share/browse/ParamInduction.agda.
*)

Definition Rel (A: Prop) (B: Prop) :=
  A -> B -> Prop.

Definition Sigma (T: Prop) (U: T -> Prop): Prop :=
  forall Y: Prop, (forall t: T, U t -> Y) -> Y.

Notation "'∑' '(' a : A ')' . b" := (Sigma A (fun a => b))
  (at level 200, a ident, right associativity,
   format "'∑' '(' a :  A ')' . b").

Definition Pair (T: Prop) (U: T -> Prop) (t: T) (u: U t): Sigma T U :=
  fun _ f =>
    f t u.

Notation "'(' a , b ')'" := (Pair _ _ a b).

Axiom free:
  forall {A: Prop} {P: A -> Prop} (C D: Prop),
  forall R1: Rel A A,
  forall R2: (forall x0 x1, R1 x0 x1 -> Rel (P x0) (P x1)),
  forall R3: Rel C D,
  forall p: Sigma A P,
  forall k0: (forall x: A, P x -> C),
  forall k1: (forall x: A, P x -> D),
  (forall x0 x1, forall r: R1 x0 x1,
   forall w0: P x0, forall w1: P x1,
   R2 x0 x1 r w0 w1 -> R3 (k0 x0 w0) (k1 x1 w1)) ->
  R3 (p C k0) (p D k1).

Lemma l0:
  forall {A P},
  forall p: Sigma A P,
  p (Sigma A P) (Pair A P) = p.
Proof.
  intros.
  eapply free with (R1 := eq).
  exact p.
  intros.
  exact p.
  intros.
  exact p.
  intros.
  eapply H.
Qed.

Lemma l1:
  forall {A P},
  forall p: Sigma A P,
  Sigma A (fun x => Sigma (P x) (fun w => p = Pair A P x w)).
Proof.
  intros.
  destruct (l0 p).
  eapply free with (R1 := eq).
  exact p.
  intros.
  exact p.
  intros.
  exact p.
  intros.
  eapply H.
Qed.

Lemma uncurry:
  forall {A P},
  forall (C: Sigma A P -> Prop),
  forall f: (forall x: A, forall w: P x, C (x, w)),
  forall p: Sigma A P,
  C p.
Proof.
  intros.
  eapply (l1 p).
  intros.
  eapply H.
  intros.
  destruct (eq_sym H0).
  apply f.
Qed.

Theorem pi1:
  forall {A P},
  Sigma A P -> A.
Proof.
  intros.
  eapply H.
  intros.
  exact t.
Defined.

Theorem pi2:
  forall {A P},
  forall p: Sigma A P,
  P (pi1 p).
Proof.
  intros.
  eapply uncurry with (C := fun q => P (pi1 q)).
  intros.
  exact w.
Defined.