diff --git a/README.md b/README.md
new file mode 100644
index 0000000..a81366a
--- /dev/null
+++ b/README.md
@@ -0,0 +1 @@
+brew install coq
\ No newline at end of file
diff --git a/apt.txt b/apt.txt
new file mode 100644
index 0000000..4894c99
--- /dev/null
+++ b/apt.txt
@@ -0,0 +1 @@
+coqide
diff --git a/demo.ipynb b/demo.ipynb
new file mode 100644
index 0000000..d284a08
--- /dev/null
+++ b/demo.ipynb
@@ -0,0 +1,158 @@
+{
+ "cells": [
+  {
+   "cell_type": "code",
+   "execution_count": 1,
+   "metadata": {
+    "coq_kernel_metadata": {
+     "auto_roll_back": true,
+     "cell_id": "bf77268208bf49758fc7ddc1b4a205ab",
+     "evaluated": true,
+     "execution_id": "0337dd6b408e4eaa8f74445f51ab0298",
+     "rolled_back": false
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/html": [
+       "\n",
+       "<div class=\"coq_kernel_output_area\">\n",
+       "    <pre>Proving: implication\n",
+       "\n",
+       "1 subgoal\n",
+       "\n",
+       "1/1 -----------\n",
+       "forall A B : Prop, A -> (A -> B) -> B</pre>\n",
+       "</div>\n",
+       "\n",
+       "<div class=\"coq_kernel_rich_cell_output coq_kernel_status_message_area\" style=\"padding: 5px 0px;\">\n",
+       "    <i class=\"fa-check fa text-success\"></i>\n",
+       "    <span>Cell evaluated.</span>\n",
+       "</div>\n",
+       "\n",
+       "<div class=\"coq_kernel_rich_cell_output coq_kernel_status_message_area coq_kernel_rolled_back_status_message\" style=\"padding: 5px 0px; display: none;\">\n",
+       "    <i class=\"fa-exclamation-circle fa text-info\"></i>\n",
+       "    <span>Cell rolled back.</span>\n",
+       "</div>\n",
+       "\n",
+       "<div class=\"coq_kernel_rich_cell_output coq_kernel_roll_back_controls_area\" style=\"display: none; position: relative;\">\n",
+       "    <button class=\"btn btn-default btn-xs coq_kernel_roll_back_button\" onclick=\"CoqKernel.roll_back(this)\">\n",
+       "        <i class=\"fa-step-backward fa\"></i>\n",
+       "        <span class=\"toolbar-btn-label\">Rollback cell</span>\n",
+       "    </button>\n",
+       "\n",
+       "    <div style=\"display: inline-block; vertical-align: middle; padding-left: 0; padding-right: 0;\">\n",
+       "      <input class=\"coq_kernel_auto_roll_back_checkbox\" type=\"checkbox\" value=\"\" onchange=\"CoqKernel.toggle_auto_roll_back(this)\" checked>\n",
+       "      <label\">Auto rollback</label>\n",
+       "    </div>\n",
+       "</div>\n"
+      ],
+      "text/plain": [
+       "Proving: implication\n",
+       "\n",
+       "1 subgoal\n",
+       "\n",
+       "1/1 -----------\n",
+       "forall A B : Prop, A -> (A -> B) -> B"
+      ]
+     },
+     "execution_count": 2,
+     "metadata": {
+      "coq_kernel_evaluated": true,
+      "coq_kernel_execution_id": "0337dd6b408e4eaa8f74445f51ab0298",
+      "coq_kernel_rolled_back": false
+     },
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "Theorem implication :\n",
+    "  forall A B : Prop,\n",
+    "  A ->\n",
+    "  (A -> B) ->\n",
+    "  B\n",
+    "."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 2,
+   "metadata": {
+    "coq_kernel_metadata": {
+     "auto_roll_back": true,
+     "cell_id": "c28e58c60e7d437f8cbe75a62672519a",
+     "evaluated": true,
+     "execution_id": "5926e563d0b24d3ea30e1f490d0d8460",
+     "rolled_back": false
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/html": [
+       "\n",
+       "<div class=\"coq_kernel_output_area\">\n",
+       "    <pre></pre>\n",
+       "</div>\n",
+       "\n",
+       "<div class=\"coq_kernel_rich_cell_output coq_kernel_status_message_area\" style=\"padding: 5px 0px;\">\n",
+       "    <i class=\"fa-check fa text-success\"></i>\n",
+       "    <span>Cell evaluated.</span>\n",
+       "</div>\n",
+       "\n",
+       "<div class=\"coq_kernel_rich_cell_output coq_kernel_status_message_area coq_kernel_rolled_back_status_message\" style=\"padding: 5px 0px; display: none;\">\n",
+       "    <i class=\"fa-exclamation-circle fa text-info\"></i>\n",
+       "    <span>Cell rolled back.</span>\n",
+       "</div>\n",
+       "\n",
+       "<div class=\"coq_kernel_rich_cell_output coq_kernel_roll_back_controls_area\" style=\"display: none; position: relative;\">\n",
+       "    <button class=\"btn btn-default btn-xs coq_kernel_roll_back_button\" onclick=\"CoqKernel.roll_back(this)\">\n",
+       "        <i class=\"fa-step-backward fa\"></i>\n",
+       "        <span class=\"toolbar-btn-label\">Rollback cell</span>\n",
+       "    </button>\n",
+       "\n",
+       "    <div style=\"display: inline-block; vertical-align: middle; padding-left: 0; padding-right: 0;\">\n",
+       "      <input class=\"coq_kernel_auto_roll_back_checkbox\" type=\"checkbox\" value=\"\" onchange=\"CoqKernel.toggle_auto_roll_back(this)\" checked>\n",
+       "      <label\">Auto rollback</label>\n",
+       "    </div>\n",
+       "</div>\n"
+      ],
+      "text/plain": []
+     },
+     "execution_count": 9,
+     "metadata": {
+      "coq_kernel_evaluated": true,
+      "coq_kernel_execution_id": "5926e563d0b24d3ea30e1f490d0d8460",
+      "coq_kernel_rolled_back": false
+     },
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "Proof.\n",
+    "  intros A B.\n",
+    "  intros proof_of_A.\n",
+    "  intros A_implies_B.\n",
+    "  pose (proof_of_B := A_implies_B proof_of_A).\n",
+    "  exact proof_of_B.\n",
+    "Qed."
+   ]
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "Coq",
+   "language": "coq",
+   "name": "coq"
+  },
+  "language_info": {
+   "file_extension": ".v",
+   "mimetype": "text/x-coq",
+   "name": "coq",
+   "version": "8.6"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}
diff --git a/postBuild b/postBuild
new file mode 100755
index 0000000..8251d84
--- /dev/null
+++ b/postBuild
@@ -0,0 +1,2 @@
+pip install --user coq_jupyter==1.5.0
+python -m coq_jupyter.install