Added some lemmata from paper

FiniteSets/kuratowski/length.v

@@ -290,4 +290,65 @@ Section length_sum.
     rewrite ?(length_fmap_inj _ _).
     reflexivity.
   Defined.
-End length_sum.
+End length_sum.
+
+Section length_zero_one.
+  Context {A : Type} `{Univalence} `{MerelyDecidablePaths A}.
+
+  Lemma Z_not_S n : S n = 0 -> Empty.
+  Proof.
+    refine (@equiv_path_nat (n.+1) 0)^-1.
+  Defined.
+
+  Lemma remove_S n m : S n = S m -> n = m.
+  Proof.
+    intros X.
+    enough (n.+1 =n m.+1) as X0.
+    {
+      simpl in X0.
+      apply (equiv_path_nat X0).
+    }
+    apply ((equiv_path_nat)^-1 X).
+  Defined.
+  
+  Theorem length_zero : forall (X : FSet A) (HX : length X = 0), X = ∅.
+  Proof.
+    simple refine (FSet_cons_ind (fun Z => _) _ _ _ _ _)
+    ; try (intros ; apply path_ishprop) ; simpl.
+    - reflexivity.
+    - intros a X HX HaX.
+      rewrite length_compute in HaX.
+      unfold member_dec, fset_member_bool in HaX.
+      destruct (dec (a ∈ X)).
+      * pose (HX HaX) as XE.
+        pose (transport (fun Z => a ∈ Z) XE t) as Nonsense.
+        contradiction Nonsense.        
+      * contradiction (Z_not_S _ HaX).
+  Defined.  
+
+  Theorem length_one : forall (X : FSet A) (HX : length X = 1), hexists (fun a => X = {|a|}).
+  Proof.
+    simple refine (FSet_cons_ind (fun Z => _) _ _ _ _ _)
+    ; try (intros ; apply path_ishprop) ; simpl.
+    - intros.
+      contradiction (Z_not_S _ (HX^)).
+    - intros a X HX HaX.
+      refine (tr(a;_)).
+      rewrite length_compute in HaX.
+      unfold member_dec, fset_member_bool in HaX.
+      destruct (dec (a ∈ X)).
+      * specialize (HX HaX).
+        strip_truncations.
+        destruct HX as [b HX].
+        assert (({|a|} : FSet A) = {|b|}) as p.
+        {
+          rewrite HX in t.
+          strip_truncations.
+          f_ap.
+        }
+        rewrite HX, p.
+        apply union_idem.
+      * rewrite (length_zero _ (remove_S _ _ HaX)).
+        apply nr.
+  Defined.
+End length_zero_one.

FiniteSets/kuratowski/properties.v

@@ -135,7 +135,7 @@ Section monad_fset.
     - exact {|tt|}.
   Defined.
 
-  Lemma FSet_Unit `{Funext} : FSet Unit <~> Unit + Unit.
+  Lemma FSet_Unit : FSet Unit <~> Unit + Unit.
   Proof.
     apply BuildEquiv with FSet_Unit_2.
     apply equiv_biinv_isequiv.
@@ -182,11 +182,13 @@ Section monad_fset.
       reflexivity.
     - intros [a | b]; simpl; rewrite !union_idem; reflexivity.
   Defined.
+  
   Definition fsum2 {A B : Type} : FSet A * FSet B -> FSet (A + B).
   Proof.
     intros [X Y].
     exact ((fset_fmap inl X) ∪ (fset_fmap inr Y)).
   Defined.
+  
   Lemma fsum1_inl {A B : Type} (X : FSet A) :
     fsum1 (fset_fmap inl X) = (X, ∅ : FSet B).
   Proof.
@@ -196,6 +198,7 @@ Section monad_fset.
     rewrite nl.
     reflexivity.
   Defined.
+  
   Lemma fsum1_inr {A B : Type} (Y : FSet B) :
     fsum1 (fset_fmap inr Y) = (∅ : FSet A, Y).
   Proof.
@@ -206,7 +209,7 @@ Section monad_fset.
     reflexivity.
   Defined.
   
-  Lemma FSet_sum `{Funext} {A B : Type}: FSet (A + B) <~> FSet A * FSet B.
+  Lemma FSet_sum {A B : Type}: FSet (A + B) <~> FSet A * FSet B.
   Proof.
     apply BuildEquiv with fsum1.
     apply equiv_biinv_isequiv.
@@ -581,6 +584,20 @@ Section properties_membership_decidable.
     apply comprehension_isIn_d.
   Defined.
 
+  Lemma intersection_isIn (X Y: FSet A) (a : A) :
+    a ∈ (X ∩ Y) = BuildhProp ((a ∈ X) * (a ∈ Y)).
+  Proof.
+    unfold intersection, fset_intersection.
+    rewrite comprehension_isIn.
+    unfold member_dec, fset_member_bool.
+    destruct (dec (a ∈ Y)) as [? | n].
+    - apply path_iff_hprop ; intros X0
+      ; try split ; try (destruct X0) ; try assumption.
+    - apply path_iff_hprop ; try contradiction.
+      intros [? p].
+      apply (n p).
+  Defined.
+
   Lemma difference_isIn_d (X Y: FSet A) (a : A) :
     a ∈_d (difference X Y) = andb (a ∈_d X) (negb (a ∈_d Y)).
   Proof.

FiniteSets/misc/dec_kuratowski.v

@@ -67,13 +67,16 @@ Section length.
 
   Variable (length : FSet A -> nat)
            (length_singleton : forall (a : A), length {|a|} = 1)
-           (length_one : forall (X : FSet A), length X = 1 -> {a : A & X = {|a|}}).
+           (length_one : forall (X : FSet A), length X = 1 -> hexists (fun a => X = {|a|})).
 
   Theorem dec_length (a b : A) : Decidable(merely(a = b)).
   Proof.
     destruct (dec (length ({|a|} ∪ {|b|}) = 1)).
-    - destruct (length_one _ p) as [c Xc].
-      refine (inl _).
+    - refine (inl _).
+      pose (length_one _ p) as Hp.
+      simple refine (Trunc_rec _ Hp).
+      clear Hp ; intro Hp.
+      destruct Hp as [c Xc].
       assert (merely(a = c) * merely(b = c)).
       { split.
         * pose (transport (fun z => a ∈ z) Xc) as t.