ndefinition i2d : ∀a,b.∀x,y:I2 a b.
∀e1:a = a.∀e2:R1 T1 a (λz,p.T2 z) b a e1 = b.
∀e: R2 T1 a (λz,p.T2 z) b (λz1,p1,z2,p2.I2 z1 z2) x a e1 b e2 = y.Type[2] ≝
ndefinition i2d : ∀a,b.∀x,y:I2 a b.
∀e1:a = a.∀e2:R1 T1 a (λz,p.T2 z) b a e1 = b.
∀e: R2 T1 a (λz,p.T2 z) b (λz1,p1,z2,p2.I2 z1 z2) x a e1 b e2 = y.Type[2] ≝