From 617451da28ce547071554c5df71bd80c410b147d Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Sun, 24 Sep 2017 23:35:45 +0200
Subject: [PATCH] Some closure properties for K-finite objects

---
 FiniteSets/kuratowski/operations.v |  2 +-
 FiniteSets/subobjects/k_finite.v   | 76 +++++++++++++++++++++++++++++-
 2 files changed, 76 insertions(+), 2 deletions(-)

diff --git a/FiniteSets/kuratowski/operations.v b/FiniteSets/kuratowski/operations.v
index 7361e29..7474b6b 100644
--- a/FiniteSets/kuratowski/operations.v
+++ b/FiniteSets/kuratowski/operations.v
@@ -237,4 +237,4 @@ Section FSet_cons_rec.
   Definition FSet_cons_beta_cons (a : A) (X : FSet A)
     : FSet_cons_rec ({|a|} ∪ X) = Pcons a X (FSet_cons_rec X)
     := ap (fun z => Pcons a z _) (repr_iso_id_l _).
-End FSet_cons_rec.
\ No newline at end of file
+End FSet_cons_rec.
diff --git a/FiniteSets/subobjects/k_finite.v b/FiniteSets/subobjects/k_finite.v
index b3778b0..6509366 100644
--- a/FiniteSets/subobjects/k_finite.v
+++ b/FiniteSets/subobjects/k_finite.v
@@ -65,6 +65,14 @@ End k_finite.
 
 Arguments map {_} {_} _.
 
+Ltac kf_unfold :=
+  repeat match goal with
+  | [ H : Kf ?t |- _ ] => apply Kf_unfold in H
+  | [ H : @trunctype_type _ (Kf ?t) |- _ ] => apply Kf_unfold in H
+  | [ |- Kf ?t ] => apply Kf_unfold
+  | [ |- @trunctype_type _ (Kf _) ] => apply Kf_unfold
+  end.
+
 Section structure_k_finite.
   Context (A : Type).
   Context `{Univalence}.
@@ -120,6 +128,72 @@ End structure_k_finite.
 Section k_properties.
   Context `{Univalence}.
 
+  (* Some closure properties *)
+  (* https://ncatlab.org/nlab/show/finite+object#closure_of_finite_objects *)
+  Lemma Kf_Empty : Kf Empty.
+  Proof.
+    kf_unfold.
+    exists ∅. done.
+  Defined.
+
+  Lemma Kf_Unit : Kf Unit.
+  Proof.
+    kf_unfold.
+    exists {|tt|}.
+    intros []. simpl.
+    apply (tr (idpath)).
+  Defined.
+
+  Lemma Kf_sum {A B : Type} : Kf A -> Kf B -> Kf (A + B).
+  Proof.
+    intros HA HB.
+    kf_unfold.
+    destruct HA as [X HX].
+    destruct HB as [Y HY].
+    exists ((fset_fmap inl X) ∪ (fset_fmap inr Y)).
+    intros [a | b]; simpl; apply tr; [ left | right ];
+      apply fmap_isIn.
+    + apply (HX a).
+    + apply (HY b).
+  Defined.
+
+  Lemma Kf_subterm (A : hProp) : Decidable A <~> Kf A.
+  Proof.
+    apply equiv_iff_hprop.
+    { intros Hdec.
+      kf_unfold.
+      destruct Hdec as [HA | HA].
+      - exists {|HA|}. simpl.
+        intros a. apply tr.
+        apply A.
+      - exists ∅. intros a.
+        apply (HA a). }
+    { intros HA.
+      kf_unfold.
+      destruct HA as [X HX].
+      destruct (merely_choice X) as [HX2 | HX2].
+      + rewrite HX2 in HX.
+        right. unfold not.
+        apply HX.
+      + strip_truncations.
+        destruct HX2 as [a ?].
+        left. apply a. }
+  Defined.
+
+  Lemma Kf_prod {A B : Type} : Kf A -> Kf B -> Kf (A * B).
+  Proof.
+    intros HA HB.
+    kf_unfold.
+    destruct HA as [X HA].
+    destruct HB as [Y HB].
+    exists (product X Y).
+    intros [a b]. unfold map.
+    rewrite product_isIn.
+    split.
+    - apply (HA a).
+    - apply (HB b).
+  Defined.
+
   Lemma Kf_surjection {X Y : Type} (f : X -> Y) `{IsSurjection f} :
     Kf X -> Kf Y.
   Proof.
@@ -243,4 +317,4 @@ Section alternative_definition.
       intro x ; apply k_to_fset_to_k.
   Defined.
   
-End alternative_definition.
\ No newline at end of file
+End alternative_definition.