From 90d795b70853a84005e61e3ecb8e2ad3ade2c92b Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Thu, 3 Aug 2017 23:21:43 +0200
Subject: [PATCH] Correspondence between enumerated subobjects and k-finite
 subobjects

---
 FiniteSets/fsets/isomorphism.v     | 15 +++++--
 FiniteSets/variations/enumerated.v | 63 +++++++++++++++++++++++++++++-
 FiniteSets/variations/k_finite.v   |  2 +-
 3 files changed, 75 insertions(+), 5 deletions(-)

diff --git a/FiniteSets/fsets/isomorphism.v b/FiniteSets/fsets/isomorphism.v
index e72fa58..ae2394f 100644
--- a/FiniteSets/fsets/isomorphism.v
+++ b/FiniteSets/fsets/isomorphism.v
@@ -54,10 +54,8 @@ Section Iso.
     - intros a x HR. rewrite HR. reflexivity.
   Defined.
 
-
-  Theorem repr_iso: FSet A <~> FSetC A.
+  Global Instance: IsEquiv FSet_to_FSetC.
   Proof.
-    simple refine (@BuildEquiv (FSet A) (FSetC A) FSet_to_FSetC _ ).
     apply isequiv_biinv.
     unfold BiInv. split.
     exists FSetC_to_FSet.
@@ -66,6 +64,17 @@ Section Iso.
     unfold Sect. apply repr_iso_id_r.
   Defined.
 
+  Global Instance: IsEquiv FSetC_to_FSet.
+  Proof.
+    change (IsEquiv (FSet_to_FSetC)^-1).
+    apply isequiv_inverse.
+  Defined.
+
+  Theorem repr_iso: FSet A <~> FSetC A.
+  Proof.
+    simple refine (@BuildEquiv (FSet A) (FSetC A) FSet_to_FSetC _ ).
+  Defined.
+
   Theorem fset_fsetc : FSet A = FSetC A.
   Proof.
     apply (equiv_path _ _)^-1.
diff --git a/FiniteSets/variations/enumerated.v b/FiniteSets/variations/enumerated.v
index 24a3f46..e3e72a3 100644
--- a/FiniteSets/variations/enumerated.v
+++ b/FiniteSets/variations/enumerated.v
@@ -239,7 +239,7 @@ Section enumerated_fset.
     intros Hls.
     strip_truncations.
     destruct Hls as [ls Hls].
-    exists (list_to_fset ls). 
+    exists (list_to_fset ls).
     apply path_forall. intro a.
     symmetry. apply path_hprop.
     apply if_hprop_then_equiv_Unit. apply _.
@@ -398,4 +398,65 @@ Section subobjects.
     - intros. apply path_ishprop.
   Defined.
   Transparent enumeratedS.
+
+  Instance hprop_sub_fset (P : Sub A) :
+    IsHProp {X : FSet A & k_finite.map X = P}.
+  Proof.
+    apply hprop_allpath. intros [X HX] [Y HY].
+    assert (X = Y) as HXY.
+    { apply (isinj_embedding k_finite.map). apply _.
+      apply (HX @ HY^). }
+    apply path_sigma with HXY.
+    apply set_path2.
+  Defined.
+
+  Fixpoint list_weaken_to_fset (P : Sub A) (ls : list (sigT P)) : FSet A :=
+    match ls with
+    | nil => ∅
+    | cons x xs => {|x.1|} ∪ (list_weaken_to_fset P xs)
+    end.
+
+  Lemma list_weaken_to_fset_ext (P : Sub A) (ls : list (sigT P)) (a : A) (Ha : P a):
+    listExt ls (a;Ha) -> isIn a (list_weaken_to_fset P ls).
+  Proof.
+    induction ls as [|[x Hx] xs]; simpl.
+    - apply idmap.
+    - intros Hin.
+      strip_truncations. apply tr.
+      destruct Hin as [Hax | Hin].
+      + left.
+        strip_truncations. apply tr.
+        exact (Hax..1).
+      + right. by apply IHxs.
+  Defined.
+
+  Lemma list_weaken_to_fset_in_sub (P : Sub A) (ls : list (sigT P)) (a : A) :
+    a ∈ (list_weaken_to_fset P ls) -> P a.
+  Proof.
+    induction ls as [|[x Hx] xs]; simpl.
+    - apply Empty_rec.
+    - intros Ha.
+      strip_truncations.
+      destruct Ha as [Hax | Hin].
+      + strip_truncations.
+        by rewrite Hax.
+      + by apply IHxs.
+  Defined.
+
+  Definition enumeratedS_to_FSet :
+    forall (P : Sub A), enumeratedS P ->
+    {X : FSet A & k_finite.map X = P}.
+  Proof.
+    intros P HP.
+    strip_truncations.
+    destruct HP as [ls Hls].
+    exists (list_weaken_to_fset _ ls).
+    apply path_forall. intro a.
+    symmetry. apply path_iff_hprop.
+    - intros Ha.
+      apply list_weaken_to_fset_ext with Ha.
+      apply Hls.
+    - unfold k_finite.map.
+      apply list_weaken_to_fset_in_sub.
+  Defined.
 End subobjects.
diff --git a/FiniteSets/variations/k_finite.v b/FiniteSets/variations/k_finite.v
index 982aba6..a0cf674 100644
--- a/FiniteSets/variations/k_finite.v
+++ b/FiniteSets/variations/k_finite.v
@@ -8,7 +8,7 @@ Section k_finite.
 
   Definition map (X : FSet A) : Sub A := fun a => isIn a X.
 
-  Instance map_injective : IsEmbedding map.
+  Global Instance map_injective : IsEmbedding map.
   Proof.
     apply isembedding_isinj_hset. (* We use the fact that both [FSet A] and [Sub A] are hSets *)
     intros X Y HXY.