Added structure to k_finite sts

FiniteSets/Sub.v

@@ -5,10 +5,17 @@ Section subobjects.
   Variable A : Type.
 
   Definition Sub := A -> hProp.
+
+  Definition empty_sub : Sub := fun _ => False_hp.
+
+  Definition singleton (a : A) : Sub := fun b => BuildhProp (Trunc (-1) (b = a)).
 End subobjects.
 
-Section blah.
-  Variable A : Type.
+Arguments empty_sub {_}.
+Arguments singleton {_} _.
+
+Section sub_classes.
+  Context {A : Type}.
   Variable C : (A -> hProp) -> hProp.
   Context `{Univalence}.
 
@@ -20,4 +27,90 @@ Section blah.
 
   Definition hasUnion := forall X Y, C X -> C Y -> C (max_fun X Y).
   Definition hasIntersection := forall X Y, C X -> C Y -> C (min_fun X Y).
-End blah.
+  Definition hasEmpty := C empty_sub.
+  Definition hasSingleton := forall a, C (singleton a).
+  Definition hasDecidableEmpty := forall X, C X -> hor (X = empty_sub) (hexists (fun a => X a)).
+End sub_classes.
+
+Section isIn.
+  Variable A : Type.
+  Variable C : (A -> hProp) -> hProp.
+
+  Context `{Univalence}.
+  Context {HS : hasSingleton C} {HIn : forall X, C X -> forall a, Decidable (X a)}.
+
+  Theorem decidable_A_isIn : forall a b : A, Decidable (Trunc (-1) (b = a)).
+  Proof.
+    intros.
+    unfold Decidable, hasSingleton in *.
+    pose (HIn (singleton a) (HS a) b).
+    destruct s.
+    - unfold singleton in t.
+      left.
+      apply t.
+    - right.
+      intro p.
+      unfold singleton in n.
+      strip_truncations.
+      contradiction (n (tr p)).
+  Defined.
+
+End isIn.
+
+Context `{Univalence}.
+
+Instance koe : forall (T : Type) (Ttrunc : IsHProp T), IsTrunc (-1) (T + ~T).
+Proof.
+  intros.
+  apply (equiv_hprop_allpath _)^-1.
+  intros [x | nx] [y | ny] ; try f_ap ; try (apply Ttrunc) ; try contradiction.
+  - apply equiv_hprop_allpath. apply _.
+Defined.    
+
+Section intersect.
+  Variable A : Type.
+  Variable C : (Sub A) -> hProp.
+
+  Context `{Univalence}.
+  Context
+    {HI :hasIntersection C} {HE : hasEmpty C}
+    {HS : hasSingleton C} {HDE : hasDecidableEmpty C}.
+
+  Theorem decidable_A_intersect : forall a b : A, Decidable (Trunc (-1) (b = a)).
+  Proof.
+    intros.
+    unfold Decidable, hasEmpty, hasIntersection, hasSingleton, hasDecidableEmpty in *.
+    pose (HI (singleton a) (singleton b) (HS a) (HS b)) as IntAB.
+    pose (HDE (min_fun (singleton a) (singleton b)) IntAB) as IntE.
+    Print Trunc_rec.
+    refine (@Trunc_rec _ _ _  _ _ IntE) ; intros [p | p] ; unfold min_fun, singleton in p.
+    - right.
+      pose (apD10 p b) as pb ; unfold empty_sub in pb ; cbn in pb.
+      assert (BuildhProp (Trunc (-1) (b = b)) = Unit_hp).
+      {
+        apply path_iff_hprop.
+        - apply (fun _ => tt).
+        - apply (fun _ => tr idpath).          
+      }
+      rewrite X in pb.
+      unfold Unit_hp in pb.
+      assert (forall P : hProp, land P Unit_hp = P).
+      {
+        intro P.
+        apply path_iff_hprop.
+        - intros [x _] ; assumption.
+        - apply (fun x => (x, tt)).          
+      }
+      rewrite (X0 (BuildhProp (Trunc (-1) (b = a)))) in pb.
+      intro q.
+      assert (BuildhProp (Trunc (-1) (b = a))).
+      {
+        apply q.
+      }
+      apply (pb # X1).
+    - strip_truncations.
+      destruct p as [a0 [t1 t2]].
+      strip_truncations.
+      apply (inl (tr (t2^ @ t1))).
+  Defined.
+End intersect.

FiniteSets/fsets/properties.v

@@ -151,4 +151,34 @@ Section properties.
       reflexivity.
   Defined.
   
+  Lemma merely_choice : forall X : FSet A, hor (X = E) (hexists (fun a => isIn a X)).
+  Proof.
+    hinduction; try (intros; apply equiv_hprop_allpath ; apply _).
+    - apply (tr (inl idpath)).
+    - intro a.
+      refine (tr (inr (tr (a ; tr idpath)))).
+    - intros X Y TX TY.
+      strip_truncations.
+      destruct TX as [XE | HX] ; destruct TY as [YE | HY] ; try(strip_truncations ; apply tr).
+      * apply tr ; left.
+        rewrite XE, YE.
+        apply (union_idem E).
+      * right.
+        destruct HY as [a Ya].
+        apply tr.
+        exists a.
+        apply (tr (inr Ya)).
+      * right.
+        destruct HX as [a Xa].
+        apply tr.
+        exists a.
+        apply (tr (inl Xa)).
+      * right.
+        destruct HX as [a Xa].
+        destruct HY as [b Yb].
+        apply tr.
+        exists a.
+        apply (tr (inl Xa)).
+  Defined.
+
 End properties.

FiniteSets/variations/k_finite.v

@@ -1,18 +1,11 @@
 Require Import HoTT HitTactics.
-Require Import lattice representations.definition fsets.operations extensionality.
-
-Definition Sub A := A -> hProp.
+Require Import lattice representations.definition fsets.operations extensionality Sub fsets.properties.
 
 Section k_finite.
 
   Context {A : Type}.
   Context `{Univalence}.
 
-  Instance subA_set : IsHSet (Sub A).
-  Proof.
-    apply _.
-  Defined.
-
   Definition map (X : FSet A) : Sub A := fun a => isIn a X.
 
   Instance map_injective : IsEmbedding map.
@@ -52,3 +45,58 @@ Section k_finite.
   Defined.
 
 End k_finite.
+
+Section structure_k_finite.
+  Context {A : Type}.
+  Context `{Univalence}.
+
+  Lemma map_union : forall X Y : FSet A, map (U X Y) = max_fun (map X) (map Y).
+  Proof.
+    intros.
+    unfold map, max_fun.
+    reflexivity.
+  Defined.
+      
+  Lemma k_finite_union : @hasUnion A Kf_sub.
+  Proof.
+    unfold hasUnion, Kf_sub, Kf_sub_intern.
+    intros.
+    destruct X0 as [SX XP].
+    destruct X1 as [SY YP].
+    exists (U SX SY).
+    rewrite map_union.
+    rewrite XP, YP.
+    reflexivity.
+  Defined.
+
+  Lemma k_finite_empty : @hasEmpty A Kf_sub.
+  Proof.
+    unfold hasEmpty, Kf_sub, Kf_sub_intern, map, empty_sub.
+    exists E.
+    reflexivity.
+  Defined.
+
+  Lemma k_finite_singleton : @hasSingleton A Kf_sub.
+  Proof.
+    unfold hasSingleton, Kf_sub, Kf_sub_intern, map, singleton.
+    intro.
+    exists (L a).
+    cbn.
+    apply path_forall.
+    intro z. 
+    reflexivity.
+  Defined.
+
+  Lemma k_finite_hasDecidableEmpty : @hasDecidableEmpty A Kf_sub.
+  Proof.
+    unfold hasDecidableEmpty, hasEmpty, Kf_sub, Kf_sub_intern, map.
+    intros.
+    destruct X0 as [SX EX].
+    rewrite EX.
+    simple refine (Trunc_ind _ _ (merely_choice SX)).
+    intros [SXE | H1].
+    - rewrite SXE.
+      apply (tr (inl idpath)).
+    - apply (tr (inr H1)).
+  Defined.
+End structure_k_finite.