diff --git a/src/Data/Maybe.ard b/src/Data/Maybe.ard
new file mode 100644
index 00000000..01287f65
--- /dev/null
+++ b/src/Data/Maybe.ard
@@ -0,0 +1,33 @@
+\import Logic
+\import Paths
+\import Set
+
+-- | Maybe A
+-- Maybe represents an optional value. It might also be used to represent failure.
+\data Maybe (A : \Type) | nothing | just A
+  \where {
+    \func bind {A B : \Type} (a : Maybe A)(f : A -> Maybe B) : Maybe B \elim a
+      | nothing => nothing
+      | just a => f a
+
+    \lemma justA/=nothing  {A : \Type} (a : A) (p : just a = nothing) : Empty =>
+      IsJust.absurd (transport IsJust p itIsJust)
+  }
+
+-- | IsJust is a proof that the value is actually a just
+\data IsJust {A : \Type} (m : Maybe A) : \Prop \with
+  | just _ => itIsJust
+  \where {
+    \func absurd {A B : \Type} (s : IsJust {A} nothing) : B
+
+    \lemma notNothing {A : \Type} (m : Maybe A) (ev : IsJust m) : Not (m = nothing) \elim m, ev
+      | just a, itIsJust => Maybe.justA/=nothing a
+  }
+
+\func isJust {A : \Type} (m : Maybe A) : \Type
+  | nothing => Empty
+  | just a => IsJust (just a)
+
+\func isItJust {A : \Type} (m : Maybe A) : Dec (IsJust m) \elim m
+  | nothing => no (IsJust.absurd {A} {Empty})
+  | just a => yes itIsJust