Enumerated implies Kurarowski-finite

FiniteSets/Sub.v

@@ -57,21 +57,19 @@ Section isIn.
 
 End isIn.
 
-Context `{Univalence}.
+Section intersect.
+  Variable A : Type.
+  Variable C : (Sub A) -> hProp.
+  Context `{Univalence}.
 
-Instance koe : forall (T : Type) (Ttrunc : IsHProp T), IsTrunc (-1) (T + ~T).
+  Instance hprop_lem : forall (T : Type) (Ttrunc : IsHProp T), IsHProp (T + ~T).
-Proof.
+  Proof.
     intros.
     apply (equiv_hprop_allpath _)^-1.
     intros [x | nx] [y | ny] ; try f_ap ; try (apply Ttrunc) ; try contradiction.
     - apply equiv_hprop_allpath. apply _.
-Defined.    
+  Defined.
 
-Section intersect.
-  Variable A : Type.
-  Variable C : (Sub A) -> hProp.
-
-  Context `{Univalence}.
   Context
     {HI :hasIntersection C} {HE : hasEmpty C}
     {HS : hasSingleton C} {HDE : hasDecidableEmpty C}.
@@ -82,7 +80,6 @@ Section intersect.
     unfold Decidable, hasEmpty, hasIntersection, hasSingleton, hasDecidableEmpty in *.
     pose (HI (singleton a) (singleton b) (HS a) (HS b)) as IntAB.
     pose (HDE (min_fun (singleton a) (singleton b)) IntAB) as IntE.
-    Print Trunc_rec.
     refine (@Trunc_rec _ _ _  _ _ IntE) ; intros [p | p] ; unfold min_fun, singleton in p.
     - right.
       pose (apD10 p b) as pb ; unfold empty_sub in pb ; cbn in pb.

FiniteSets/variations/enumerated.v

@@ -1,6 +1,8 @@
 (* Enumerated finite sets *)
-Require Import HoTT HoTT.Types.Bool.
+Require Import HoTT.
 Require Import disjunction.
+Require Import representations.cons_repr representations.definition variations.k_finite.
+From fsets Require Import operations isomorphism.
 
 Definition Sub A := A -> hProp.
 
@@ -73,9 +75,11 @@ induction ls as [| a ls].
     * apply IHls. apply HIH.
 Defined.
 
+(** Definition of finite sets in an enumerated sense *)
 Definition enumerated (A : Type) : Type :=
   exists ls, forall (a : A), listExt ls a.
 
+(** Properties of enumerated sets: closed under decidable subsets *)
 Lemma enumerated_comprehension (A : Type) (P : A -> Bool) :
   enumerated A -> enumerated { x : A | P x = true }.
 Proof.
@@ -96,6 +100,7 @@ induction ls.
   + right. apply IHls. apply HIH.
 Defined.
 
+(** Properties of enumerated sets: closed under surjections *)
 Lemma enumerated_surj (A B : Type) (f : A -> B) :
   IsSurjection f -> enumerated A -> enumerated B.
 Proof.
@@ -129,6 +134,7 @@ induction ls'; simpl.
   right. apply IHls'. apply Hls.
 Defined.
 
+(** Properties of enumerated sets: closed under sums *)
 Lemma enumerated_sum (A B : Type) :
   enumerated A -> enumerated B -> enumerated (A + B).
 Proof.
@@ -190,11 +196,46 @@ induction xs as [| x' xs]; intros x y.
       simpl. apply tr. right. assumption.
 Defined.      
 
+(** Properties of enumerated sets: closed under products *)
 Lemma enumerated_prod (A B : Type) `{Funext} :
   enumerated A -> enumerated B -> enumerated (A * B).
 Proof.
-intros [eA HeA] [eB HeB].
+  intros [eA HeA] [eB HeB].
-exists (listProd eA eB).
+  exists (listProd eA eB).
-intros [x y].
+  intros [x y].
-apply listExt_prod; [ apply HeA | apply HeB ].
+  apply listExt_prod; [ apply HeA | apply HeB ].
 Defined.
