Show that Kf (A + B) -> Kf A

FiniteSets/kuratowski/properties.v

@@ -63,6 +63,28 @@ Section monad_fset.
       + left. by apply HX0.
       + right. by apply HX1.
   Defined.
+
+  Lemma bind_isIn `{Univalence} {A : Type} (X : FSet (FSet A)) (a : A) :
+    (exists x, x ∈ X * a ∈ x) -> a ∈ (bind _ X).
+  Proof.
+    hinduction X;
+      try (intros; apply path_forall; intro; apply path_ishprop).
+    - simpl. intros [x [[] ?]].
+    - intros x [y [Hx Hy]].
+      strip_truncations.
+      rewrite <- Hx.
+      apply Hy.
+    - intros x x' IHx IHx'.
+      intros [z [Hz Ha]].
+      strip_truncations.
+      apply tr.
+      destruct Hz as [Hz | Hz]; [ left | right ].
+      + apply IHx.
+        exists z. split; assumption.
+      + apply IHx'.
+        exists z. split; assumption.
+  Defined.
+
 End monad_fset.
 
 (** Lemmas relating operations to the membership predicate *)

FiniteSets/subobjects/k_finite.v

@@ -1,5 +1,5 @@
 Require Import HoTT HitTactics.
-Require Import sub lattice_interface lattice_examples FSets.
+Require Import sub lattice_interface monad_interface lattice_examples FSets.
 
 Section k_finite.
 
@@ -171,6 +171,23 @@ Section k_properties.
     + apply (HY b).
   Defined.
 
+  Lemma Kf_sum_inv {A B : Type} : Kf (A + B) -> Kf A.
+  Proof.
+    intros HAB. kf_unfold.
+    destruct HAB as [X HX].
+    pose (f := fun z => match (z : A + B) with
+                     | inl a => ({|a|} : FSet A)
+                     | inr b => ∅
+                     end).
+    exists (bind _ (fset_fmap f X)).
+    intro a.
+    apply bind_isIn.
+    specialize (HX (inl a)).
+    exists {|a|}. split; [ | apply tr; reflexivity ].
+    apply (fmap_isIn f (inl a) X).
+    apply HX.
+  Defined.
+
   Lemma Kf_subterm (A : hProp) : Decidable A <~> Kf A.
   Proof.
     apply equiv_iff_hprop.