From 5233fc6de9fec86dac225aa2629b16f7e9bcb2dd Mon Sep 17 00:00:00 2001
From: Niels <nnmvdw@gmail.com>
Date: Wed, 9 Aug 2017 12:07:43 +0200
Subject: [PATCH] Added proof that the finite sets in HoTTlibrary have no
 intersection and union

---
 FiniteSets/Sub.v | 144 ++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 142 insertions(+), 2 deletions(-)

diff --git a/FiniteSets/Sub.v b/FiniteSets/Sub.v
index 1b4a893..29bffa8 100644
--- a/FiniteSets/Sub.v
+++ b/FiniteSets/Sub.v
@@ -24,9 +24,8 @@ Section sub_classes.
   Variable C : (A -> hProp) -> hProp.
   Context `{Univalence}.
 
-  Instance blah : Lattice (Sub A).
+  Instance subobject_lattice : Lattice (Sub A).
   Proof.
-    unfold Sub.
     apply _.
   Defined.  
 
@@ -101,3 +100,144 @@ Section intersect.
       apply (inl (tr (t2^ @ t1))).
   Defined.
 End intersect.
+
+Section finite_hott.
+  Variable A : Type.
+  Context `{Univalence} `{IsHSet A}.
+  
+  Definition finite (X : Sub A) : hProp := BuildhProp (Finite {a : A & a ∈ X}).
+
+  Definition singleton : closedSingleton finite.
+  Proof.
+    intros a.
+    simple refine (Build_Finite _ _ _).
+    - apply 1.
+    - apply tr.
+      simple refine (BuildEquiv _ _ _ _).
+      * apply (fun _ => inr tt).
+      * simple refine (BuildIsEquiv _ _ _ _ _ _ _) ; unfold Sect in *.
+        ** apply (fun _ => (a;tr idpath)).
+        ** intros x ; destruct x as [ | x] ; try contradiction.
+           destruct x ; reflexivity.
+        ** intros [b bp] ; simpl.
+           strip_truncations.
+           simple refine (path_sigma _ _ _ _ _).
+           *** apply bp^.
+           *** apply path_ishprop.
+        ** intros.
+           apply path_ishprop.
+  Defined.
+
+  Definition empty_finite : closedEmpty finite.
+  Proof.
+    simple refine (Build_Finite _ _ _).
+    - apply 0.
+    - apply tr.
+      simple refine (BuildEquiv _ _ _ _).
+      intros [a p] ; apply p.
+  Defined.
+
+  Definition decidable_empty_finite : hasDecidableEmpty finite.
+  Proof.
+    intros X Y.
+    destruct Y as [n Xn].
+    strip_truncations.
+    simpl in Xn.
+    destruct Xn as [f [g fg gf adj]].
+    destruct n.
+    - refine (tr(inl _)).
+      unfold empty.
+      apply path_forall.
+      intro z.
+      apply path_iff_hprop.
+      * intros p.
+        contradiction (f(z;p)).
+      * contradiction.
+    - refine (tr(inr _)).
+      apply (tr(g(inr tt))).
+  Defined.
+  
+  Lemma no_union
+        (f : forall (X Y : Sub A),
+            Finite {a : A & X a} -> Finite {a : A & Y a}
+            -> Finite ({a : A & (X ∪ Y) a}))
+        (a b : A)
+    :
+      hor (a = b) (a = b -> Empty).
+  Proof.
+    specialize (f {|a|} {|b|} (singleton a) (singleton b)).
+    destruct f as [n pn].
+    strip_truncations.
+    destruct pn as [f [g fg gf adj]].
+    unfold Sect in *.
+    destruct n.
+    - cbn in *. contradiction f.
+      exists a.
+      apply (tr(inl(tr idpath))).
+    - destruct n ; cbn in *.
+      -- pose ((a;tr(inl(tr idpath)))
+               : {a0 : A & Trunc (-1) (Trunc (-1) (a0 = a) + Trunc (-1) (a0 = b))})
+         as s1.
+         pose ((b;tr(inr(tr idpath)))
+               : {a0 : A & Trunc (-1) (Trunc (-1) (a0 = a) + Trunc (-1) (a0 = b))})
+         as s2.
+         pose (f s1) as fs1.
+         pose (f s2) as fs2.
+         assert (fs1 = fs2) as fs_eq.
+         { apply path_ishprop. }
+         pose (g fs1) as gfs1.
+         pose (g fs2) as gfs2.
+         refine (tr(inl _)).
+         refine (ap (fun x => x.1) (gf s1)^ @ _ @ (ap (fun x => x.1) (gf s2))). 
+         unfold fs1, fs2 in fs_eq. rewrite fs_eq.
+         reflexivity.
+      -- refine (tr(inr _)).
+         intros p.
+         pose (inl(inr tt) : Fin n + Unit + Unit) as s1.
+         pose (inr tt : Fin n + Unit + Unit) as s2.
+         pose (g s1) as gs1.
+         pose (c := g s1).
+         assert (c = gs1) as ps1. reflexivity.
+         pose (g s2) as gs2.
+         pose (d := g s2).
+         assert (d = gs2) as ps2. reflexivity.
+         pose (f gs1) as gfs1.
+         pose (f gs2) as gfs2.
+         destruct c as [x px] ; destruct d as [y py].
+         simple refine (Trunc_ind _ _ px) ; intros p1.
+         simple refine (Trunc_ind _ _ py) ; intros p2.
+         simpl.
+         assert (x = y -> Empty) as X1.
+         {
+           enough (s1 = s2) as X.
+           {
+             intros. 
+             unfold s1, s2 in X.
+             refine (not_is_inl_and_inr' (inl(inr tt)) _ _).
+             + apply tt.
+             + rewrite X ; apply tt.
+           }
+           transitivity gfs1.
+           { unfold gfs1, s1. apply (fg s1)^. }
+           symmetry ; transitivity gfs2.
+           { unfold gfs2, s2. apply (fg s2)^. }
+           unfold gfs2, gfs1.
+           rewrite <- ps1, <- ps2.
+           f_ap.
+           simple refine (path_sigma _ _ _ _ _).
+           * cbn.
+             destruct p1 as [p1 | p1] ; destruct p2 as [p2 | p2] ; strip_truncations.
+             ** apply (p2 @ p1^).
+             ** refine (p2 @ _^ @ p1^). auto.
+             ** refine (p2 @ _ @ p1^). auto.
+             ** apply (p2 @ p1^).                              
+           * apply path_ishprop.
+         }
+         apply X1.
+         destruct p1 as [p1 | p1] ; destruct p2 as [p2 | p2] ; strip_truncations.
+         ** apply (p1 @ p2^).
+         ** refine (p1 @ _ @ p2^). auto.
+         ** refine (p1 @ _ @ p2^). symmetry. auto.
+         ** apply (p1 @ p2^).
+  Defined.
+End finite_hott.
\ No newline at end of file