+
+(** If a set is enumerated is it Kuratowski-finite *)
+Section enumerated_fset.
+  Variable A : Type.
+  Context `{Univalence}.
+
+  Fixpoint list_to_fset (ls : list A) : FSet A :=
+    match ls with
+    | nil => ∅
+    | cons x xs => {|x|} ∪ (list_to_fset xs)
+    end.
+  
+  Lemma list_to_fset_ext (ls : list A) (a : A):
+    listExt ls a -> isIn a (list_to_fset ls).
+  Proof.
+    induction ls as [|x xs]; simpl.
+    - apply idmap.
+    - intros Hin.
+      strip_truncations. apply tr.
+      destruct Hin as [Hax | Hin].
+      + left. exact Hax.
+      + right. by apply IHxs.
+  Defined.
+
+  Lemma enumerated_Kf : enumerated A -> Kf A.
+  Proof.
+    intros [ls Hls].
+    exists (list_to_fset ls). 
+    apply path_forall. intro a.
+    symmetry. apply path_hprop.
+    apply if_hprop_then_equiv_Unit. apply _.
+    by apply list_to_fset_ext.
+  Defined.
+End enumerated_fset.

FiniteSets/variations/k_finite.v

@@ -3,7 +3,7 @@ Require Import lattice representations.definition fsets.operations extensionalit
 
 Section k_finite.
 
-  Context {A : Type}.
+  Context (A : Type).
   Context `{Univalence}.
 
   Definition map (X : FSet A) : Sub A := fun a => isIn a X.
@@ -33,8 +33,25 @@ Section k_finite.
 
   Definition Kf : hProp := Kf_sub (fun x => True).
 
-  Lemma Kf_unfold : Kf <-> (exists (X : FSet A), forall (a : A), map X a).
+  Instance: IsHProp {X : FSet A & forall a : A, map X a}.
   Proof.
+    apply hprop_allpath.
+    intros [X PX] [Y PY].
+    assert (X = Y) as HXY.
+    { apply fset_ext. intros a.
+      unfold map in *.
+      apply path_hprop.
+      apply equiv_iff_hprop; intros.
+      + apply PY.
+      + apply PX. }
+    apply path_sigma with HXY. simpl.
+    apply path_forall. intro.
+    apply path_ishprop.
+  Defined.
+
+  Lemma Kf_unfold : Kf <~> (exists (X : FSet A), forall (a : A), map X a).
+  Proof.
+    apply equiv_equiv_iff_hprop. apply _. apply _.
     split.
     - intros [X PX]. exists X. intro a.
       rewrite <- PX. done.
@@ -46,8 +63,10 @@ Section k_finite.
 
 End k_finite.
 
+Arguments map {_} {_} _.
+
 Section structure_k_finite.
-  Context {A : Type}.
+  Context (A : Type).
   Context `{Univalence}.
 
   Lemma map_union : forall X Y : FSet A, map (U X Y) = max_fun (map X) (map Y).
@@ -57,7 +76,7 @@ Section structure_k_finite.
     reflexivity.
   Defined.
 
-  Lemma k_finite_union : @hasUnion A Kf_sub.
+  Lemma k_finite_union : hasUnion (Kf_sub A).
   Proof.
     unfold hasUnion, Kf_sub, Kf_sub_intern.
     intros.
@@ -69,14 +88,14 @@ Section structure_k_finite.
     reflexivity.
   Defined.
 
-  Lemma k_finite_empty : @hasEmpty A Kf_sub.
+  Lemma k_finite_empty : hasEmpty (Kf_sub A).
   Proof.
     unfold hasEmpty, Kf_sub, Kf_sub_intern, map, empty_sub.
     exists E.
     reflexivity.
   Defined.
 
-  Lemma k_finite_singleton : @hasSingleton A Kf_sub.
+  Lemma k_finite_singleton : hasSingleton (Kf_sub A).
   Proof.
     unfold hasSingleton, Kf_sub, Kf_sub_intern, map, singleton.
     intro.
@@ -87,7 +106,7 @@ Section structure_k_finite.
     reflexivity.
   Defined.
 
-  Lemma k_finite_hasDecidableEmpty : @hasDecidableEmpty A Kf_sub.
+  Lemma k_finite_hasDecidableEmpty : hasDecidableEmpty (Kf_sub A).
   Proof.
     unfold hasDecidableEmpty, hasEmpty, Kf_sub, Kf_sub_intern, map.
     intros.