K-finite objects are closed under surjections

FiniteSets/fsets/monad.v

@@ -1,6 +1,6 @@
 (* [FSet] is a (strong and stable) finite powerset monad *)
 Require Import HoTT HitTactics.
-Require Export representations.definition fsets.properties.
+Require Export representations.definition fsets.properties fsets.operations.
 
 Definition ffmap {A B : Type} : (A -> B) -> FSet A -> FSet B.
 Proof.
@@ -68,3 +68,17 @@ Defined.
 Lemma join_fmap_return_1 {A : Type} (X : FSet A) :
   join (ffmap (fun x => {|x|}) X) = X.
 Proof. refine ((join_return_fmap _)^ @ join_return_1 _). Defined.
+
+Lemma fmap_isIn `{Univalence} {A B : Type} (f : A -> B) (a : A) (X : FSet A) :
+  a ∈ X -> (f a) ∈ (ffmap f X).
+Proof.
+  hinduction X; try (intros; apply path_ishprop).
+  - apply idmap.
+  - intros b Hab; strip_truncations.
+    apply (tr (ap f Hab)).
+  - intros X0 X1 HX0 HX1 Ha.
+    strip_truncations. apply tr.
+    destruct Ha as [Ha | Ha].
+    + left. by apply HX0.
+    + right. by apply HX1.
+Defined.

FiniteSets/variations/k_finite.v

@@ -1,5 +1,5 @@
 Require Import HoTT HitTactics.
-Require Import lattice representations.definition fsets.operations extensionality Sub fsets.properties.
+Require Import lattice representations.definition fsets.operations extensionality Sub fsets.properties fsets.monad.
 
 Section k_finite.
 
@@ -116,3 +116,21 @@ Section structure_k_finite.
     - apply (tr (inr H1)).
   Defined.
 End structure_k_finite.
+
+Section k_properties.
+  Context `{Univalence}.
+
+  Lemma Kf_surjection {X Y : Type} (f : X -> Y) `{IsSurjection f} :
+    Kf X -> Kf Y.
+  Proof.
+    intros HX. apply Kf_unfold. apply Kf_unfold in HX.
+    destruct HX as [Xf HXf].
+    exists (ffmap f Xf).
+    intro y.
+    pose (x' := center (merely (hfiber f y))).
+    simple refine (@Trunc_rec (-1) (hfiber f y) _ _ _ x'). clear x'; intro x.
+    destruct x as [x Hfx]. rewrite <- Hfx.
+    apply fmap_isIn.
+    apply (HXf x).
+  Defined.
+End k_properties.