Added decidable quantification

FiniteSets/_CoqProject

@@ -25,4 +25,5 @@ misc/bad.v
 misc/dec_lem.v
 misc/ordered.v
 misc/projective.v
-misc/dec_kuratowski.v
+misc/dec_kuratowski.v
+misc/dec_fset.v

FiniteSets/misc/dec_fset.v

@@ -116,4 +116,18 @@ Section quantifiers.
   Proof.
     hinduction ; try (apply _) ; try (intros ; apply path_ishprop).
   Defined.
-End quantifiers.
+End quantifiers.
+
+Section simple_example.
+  Context `{Univalence}.
+
+  Definition P : nat -> hProp := fun n => BuildhProp(n = n).
+  Definition X : FSet nat := {|0|} ∪ {|1|}.
+
+  Definition simple_example : all P X.
+  Proof.
+    refine (from_squash (all P X)).
+    compute.
+    apply tt.
+  Defined.
+End simple_example.

FiniteSets/prelude.v

@@ -1,6 +1,20 @@
 (** Some general prerequisities in homotopy type theory. *)
 Require Import HoTT.
 
+Definition squash (A : Type) `{Decidable A} : Type :=
+  match dec A with
+  | inl _ => Unit
+  | inr _ => Empty
+  end.
+
+Definition from_squash (A : Type) `{Decidable A} {x : squash A} : A.
+Proof.
+  unfold squash in *.
+  destruct (dec A).
+  - apply a.
+  - contradiction.
+Defined.
+
 Lemma ap_inl_path_sum_inl {A B} (x y : A) (p : inl x = inl y) :
   ap inl (path_sum_inl B p) = p.
 Proof.