# Eqdep_dec_Type

This extends Eqdep_dec to work on predicates over Type

```Require Export Eqdep_dec.
Definition K_dec_Type :=
fun A : Type =>
let comp :=
fun (x y y' : A) (eq1 : x = y) (eq2 : x = y') =>
eq_ind x (fun a : A => a = y') eq2 y eq1 in
fun (eq_dec : forall x y : A, x = y \/ x <> y) (x : A) =>
let nu :=
fun (y : A) (u : x = y) =>
match eq_dec x y with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y) (neqxy u)
end in
let nu_constant :=
fun (y : A) (u v : x = y) =>
match
eq_dec x y as o
return
(match o with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y) (neqxy u)
end =
match o with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y) (neqxy v)
end)
with
| or_introl e => refl_equal e
| or_intror n =>
match
n u as f return (False_ind (x = y) f = False_ind (x = y) (n v))
with
end
end in
let nu_inv :=
fun (y : A) (v : x = y) => comp x x y (nu x (refl_equal x)) v in
fun (P : x = x -> Type) (H : P (refl_equal x)) (p : x = x) =>
eq_rect (refl_equal x) (fun p0 : x = x => P p0) H p
(eq_proofs_unicity eq_dec (refl_equal x) p).
Definition K_dec_set_Type :=
fun (A : Set) (H : forall x y : A, {x = y} + {x <> y}) (x : A)
(P : x = x -> Type) (H0 : P (refl_equal x)) (p : x = x) =>
eq_rect_r P
(K_dec_Type _
(fun x0 y : A =>
match H x0 y with
| left e =>
eq_ind x0 (fun y0 : A => x0 = y0 \/ x0 <> y0)
(or_introl (x0 <> x0) (refl_equal x0)) y e
| right n =>
or_intror (x0 = y)
(fun neq : x0 = y =>
n (eq_ind x0 (fun y0 : A => x0 = y0) (refl_equal x0) y neq))
end) _ (fun e : x = x => P (eqT2eq e)) H0 (eq2eqT p)) (eq_eqT_bij p).
Lemma inj_right_pair2 :
forall A : Set,
(forall x y : A, {x = y} + {x <> y}) ->
forall (x : A) (P : A -> Set) (y y' : P x),
existS P x y = existS P x y' -> y = y'.
Proof.
intros.
set
(Proj :=
fun (e : sigS P) (def : P x) =>
match e with
| existS x' dep =>
match H x' x with
| left eqdep => eq_rec x' P dep x eqdep
| _ => def
end
end) in *.
cut (Proj (existS P x y) y = Proj (existS P x y') y).
simpl in |- *.
induction (H x x).
intro e.
set
(B :=
K_dec_set H
(fun z : x = x =>
eq_rec x P y x z = eq_rec x P y' x z ->
eq_rec x P y x (refl_equal x) = eq_rec x P y' x (refl_equal x))
(fun z : eq_rec x P y x (refl_equal x) = eq_rec x P y' x (refl_equal x) =>
z) a e) in *.
apply B.
elim b.
auto.
rewrite H0.
reflexivity.
Qed.```
##### Clone this wiki locally
You can’t perform that action at this time.
Press h to open a hovercard with more details.