diff --git a/libs/contrib/Data/Graph.idr b/libs/contrib/Data/Graph.idr
new file mode 100644
index 000000000..14c75e147
--- /dev/null
+++ b/libs/contrib/Data/Graph.idr
@@ -0,0 +1,8 @@
+module Data.Graph
+
+import Data.Vect
+
+data Edge e = MkEdge e e
+
+data Graph : Nat −> Nat −> Type −> Type −> Type where
+  MkGraph : Vect m v −> Vect n (Edge k) −> Graph m n v k
diff --git a/libs/contrib/Data/Polyhedra.idr b/libs/contrib/Data/Polyhedra.idr
new file mode 100644
index 000000000..8e8e9003b
--- /dev/null
+++ b/libs/contrib/Data/Polyhedra.idr
@@ -0,0 +1,9 @@
+module Data.Polyhedra
+
+import Data.Vect
+import Data.Graph
+
+data Face f = MkFace (Vect n f)
+
+data Polyhedron : Nat -> Nat -> Nat -> Type -> Type where
+  MkPolyhedron : Vect k v -> Vect m (Edge v) -> Vect n (Face v) -> Polyhedron k m n v