1. T : Type2. T ~ T ⟶ 𝔹⊢ False{ RepeatFor 2 (D (-1)) }1. T : Type2. f : T ⟶ T ⟶ 𝔹3. Inj(T;T ⟶ 𝔹;f)4. Surj(T;T ⟶ 𝔹;f)⊢ False