(* do dalszej części potrzebne są reguły redukcji, stąd definicja indukcyjna *)
Inductive eq (A:Type) (a:A) : A -> Type := eq_refl : eq A a a.

(* tego nie da sie udowodnic dla indukcyjnego eq *)
Axiom eq_unique :  forall (A:Type) (a:A) (phi : eq A a a -> Type),
   phi (eq_refl A a) -> forall q:eq A a a, phi q.

Lemma eq_elim : forall (A:Type) (a:A) (phi:forall n, eq A a n -> Type),
   phi a (eq_refl A a) -> forall (b:A) (q: eq A a b), phi b q. 
exact eq_rect.
Defined.

Lemma eq_subst : forall (A:Type) (a:A) (phi : A -> Type),
   phi a -> forall b:A, eq A a b -> phi b.
intros A a phi X b H.
change ((fun b (_: eq A a b) => phi b) b H). 
apply eq_elim.
apply X.
Defined.


Inductive cell : Type := C : forall A:Type, A -> cell.

Definition pi1 (c:cell) := match c with C A _ => A end.
Definition pi2 (c:cell) := match c return (pi1 c) with C A a => a end.

Definition coercion : forall S T:Type, eq Type S T -> S -> T :=
  fun S T H s => eq_subst Type S (fun x => x) s T H.

Lemma sproj: forall Aa Bb : cell, eq cell Aa Bb -> forall e: eq Type (pi1 Aa) (pi1 Bb), 
eq (pi1 Bb) (coercion (pi1 Aa) (pi1 Bb) e (pi2 Aa)) (pi2 Bb).
intros Aa Bb X.
eapply eq_subst with (2:=X).
clear X Bb.
intro e.
eapply eq_unique with (q:=e).
unfold coercion.
unfold eq_subst.
simpl.
apply eq_refl.
Defined.

(* zeby to otypowac potrzebujemy zredukowac sproj, czyli eq_subst dla eq_refl *)
Definition wskazowka (A:Type)(a a':A)(e:eq cell (C A a) (C A a')) : eq A a a' := 
  sproj (C A a) (C A a') e (eq_refl Type A).

Definition JMeq : forall (A:Type), A -> forall (B:Type), B -> Type :=
  fun A a B b => eq cell (C A a) (C B b).

Definition JMeq_refl : forall (A:Type) (a:A), (JMeq A a A a) :=
  fun A a => eq_refl cell (C A a).

Lemma JMeq_elim : 
  forall (A:Type)(a:A)(phi : forall a', JMeq A a A a' -> Type),
  phi a (JMeq_refl A a) -> forall a' (l:JMeq A a A a'), phi a' l.
unfold JMeq_refl.
unfold JMeq.
intros.
generalize l.
pattern a'.
apply eq_subst with (2 := wskazowka _ _ _ l). (* (2:=sproj (C A a) (C A a') l (eq_refl Type A)); compute *)
intros.
apply eq_unique with (q:=l0).
apply X.
Qed.