diff --git a/library/data/empty.lean b/library/data/empty.lean
index 817ace12a..e1fbcd9ad 100644
--- a/library/data/empty.lean
+++ b/library/data/empty.lean
@@ -16,3 +16,23 @@ namespace empty
   protected theorem subsingleton [instance] : subsingleton empty :=
   subsingleton.intro (λ a b, !elim a)
 end empty
+
+definition tneg.tneg (A : Type) := A → empty
+prefix `~` := tneg.tneg
+namespace tneg
+variables {A B : Type}
+protected definition intro (H : A → empty)        : ~A     := H
+protected definition elim  (H1 : ~A) (H2 : A)     : empty  := H1 H2
+protected definition empty                        : ~empty := λH : empty, H
+definition tabsurd         (H1 : A) (H2 : ~A)     : B      := !empty.elim (H2 H1)
+definition tneg_tneg_intro (H : A)                : ~~A    := λH2 : ~A, tneg.elim H2 H
+definition tmt             (H1 : A → B) (H2 : ~B) : ~A     := λHA : A, tabsurd (H1 HA) H2
+
+definition tneg_pi_left {B : A → Type} (H : ~Πa, B a) : ~~A :=
+λHnA : ~A, tneg.elim H (λHA : A, tabsurd HA HnA)
+
+definition tneg_function_right (H : ~(A → B)) : ~B :=
+λHB : B, tneg.elim H (λHA : A, HB)
+
+
+end tneg