transport_fst_and_refl_implies_j.v

Set Universe Polymorphism.

Axiom Path : forall (A : Type), A -> A -> Type.
Axiom refl : forall {A x}, Path A x x.
Axiom transport : forall {A x y} (p : Path A x y),
  forall (P : A -> Type), P x -> P y.

Axiom transport_refl : forall {A x y} (p : Path A x y),
  transport p (fun z => Path A x z) refl = p.
Axiom transport_fst : forall {A x y} (p : Path A x y),
  forall L (R : forall x, L x -> Type) s,
  projT1 (transport p (fun z => {x : L z & R z x}) s) =
    transport p L (projT1 s).
Lemma Weak_J {A x y} (p : Path A x y) :
  forall (P : forall z, Path A x z -> Type),
    P x refl -> {p : Path A x y & P y p}.
  intros P r.
  apply (transport p).
  exact (existT _ refl r).
Defined.
Lemma J {A x y} (p : Path A x y) :
  forall (P : forall z, Path A x z -> Type),
    P x refl -> P y p.
  intros P r.
  assert (projT1 (Weak_J p P r) = p).
  unfold Weak_J.
  rewrite transport_fst.
  apply transport_refl.
  destruct H.
  exact (projT2 (Weak_J p P r)).
Defined.