diff --git a/FiniteSets/Sub.v b/FiniteSets/Sub.v
index 8c99993..da92340 100644
--- a/FiniteSets/Sub.v
+++ b/FiniteSets/Sub.v
@@ -62,7 +62,7 @@ Section intersect.
   Variable C : (Sub A) -> hProp.
   Context `{Univalence}.
 
-  Instance hprop_lem : forall (T : Type) (Ttrunc : IsHProp T), IsHProp (T + ~T).
+  Global Instance hprop_lem : forall (T : Type) (Ttrunc : IsHProp T), IsHProp (T + ~T).
   Proof.
     intros.
     apply (equiv_hprop_allpath _)^-1.
diff --git a/FiniteSets/_CoqProject b/FiniteSets/_CoqProject
index b30ce1f..d7c3a24 100644
--- a/FiniteSets/_CoqProject
+++ b/FiniteSets/_CoqProject
@@ -17,6 +17,7 @@ fsets/length.v
 fsets/monad.v
 FSets.v
 Sub.v
+representations/T.v
 implementations/lists.v
 variations/enumerated.v
 variations/k_finite.v
diff --git a/FiniteSets/representations/T.v b/FiniteSets/representations/T.v
new file mode 100644
index 0000000..c27ebb2
--- /dev/null
+++ b/FiniteSets/representations/T.v
@@ -0,0 +1,332 @@
+(* Type which proves that all types have merely decidable equality implies LEM *)
+Require Import HoTT HitTactics Sub.
+
+Module Export T.
+  Section HIT.
+    Variable A : Type.
+
+    Private Inductive T (B : Type) : Type :=
+    | b : T B
+    | c : T B.    
+
+    Axiom p : A -> b A = c A.
+    Axiom setT : IsHSet (T A).
+
+  End HIT.
+
+  Arguments p {_} _.
+
+  Section T_induction.
+    Variable A : Type.
+    Variable (P : (T A) -> Type).
+    Variable (H : forall x, IsHSet (P x)).
+    Variable (bP : P (b A)).
+    Variable (cP : P (c A)).
+    Variable (pP : forall a : A, (p a) # bP = cP).
+    
+    (* Induction principle *)
+    Fixpoint T_ind
+             (x : T A)
+             {struct x}
+      : P x
+      := (match x return _ -> _ -> P x with
+          | b => fun _ _ => bP
+          | c => fun _ _ => cP                              
+          end) pP H.
+
+    Axiom T_ind_beta_p : forall (a : A),
+        apD T_ind (p a) = pP a.
+  End T_induction.
+
+  Section T_recursion.
+
+    Variable A : Type.
+    Variable P : Type.
+    Variable H : IsHSet P.
+    Variable bP : P.
+    Variable cP : P.
+    Variable pP : A -> bP = cP.
+
+    Definition T_rec : T A -> P.
+    Proof.
+      simple refine (T_ind A _ _ _ _ _) ; cbn.
+      - apply bP.
+      - apply cP.
+      - intro a.
+        simple refine ((transport_const _ _) @  (pP a)).
+    Defined.
+
+    Definition T_rec_beta_p : forall (a : A),
+        ap T_rec (p a) = pP a.
+    Proof.
+      intros.
+      unfold T_rec.
+      eapply (cancelL (transport_const (p a) _)).
+      simple refine ((apD_const _ _)^ @ _).
+      apply T_ind_beta_p.
+    Defined.
+  End T_recursion.
+
+  Instance T_recursion A : HitRecursion (T A)
+    := {indTy := _; recTy := _; 
+        H_inductor := T_ind A; H_recursor := T_rec A }.
+
+End T.
+
+Check T.
+
+Section merely_dec_lem.
+  Variable A : hProp.
+  Context `{Univalence}.
+
+  Definition code_b : T A -> hProp.
+  Proof.
+    hrecursion.
+    - apply Unit_hp.
+    - apply A.
+    - intro a.
+      apply path_iff_hprop.
+      * apply (fun _ => a).
+      * apply (fun _ => tt).
+  Defined.
+
+  Definition code_c : T A -> hProp.
+  Proof.
+    hrecursion.
+    - apply A.
+    - apply Unit_hp.
+    - intro a.
+      apply path_iff_hprop.
+      * apply (fun _ => tt).
+      * apply (fun _ => a).
+  Defined.
+
+  Definition code : T A -> T A -> hProp.
+  Proof.
+    simple refine (T_rec _ _ _ _ _ _).
+    - exact code_b.
+    - exact code_c.
+    - intro a.
+      apply path_forall.
+      intro z.
+      hinduction z.
+      * apply path_iff_hprop.
+        ** apply (fun _ => a).
+        ** apply (fun _ => tt).
+      * apply path_iff_hprop.
+        ** apply (fun _ => tt).
+        ** apply (fun _ => a).
+      * intros. apply set_path2.
+  Defined.
+
+  Local Ltac f_prop := apply path_forall ; intro ; apply path_ishprop.
+
+  Lemma transport_code_b_x (a : A) : 
+    transport code_b (p a) = fun _ => a.
+  Proof.
+    f_prop.
+  Defined.
+
+  Lemma transport_code_c_x (a : A) : 
+    transport code_c (p a) = fun _ => tt.
+  Proof.
+    f_prop.    
+  Defined.
+
+  Lemma transport_code_c_x_V (a : A) : 
+    transport code_c (p a)^ = fun _ => a.
+  Proof. 
+    f_prop.    
+  Defined.
+
+  Lemma transport_code_x_b (a : A) : 
+    transport (fun x => code x (b A)) (p a) = fun _ => a.
+  Proof.
+    f_prop.
+  Defined.
+
+  Lemma transport_code_x_c (a : A) : 
+    transport (fun x => code x (c A)) (p a) = fun _ => tt.
+  Proof.
+    f_prop.
+  Defined.
+
+  Lemma transport_code_x_c_V (a : A) : 
+    transport (fun x => code x (c A)) (p a)^ = fun _ => a.
+  Proof.
+    f_prop.
+  Defined.
+
+  Lemma ap_diag {B : Type} {x y : B} (p : x = y) :
+    ap (fun x : B => (x, x)) p = path_prod' p p.   
+  Proof.
+      by path_induction.
+  Defined.
+
+  Lemma transport_code_diag (a : A) z :
+    (transport (fun i : (T A) => code i i) (p a)) z = tt.
+  Proof.
+    apply path_ishprop.
+  Defined.
+
+  Definition r : forall (x : T A), code x x.
+  Proof.
+    simple refine (T_ind _ _ _ _ _ _); simpl.
+    - exact tt.
+    - exact tt.
+    - intro a.
+      apply transport_code_diag.
+  Defined.
+
+  Definition encode_pre : forall (x y : T A), x = y -> code x y
+    := fun x y p => transport (fun z => code x z) p (r x).
+
+  Definition encode : forall x y, x = y -> code x y.
+  Proof.
+    intros x y.
+    intro p.
+    refine (transport (fun z => code x z) p _). clear p.
+    revert x. simple refine (T_ind _ _ _ _ _ _); simpl.
+    - exact tt.
+    - exact tt.
+    - intro a.
+      apply path_ishprop.
+  Defined.
+
+  Definition decode_b : forall (y : T A), code_b y -> (b A) = y.
+  Proof.
+    simple refine (T_ind _ _ _ _ _ _) ; simpl.
+    - exact (fun _ => idpath).
+    - exact (fun a => p a).
+    - intro a.
+      apply path_forall.
+      intro t.
+      refine (transport_arrow _ _ _ @ _).
+      refine (transport_paths_FlFr _ _ @ _).
+      hott_simpl.
+      f_ap.
+      apply path_ishprop.
+  Defined.
+
+  Definition decode_c : forall (y : T A), code_c y -> (c A) = y.
+  Proof.
+    simple refine (T_ind _ _ _ _ _ _); simpl.
+    - exact (fun a => (p a)^).
+    - exact (fun _ => idpath).
+    - intro a.
+      apply path_forall.
+      intro t.
+      refine (transport_arrow _ _ _ @ _).
+      refine (transport_paths_FlFr _ _ @ _).
+      rewrite transport_code_c_x_V.
+      hott_simpl.      
+  Defined.
+
+  Lemma transport_paths_FlFr_trunc :
+    forall {X Y : Type} (f g : X -> Y) {x1 x2 : X} (q : x1 = x2)
+           (r : f x1 = g x1),
+      transport (fun x : X => Trunc 0 (f x = g x)) q (tr r) = tr (((ap f q)^ @ r) @ ap g q).
+  Proof.
+    destruct q; simpl. intro r.
+    refine (ap tr _).
+    exact ((concat_1p r)^ @ (concat_p1 (1 @ r))^).
+  Defined.
+  
+  Definition decode : forall (x y : T A), code x y -> x = y.
+  Proof.
+    simple refine (T_ind _ _ _ _ _ _); simpl.
+    - intro y. exact (decode_b y).
+    - intro y. exact (decode_c y).
+    - intro a.
+      apply path_forall. intro z.
+      rewrite transport_forall_constant.
+      apply path_forall. intros c.
+      rewrite transport_arrow.
+      hott_simpl.
+      rewrite (transport_paths_FlFr _ _).
+      revert z c. simple refine (T_ind _ _ _ _ _ _) ; simpl.
+      + intro.
+        hott_simpl.
+        f_ap.
+        refine (ap (fun x => (p x)) _).
+        apply path_ishprop.
+      + intro.        
+        rewrite transport_code_x_c_V.
+        hott_simpl.
+      + intro b.
+        apply path_forall.
+        intro z.
+        rewrite transport_forall.
+        apply set_path2.
+  Defined.
+
+  Lemma decode_encode (u v : T A) : forall (p : u = v),
+      decode u v (encode u v p) = p.
+  Proof.
+    intros p. induction p.
+    simpl. revert u. simple refine (T_ind _ _ _ _ _ _).
+    + simpl. reflexivity.
+    + simpl. reflexivity.    
+    + intro a.
+      apply set_path2.
+  Defined.
+
+  Lemma encode_decode : forall (u v : T A) (c : code u v),
+      encode u v (decode u v c) = c.
+  Proof.
+    simple refine (T_ind _ _ _ _ _ _).
+    - simple refine (T_ind _ _ _ _ _ _).
+      + simpl. apply path_ishprop.
+      + simpl. intro a. apply path_ishprop.
+      + intro a. apply path_forall; intros ?. apply set_path2.
+    - simple refine (T_ind _ _ _ _ _ _).
+      + simpl. intro a. apply path_ishprop. 
+      + simpl. apply path_ishprop. 
+      + intro a. apply path_forall; intros ?. apply set_path2.
+    - intro a. repeat (apply path_forall; intros ?). apply set_path2.
+  Defined.
+  
+
+  Instance T_hprop (a : A) : IsHProp (b A = c A).
+  Proof.
+    apply hprop_allpath.
+    intros x y.
+    pose (encode (b A) _ x) as t1.
+    pose (encode (b A) _ y) as t2.
+    assert (t1 = t2).
+    {
+      unfold t1, t2.
+      apply path_ishprop.
+    }
+    pose (decode _ _ t1) as t3.
+    pose (decode _ _ t2) as t4.
+    assert (t3 = t4) as H1.
+    {
+      unfold t3, t4.
+      f_ap.
+    }
+    unfold t3, t4, t1, t2 in H1.
+    rewrite ?decode_encode in H1.
+    apply H1.
+  Defined.
+  
+  Lemma equiv_pathspace_T : (b A = c A) = A.
+  Proof.
+    apply path_iff_ishprop.
+    - intro x.
+      apply (encode (b A) (c A) x).
+    - apply p.
+  Defined.
+
+End merely_dec_lem.
+
+Theorem merely_dec `{Univalence} : (forall (A : Type) (a b : A), hor (a = b) (~a = b))
+                                   ->
+                                   forall (A : hProp), A + (~A).
+Proof.
+  intros.
+  specialize (X (T A) (b A) (c A)).
+  rewrite (equiv_pathspace_T A) in X.
+  strip_truncations.
+  apply X.
+Defined.