include "basics/logic.ma". axiom streicherK : ∀T:Type[1].∀t:T.∀P:t = t → Type[2]. P (refl ? t) → ∀p.P p. definition R2 : ∀T0:Type[0]. ∀a0:T0. ∀T1:∀x0:T0. a0=x0 → Type[0]. ∀a1:T1 a0 (refl ? a0). ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0]. ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1). ∀b0:T0. ∀e0:a0 = b0. ∀b1: T1 b0 e0. ∀e1:R1 ?? T1 a1 ? e0 = b1. T2 b0 e0 b1 e1. #T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1; @(eq_rect_Type0 ????? e1); @(R1 ?? ? ?? e0); @a2; qed. definition R3 : ∀T0:Type[0]. ∀a0:T0. ∀T1:∀x0:T0. a0=x0 → Type[0]. ∀a1:T1 a0 (refl ? a0). ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0]. ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1). ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1. ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0]. ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2). ∀b0:T0. ∀e0:a0 = b0. ∀b1: T1 b0 e0. ∀e1:R1 ?? T1 a1 ? e0 = b1. ∀b2: T2 b0 e0 b1 e1. ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2. T3 b0 e0 b1 e1 b2 e2. #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2; @(eq_rect_Type0 ????? e2); @(R2 ?? ? ???? e0 ? e1); @a3; qed. definition R4 : ∀T0:Type[0]. ∀a0:T0. ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0]. ∀a1:T1 a0 (refl T0 a0). ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0]. ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1). ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1. ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0]. ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1) a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2). ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1. ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2. ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3. Type[0]. ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1) a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2) a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1) a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)) a3). ∀b0:T0. ∀e0:eq (T0 …) a0 b0. ∀b1: T1 b0 e0. ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1. ∀b2: T2 b0 e0 b1 e1. ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2. ∀b3: T3 b0 e0 b1 e1 b2 e2. ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3. T4 b0 e0 b1 e1 b2 e2 b3 e3. #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3; @ (eq_rect_Type0 ????? e3); @ (R3 ????????? e0 ? e1 ? e2); @ a4; qed.