diff --git a/README.md b/README.md
new file mode 100644
index 0000000000000000000000000000000000000000..1847735101d40d1086c10a7566de9cd69d3f00ee
--- /dev/null
+++ b/README.md
@@ -0,0 +1,4 @@
+parseque - Total Parser Combinators in Coq
+==========================================
+
+This is a port of [agdarsec](https://github.com/gallais/agdarsec) to Coq.
diff --git a/src/Indexed.v b/src/Indexed.v
new file mode 100644
index 0000000000000000000000000000000000000000..d5b3d5958124a4bbe53e5428c322e61b9a49dab9
--- /dev/null
+++ b/src/Indexed.v
@@ -0,0 +1,36 @@
+Section Indexed.
+
+Local Open Scope type.
+
+Variable (I : Type).
+Variable (T : Type).
+Variable (A B : I -> Type).
+
+Definition IArrow : I -> Type :=
+  fun i => A i -> B i.
+
+Definition ISum : I -> Type :=
+  fun i => A i + B i.
+
+Definition IProduct : I -> Type :=
+  fun i => A i * B i.
+
+Definition IConstant : I -> Type :=
+  fun i => T.
+
+Definition IForall : Type :=
+  forall {i}, A i.
+
+End Indexed.
+
+Arguments IArrow    {_}.
+Arguments ISum      {_}.
+Arguments IProduct  {_}.
+Arguments IConstant {_}.
+Arguments IForall   {_}.
+
+Notation "A :-> B" := (IArrow A B)   (at level 20, right associativity).
+Notation "A :+  B" := (ISum A B)     (at level 30).
+Notation "A :*  B" := (IProduct A B) (at level 40).
+Notation ":K A"    := (IConstant A)  (at level 50).
+Notation "[ A ]"   := (IForall A)    (at level 70).
\ No newline at end of file
diff --git a/src/Induction.v b/src/Induction.v
new file mode 100644
index 0000000000000000000000000000000000000000..6c12658685fb74ac1ad222b91d9062334bf8b78f
--- /dev/null
+++ b/src/Induction.v
@@ -0,0 +1,55 @@
+Require Import Indexed.
+Require Import Coq.Arith.Lt.
+Require Import Coq.Arith.Le.
+Require Import PeanoNat.
+
+
+Record Box (A : nat -> Type) (n : nat) : Type :=
+  MkBox { call : forall m, m < n -> A m }.
+
+Arguments call {_} {_} _ {_}.
+Arguments MkBox {_} {_}.
+
+Section Induction.
+
+Variables (A B C : nat -> Type).
+
+Definition map (f : [ A :-> B ]) : [ Box A :-> Box B ] :=
+  fun _ b => MkBox (fun _ mltn => f _ (call b mltn)).
+
+Definition map2 (f : [ A :-> B :-> C ]) : [ Box A :-> Box B :-> Box C ] :=
+ fun _ a b => MkBox (fun m mltn => f _ (call a mltn) (call b mltn)).
+
+Definition app : [ Box (A :-> B) :-> Box A :-> Box B ] :=
+  fun _ f a => MkBox (fun m mltn => call f mltn (call a mltn)).
+
+Definition extract (v : [ Box A ]) : [ A ] :=
+  fun _ => call (v _) (le_n _).
+
+Definition duplicate : [ Box A :-> Box (Box A) ] :=
+  fun n v => MkBox (fun m mltn =>
+             MkBox (fun p pltm =>
+  let mltp := lt_trans _ _ _ pltm mltn
+  in call v mltp)).
+
+Definition FixBox (alg : [ Box A :-> A ]) : [ Box A ] :=
+fix rec n := match n with
+ | O    => MkBox (fun m mltO => False_rect _ (Nat.nlt_0_r _ mltO))
+ | S n' => MkBox (fun m mltn => alg _
+          (MkBox (fun p pltm =>
+             let mltn' := lt_le_trans _ _ _ pltm (le_S_n _ _ mltn)
+             in call (rec n') mltn')))
+end.
+
+Definition Fix (alg : [ Box A :-> A ]) : [ A ] := extract (FixBox alg).
+
+End Induction.
+
+Arguments map {_} {_}.
+Arguments map2 {_} {_} {_}.
+Arguments app {_} {_}.
+Arguments extract {_}.
+Arguments duplicate {_}.
+
+Definition Loeb A : [ Box (Box A :-> A) :-> Box A ] :=
+  Fix _ (fun _ r alg => app _ alg (app _ r (duplicate _ alg))).
diff --git a/src/_CoqProject b/src/_CoqProject
new file mode 100644
index 0000000000000000000000000000000000000000..62467e11012d9bd2e8fdee70034607d6cdf19c3f
--- /dev/null
+++ b/src/_CoqProject
@@ -0,0 +1,2 @@
+-I.
+-R.