From 7c14d36f7d251e030ca11650b21d3d5140ecd16b Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Fri, 9 Feb 2018 18:19:14 +0100
Subject: [PATCH] Universe of finite cardinals

---
 FiniteSets/fincard.v | 59 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 59 insertions(+)
 create mode 100644 FiniteSets/fincard.v

diff --git a/FiniteSets/fincard.v b/FiniteSets/fincard.v
new file mode 100644
index 0000000..85ba9c0
--- /dev/null
+++ b/FiniteSets/fincard.v
@@ -0,0 +1,59 @@
+Require Import FSets list_representation.
+Require Import kuratowski.length misc.dec_kuratowski.
+From interfaces Require Import lattice_interface.
+From subobjects Require Import sub b_finite enumerated k_finite.
+
+Require Import HoTT.Spaces.Card.
+
+Section contents.
+  Context `{Univalence}.
+  
+  Definition isKf_card (X : Card) : hProp.
+  Proof.
+    strip_truncations.
+    refine (Kf X).
+  Defined.
+
+  Definition Kf_card := BuildhSet (@sig Card isKf_card).
+
+  Definition Kf_card' := BuildhSet (Trunc 0 (@sig hSet (fun X => Kf X))).
+
+  Definition f : Kf_card -> Kf_card'.
+  Proof.
+    intros [X HX].
+    unfold Kf_card'.
+    revert HX. strip_truncations.
+    intros HX.
+    apply tr.
+    exists X.
+    apply HX.
+  Defined.
+
+  Definition g : Kf_card' -> Kf_card.
+  Proof.
+    unfold Kf_card, Kf_card'.
+    intros X. strip_truncations.
+    destruct X as [X HX].
+    exists (tr X). apply HX.
+  Defined.
+
+  Instance f_equiv : IsEquiv f.
+  Proof.
+    apply isequiv_biinv.
+    split; exists g.
+    - unfold Sect. unfold Kf_card. simpl.
+      intros [X HX].
+      revert HX. strip_truncations. intros HX.
+      simpl. reflexivity.
+    - intros X. strip_truncations. simpl.
+      reflexivity.
+  Defined.
+
+  Lemma kf_card_equiv :
+    Kf_card = Kf_card'.
+  Proof.
+    apply path_hset.
+    simple refine (BuildEquiv Kf_card Kf_card' f _).
+  Defined.
+
+End contents.