diff --git a/hott/init/types/sum.hlean b/hott/init/types/sum.hlean
new file mode 100644
index 0000000000..664a2b5e65
--- /dev/null
+++ b/hott/init/types/sum.hlean
@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura, Jeremy Avigad
+-/
+prelude
+import init.datatypes init.reserved_notation
+
+namespace sum
+  notation A ⊎ B := sum A B
+  notation A + B := sum A B
+  namespace low_precedence_plus
+    reserve infixr `+`:25  -- conflicts with notation for addition
+    infixr `+` := sum
+  end low_precedence_plus
+end sum