diff --git a/code/Decidability/DiscreteTypes.v b/code/Decidability/DiscreteTypes.v
index 0a57721..c5c356d 100644
--- a/code/Decidability/DiscreteTypes.v
+++ b/code/Decidability/DiscreteTypes.v
@@ -141,57 +141,4 @@ Section ClosureProperties.
         * exact inr.
   Qed.
 
-  Definition nopathsnilcons {X : UU} (a : X) (l : list X) : ¬ (nil = (cons a l)). 
-  Proof.
-    intros eq.
-    set (P := (@list_ind X (λ _, UU) unit (λ _ _ _, empty))).
-    exact (@transportf (list X) P nil (cons a l) eq tt). 
-  Qed.
-
-  Definition nopathsconsnil {X : UU} (a : X) (l : list X) : ¬ ((cons a l) = nil).
-  Proof.
-    intros eq.
-    set (P := (@list_ind X (λ _, UU) empty (λ _ _ _, unit))).
-    exact (@transportf (list X) P (cons a l) nil eq tt). 
-  Qed.
-
-  Lemma isdeceqlist (X : UU) : (isdeceq X) → (isdeceq (list X)).
-  Proof.
-    intros isdx. 
-    use list_ind; cbv beta.
-    - use list_ind; cbv beta.
-      + left; apply idpath.
-      + intros. right. 
-        apply nopathsnilcons.
-    - intros x xs Ih.  
-      use list_ind; cbv beta.
-      + right. apply nopathsconsnil.
-      + intros x0 xs0 deceq. 
-        induction (Ih xs0), (isdx x x0).
-        * induction a, p.
-          left. apply idpath. 
-        * right. intros eq.
-          exact (n (cons_inj1 x x0 xs xs0 eq)).
-        * right. intros eq.
-          exact (b (cons_inj2 x x0 xs xs0 eq)).
-        * right. intros eq.
-          exact (b (cons_inj2 x x0 xs xs0 eq)).
-  Qed.
-
-  Lemma isdeceqoption (X : UU) : (isdeceq X) → (isdeceq (@option X)).
-  Proof.
-    intros isdx. 
-    intros o1 o2.
-    induction o1, o2.
-    - induction (isdx a x).
-      + induction a0. left. apply idpath. 
-      + right. intros eq. apply b, some_injectivity. exact eq.
-    - right. induction u. apply nopathssomenone.
-    - right; induction b. apply nopathsnonesome.
-    - left; induction u, b. apply idpath.
-  Qed.
-End ClosureProperties.
-
-Section ChoiceFunction.
-
-End ChoiceFunction.
+End ClosureProperties.
\ No newline at end of file
diff --git a/code/Inductive/ListProperties.v b/code/Inductive/ListProperties.v
new file mode 100644
index 0000000..ab70f51
--- /dev/null
+++ b/code/Inductive/ListProperties.v
@@ -0,0 +1,274 @@
+Require Import init.imports.
+Require Import UniMath.Combinatorics.Lists.
+
+Section Definitions.
+
+  Definition is_in {X : UU} (x : X) : (list X) → UU.
+  Proof.
+     use list_ind.
+     - exact empty.
+     - intros.
+       exact (X0 ⨿ (x = x0)). 
+  Defined.
+
+  Definition hin {X : UU} (x : X) : (list X) → hProp := (λ l : (list X), ∥is_in x l∥).
+
+  Section Tests.
+
+    Definition l : list nat := (cons 1 (cons 2 (cons 3 (nil)))).
+
+    Lemma test1In : (is_in 1 l).
+    Proof.
+      right; apply idpath.
+    Qed.
+
+    Lemma negtest4In : ¬ (is_in 4 (cons 1 nil)).  
+    Proof.
+      intros [a | b].
+      - exact a.
+      - apply (negpathssx0 2).
+        apply invmaponpathsS.
+        exact b.
+    Qed.    
+  End Tests.
+  
+End Definitions.
+
+Section Length.
+  (*Lemmas related to the length of the list*)
+  
+  Lemma length_zero_nil {X : UU} (l : list X) (eq : 0 = length l) : l = nil.   
+  Proof.
+    revert l eq.
+    use list_ind. 
+    - exact (λ x, (idpath nil)).
+    - intros x xs Ih eq.
+      apply fromempty.
+      apply (negpaths0sx (length xs) eq).
+  Qed.
+
+  Lemma length_cons {X : UU} (l : list X) (inq : 0 < length l) : ∑ (x0 : X) (l2 : list X), l = (cons x0 l2). 
+    revert l inq.
+    use list_ind.
+    - intros inq.
+      exact (fromempty (isirreflnatlth 0 inq)).
+    - intros x xs Ih ineq.
+      exact (x,, (xs,, (idpath (cons x xs)))).
+  Qed.
+
+  Lemma length_in {X : UU} (l : list X) (x : X) (inn : is_in x l) : 0 < length l.
+  Proof.
+    revert l inn.
+    use list_ind.
+    - intros inn. apply fromempty. exact inn.
+    - cbv beta. intros.
+      apply idpath.
+  Qed.
+  
+End Length.
+
+
+Section DistinctList.
+
+  Definition distinctterms {X : UU} : (list X) → UU.
+  Proof.
+    use list_ind.
+    - exact unit.
+    - intros.
+      exact (X0 × ¬(is_in x xs)).
+  Defined.
+
+  Definition hdistinct {X : UU} : (list X) → hProp := (λ l : (list X), ∥distinctterms l∥).
+  
+End DistinctList.
+
+Section Filter.
+
+  Definition filter_ex_fun {X : UU} (d : isdeceq X) (x : X) : X → list X → list X.
+  Proof.
+    intros x0 l1.
+    induction (d x x0).
+    - exact l1.
+    - exact (cons x0 l1).
+  Defined.
+  
+  Definition filter_ex {X : UU} (d : isdeceq X) (x : X) (l : list X) : list X :=
+    (@foldr X (list X) (filter_ex_fun d x) nil l).
+
+  Definition filter_ex_nil {X : UU} (d : isdeceq X) (x : X) (l : list X) : (filter_ex d x nil) = nil.
+  Proof.
+    apply idpath.
+  Qed.
+  
+  
+  Definition filter_ex_cons1 {X : UU} (d : isdeceq X) (x : X) (l : list X) : (filter_ex d x (cons x l)) = (filter_ex d x l).
+  Proof.
+    set (q:= foldr_cons (filter_ex_fun d x) nil x l).
+    unfold filter_ex; induction (pathsinv0 q).
+    unfold filter_ex_fun; induction (d x x).
+    - apply idpath.
+    - apply fromempty, b, idpath.
+  Defined.
+
+  Definition filter_ex_cons2 {X : UU} (d : isdeceq X) (x x0 : X) (l : list X) (nin : ¬ (x = x0)) : (filter_ex d x (cons x0 l)) = cons x0 (filter_ex d x l).
+  Proof.
+    set (q := foldr_cons (filter_ex_fun d x) nil x0 l).
+    unfold filter_ex; induction (pathsinv0 q).
+    unfold filter_ex_fun; induction (d x x0).
+    - apply fromempty, nin, a.
+    - apply idpath.
+  Defined.
+
+  Lemma xninfilter_ex {X : UU} (d : isdeceq X) (x : X) (l : list X) : ¬ is_in x (filter_ex d x l).
+  Proof.
+    revert l.
+    use list_ind.
+    - intros is_in.
+      exact is_in.
+    - cbv beta.
+      intros x0 xs Ih.
+      induction (d x x0).
+      + induction a. induction (pathsinv0 (filter_ex_cons1 d x xs)). exact Ih.
+      + induction (pathsinv0 (filter_ex_cons2 d x x0 xs b)). intros [lst | elm].
+        * exact (Ih lst).
+        * exact (b elm).
+  Defined.
+  
+  Lemma filter_exltlist1 {X : UU} (d : isdeceq X) (x : X) (l : list X) : (length (filter_ex d x l)) ≤ (length l).
+  Proof.
+    revert l.
+    use list_ind.
+    - use isreflnatleh.
+    - cbv beta. intros x0 xs Ih.
+      induction (d x x0).
+      + induction a.
+        induction (pathsinv0 (filter_ex_cons1 d x xs)).
+        apply natlehtolehs; exact Ih.
+      + induction (pathsinv0 (filter_ex_cons2 d x x0 xs b)).
+        exact Ih.
+  Qed.
+
+  Lemma istransnatlth {n m k : nat} : n < m → (m < k) → (n < k). 
+  Proof.
+    intros inq1 inq2.
+    apply (istransnatgth k m n).
+    - exact inq2.
+    - exact inq1.
+  Qed.
+  
+  Lemma natlthnsnmtonm {n m : nat} : (S n < m) → (n < m). 
+  Proof.
+    intros.
+    exact (istransnatlth (natlthnsn n) X). 
+  Qed.
+  
+  Lemma filter_exltlist2 {X : UU} (d : isdeceq X) (x : X) (l : list X) (inn : is_in x l) : (length (filter_ex d x l)) < (length l). 
+  Proof.
+    revert l inn.
+    use list_ind; cbv beta.
+    - intros. apply fromempty. exact inn.
+    - intros x0 xs Ih inn.
+      destruct inn as [in' | elm].
+      + set (q := (Ih in')).
+        induction (d x x0).
+        * induction a. induction (pathsinv0 (filter_ex_cons1 d x xs)).
+          apply natlthtolths. exact q.
+        * induction (pathsinv0 (filter_ex_cons2 d x x0 xs b)).
+          exact q.
+      + induction (pathsinv0 elm).
+        set (ineq := (filter_exltlist1 d x0 xs)).
+        induction (pathsinv0 (filter_ex_cons1 d x0 xs)).
+        apply natlehtolthsn.
+        exact ineq.
+  Qed.
+
+  Lemma filter_ex_in {X : UU} (d : isdeceq X) (l : list X) (x x0 : X) (neq : ¬ (x = x0)) : (is_in x0 l) → (is_in x0 (filter_ex d x l)).
+  Proof.
+    revert l.
+    use list_ind; cbv beta.
+    - intros nn. apply fromempty. exact nn.
+    - intros.
+      induction (d x x1).
+      + induction a. induction (pathsinv0 (filter_ex_cons1 d x xs)).
+        destruct X1 as [a | b].
+        * exact (X0 a).
+        * apply fromempty, neq. exact (pathsinv0 b).
+      + induction (pathsinv0 (filter_ex_cons2 d x x1 xs b)).
+        destruct X1 as [a | c].
+        * left.
+          exact (X0 a).
+        * induction (pathsinv0 c).
+          right. apply idpath.
+  Qed.
+  
+End Filter.
+
+
+
+Section Properties.
+
+  Lemma eqdecidertomembdecider {X : UU} (d : ∏ (x1 x2 : X), decidable(x1=x2)) : ∏ (x : X) (l : list X), decidable (is_in x l). 
+  Proof.
+    intros x.
+    use list_ind.
+    - right; intros inn. exact inn.
+    - intros x0 xs dec.
+      induction dec.
+      + left; left. exact a.
+      + induction (d x x0).
+        * left; right. exact a.
+        * right. intros [a | a'].
+          -- apply b. exact a.
+          -- apply b0. exact a'.
+  Defined.
+
+  (* An induction principle for lists with distinct terms. *)
+  Lemma distinct_list_induction {X : UU} : ∏ (P : list X → UU),
+  (P nil) → (∏ (x : X) (xs : (list X)) (d : (distinctterms xs)), (P xs) → ¬(is_in x xs) → (P (cons x xs))) → ∏ (xs : list X) (d : distinctterms xs), (P xs). 
+  Proof.
+    intros P Pnil Ih.
+    use list_ind.
+    - exact (λ d : _, Pnil).
+    - intros x xs X0 d.
+      destruct d as [d inn].
+      apply Ih.
+      + exact d.
+      + exact (X0 d).
+      + exact inn.
+  Defined.        
+  
+  Lemma pigeonhole_sigma {X : UU} (l1 l2 : list X) (d : ∏ (x1 x2 : X), (decidable (x1=x2))) (dist : distinctterms l2) : (length l1) < (length l2) → (∑ (x : X), (is_in x l2) × (¬ (is_in x l1))). 
+  Proof.
+    revert l2 dist l1.
+    use distinct_list_induction.
+    - intros l1 ineq.
+      apply fromempty.
+      exact (negnatlthn0 (length l1) ineq).
+    - cbn beta; intros x xs dt Ih nin.
+      intros l1 ineq.
+      induction (eqdecidertomembdecider d x l1).
+      + set (l' := filter_ex d x l1).
+        assert (length l' < length xs).
+        * apply (natlthlehtrans (length l') (length l1) (length xs)).
+          -- exact (filter_exltlist2 d x l1 a).
+          -- apply natlthsntoleh. exact ineq.
+        * set (pr := (Ih l' X0)).
+          destruct pr as [x0 [ixs il']].
+          use tpair.
+          -- exact x0.
+          -- split.
+             left.
+             ++ exact ixs.
+             ++ intros il1.
+                apply il', filter_ex_in.
+                ** intros eq.
+                   induction eq.
+                   exact (nin ixs).
+                ** exact il1.
+      + use tpair.
+        * exact x.
+        * split.
+          -- right. apply idpath.
+          -- exact b.
+  Qed.  
+End Properties.
diff --git a/code/Inductive/Option.v b/code/Inductive/Option.v
index 34dfe38..a659ca6 100644
--- a/code/Inductive/Option.v
+++ b/code/Inductive/Option.v
@@ -1,3 +1,5 @@
+
+(* Definition of an option as the coproduct of a type X with the unit type *)
 Require Import init.imports. 
 
 Section Option.
@@ -28,4 +30,3 @@ Section PathProperties.
   
   
 End PathProperties.
-
diff --git a/code/Reducibility/ManyOneReductions.v b/code/Reducibility/ManyOneReductions.v
new file mode 100644
index 0000000..df3fa8e
--- /dev/null
+++ b/code/Reducibility/ManyOneReductions.v
@@ -0,0 +1,211 @@
+Require Import init.imports.
+Require Import Decidability.DecidablePredicates.
+
+  
+Section ManyOneReducibility.
+
+Definition ismanyonereduction {X Y : UU} (p : X → hProp) (q : Y → hProp) (f : X → Y) := ∏ (x : X), p x <-> q (f x).
+
+Definition reduction {X Y : UU} (p : X → hProp) (q : Y → hProp) := ∑ (f : X → Y), ismanyonereduction p q f.
+
+Definition make_reduction {X Y : UU} (p : X → hProp) (q : Y → hProp) (f : X → Y) (isrct : ismanyonereduction p q f) : (reduction p q) := (f,, isrct).
+
+Definition ismanyonereducible {X Y : UU} (p : X → hProp) (q : Y → hProp) := ∥reduction p q∥.
+
+Notation "p ≼ q" := (ismanyonereducible p q) (at level 500).
+
+Lemma isapropismanyonereduction {X Y : UU} (p : X → hProp) (q : Y → hProp) (f : X → Y) : (isaprop (ismanyonereduction p q f)).
+Proof.
+  apply impred_isaprop; intros.
+  apply isapropdirprod; apply isapropimpl; apply propproperty.
+Qed.
+
+Lemma reductiontodecidability {X Y : UU} (p : X → hProp) (q : Y → hProp) : (p ≼ q) → (deptypeddecider q) → (deptypeddecider p).
+Proof.
+  intros rct dep1.
+  use squash_to_prop.
+  - exact (reduction p q).
+  - exact rct.
+  - apply isapropdeptypeddecider.
+  - intros [f isrct] x.
+    destruct (isrct x) as [impl1 impl2].
+    induction (dep1 (f x)).
+    + left. exact (impl2 a).
+    + right. intros px. apply b. exact (impl1 px).
+Qed.
+
+Lemma isreductionidfun {X : UU} (p : X → hProp) : (ismanyonereduction p p (idfun X)).
+Proof.
+  intros x; split; apply idfun.
+Qed.
+
+(* Many one reducibility is a preorder. *)
+
+Lemma reductionrefl {X : UU} (p : X → hProp) : reduction p p.
+Proof.
+  use make_reduction.
+  - exact (idfun X).
+  - exact (isreductionidfun p).
+Qed.
+
+Lemma reductioncomp {X Y Z : UU} (p : X → hProp) (q : Y → hProp) (r : Z → hProp) : (reduction p q) → (reduction q r) → (reduction p r).
+Proof.
+  intros [f rf] [g rg].
+  use make_reduction.
+  - exact (λ x : X, (g (f x))).
+  - intros x; destruct (rf x) as [rf1 rf2]; destruct (rg (f x)) as [rg1 rg2]; split; intros pp.
+    + exact (rg1 (rf1 pp)).
+    + exact (rf2 (rg2 pp)).
+Qed.
+
+Lemma isreduciblerefl {X : UU} (p : X → hProp) : (p ≼ p).
+Proof.
+  apply hinhpr.
+  apply reductionrefl.
+Qed.
+
+Lemma isreduciblecomp {X Y Z : UU} (p : X → hProp) (q : Y → hProp) (r : Z → hProp) : (p ≼ q) → (q ≼ r) → (p ≼ r).
+Proof.
+  apply hinhfun2.
+  apply reductioncomp.
+Qed.
+
+(* Many one reducibility forms an upper semi-lattice *)
+
+Definition coprod_pred {X Y : UU} (p : X → hProp) (q : Y → hProp) : (X ⨿ Y) → hProp.
+Proof.
+  intros [a | b].
+  - exact (p a).
+  - exact (q b).
+Defined.
+
+Notation "p + q" := (coprod_pred p q).
+
+Lemma isreduction_ii1 {X Y : UU} (p : X → hProp) (q : Y → hProp) : (ismanyonereduction p (p + q) ii1).
+Proof.
+intros x.
+split; apply idfun.
+Defined.
+
+Lemma isreduction_ii2 {X Y : UU} (p : X → hProp) (q : Y → hProp) : (ismanyonereduction q (p + q) ii2).
+Proof.
+  intros x.
+  split; apply idfun.
+Defined.
+
+Lemma reduction_coprod1 {X Y : UU} (p : X → hProp) (q : Y → hProp) : (reduction p (p+q)).
+Proof.
+  use make_reduction.
+  - apply ii1.
+  - apply isreduction_ii1.
+Defined.
+
+Lemma reduction_coprod2 {X Y : UU} (p : X → hProp) (q : Y → hProp) : (reduction q (p + q)).
+Proof.
+  use make_reduction.
+  - apply ii2.
+  - apply isreduction_ii2.
+Defined.
+
+Lemma isreducible_coprod1 {X Y : UU} (p : X → hProp) (q : Y → hProp) : (p ≼ (p + q)).
+Proof.
+  apply hinhpr.
+  apply reduction_coprod1.
+Qed.
+
+Lemma isreducible_coprod2 {X Y : UU} (p : X → hProp) (q : Y → hProp) : (q ≼ (p + q)).
+Proof.
+  apply hinhpr.
+  apply reduction_coprod2.
+Qed.
+
+Lemma isreduction_sumofmaps {X Y Z : UU} (p : X → hProp) (q : Y → hProp) (r : Z → hProp) (f : X → Z) (g : Y → Z) : (ismanyonereduction p r f) → (ismanyonereduction q r g) → (ismanyonereduction (p + q) r (sumofmaps f g)).
+Proof.
+  intros isf isg x.
+  induction x.
+  - exact (isf a).
+  - exact (isg b).
+Qed.
+
+Lemma reduction_coprod {X Y Z : UU} (p : X → hProp) (q : Y → hProp) (r : Z → hProp) : (reduction p r) → (reduction q r) → (reduction (p + q) r).
+Proof.
+  intros [f irf] [g irg].
+  use make_reduction.
+  - exact (sumofmaps f g).
+  - exact (isreduction_sumofmaps p q r f g irf irg).
+Defined.
+
+Lemma isreducible_coprod {X Y Z : UU} (p : X → hProp) (q : Y → hProp) (r : Z → hProp) : (p ≼ r) → (q≼ r) → ((p + q) ≼ r).
+Proof.
+  apply hinhfun2, reduction_coprod.
+Qed.
+
+Definition predcompl {X : UU} (p : X → hProp) : X → hProp := (λ x : X, (hneg (p x))).
+
+(* If a predicate is reducible to a predicate q, then its complement is reducible to the complement of q *)
+
+Lemma isreductioncompl {X Y : UU} (p : X → hProp) (q : Y → hProp) (f : X → Y) : (ismanyonereduction p q f) → (ismanyonereduction (predcompl p) (predcompl q) f).
+Proof.
+  intros isr x.
+  destruct (isr x) as [isr1 isr2].
+  split.
+  - intros npx qfx.
+    exact (npx (isr2 qfx)).
+  - intros nqfx px.
+    exact (nqfx (isr1 px)).
+Defined.
+
+Lemma reductioncompl {X Y : UU} (p : X → hProp) (q : Y → hProp) : (reduction p q) → (reduction (predcompl p) (predcompl q)).
+Proof.
+  intros rect.
+  exact (make_reduction (predcompl p) (predcompl q) (pr1 rect) (isreductioncompl p q (pr1 rect) (pr2 rect))).
+Defined.
+
+Lemma isreduciblecompl {X Y : UU} (p : X → hProp) (q : Y → hProp) : (p ≼ q) → ((predcompl p) ≼ (predcompl q)).
+Proof.
+  intros rdct.
+  use squash_to_prop.
+  - exact (reduction p q).
+  - exact rdct.
+  - apply propproperty.
+  - intros rect.
+    apply hinhpr.
+    apply reductioncompl.
+    exact rect.
+Qed.
+
+Definition lem := ∏ (P : UU), (isaprop P) → P ⨿ ¬P.
+
+Definition isstable {X : UU} (p : X → hProp) := ∏ (x : X), (hneg (hneg (p x))) → (p x).
+
+Lemma isapropisstable {X : UU} (p : X → hProp) : (isaprop (isstable p)).
+Proof.
+  apply impred_isaprop.
+  intros t; apply isapropimpl.
+  apply propproperty.
+Qed.
+
+Lemma fundneg {X Y : UU} (f : X → Y) : (¬¬ X) → (¬¬ Y).
+Proof.
+  intros nnx ny.
+  apply nnx.
+  intros x.
+  exact (ny (f x)).
+Qed.
+
+Lemma isreduciblestable {X Y : UU} (p : X → hProp) (q : Y → hProp) : (isstable q) → (p ≼ q) → (isstable p).
+Proof.
+  intros.
+  use squash_to_prop.
+  - exact (reduction p q).
+  - exact X1.
+  - apply isapropisstable.
+  - intros [f isr] x; destruct (isr x) as [isr1 isr2].
+    simpl.
+    intros nnpx.
+    set (nf := fundneg isr1).
+    apply isr2, (X0 (f x)).
+    exact (nf nnpx).
+Qed.
+
+End ManyOneReducibility.
diff --git a/code/_CoqProject b/code/_CoqProject
index 9e8e692..7b30385 100644
--- a/code/_CoqProject
+++ b/code/_CoqProject
@@ -2,12 +2,17 @@ COQC = coqc
 COQDEP = coqdep
 -R . "sem"
 
--o -arg "-w -notation-overridden -type-in-type"
+
+-arg "-w -notation-overridden -type-in-type -noinit"
 
 init/imports.v
 init/all.v
 
+
+Inductive/ListProperties.v
 Inductive/Option.v
 
 Decidability/DecidablePredicates.v
-Decidability/DiscreteTypes.v
\ No newline at end of file
+Decidability/DiscreteTypes.v
+
+Reducibility/ManyOneReductions.v