From 7281bfc0bfd79d3740fd6b5a72483f1b6478d7e6 Mon Sep 17 00:00:00 2001
From: Niels van der Weide <n.vanderweide@science.ru.nl>
Date: Mon, 25 Sep 2017 13:03:51 +0200
Subject: [PATCH] Added `S1` has merely decidable equality

---
 FiniteSets/prelude.v             | 49 ++++++++++++++++++++++++++++++++
 FiniteSets/subobjects/b_finite.v |  2 +-
 2 files changed, 50 insertions(+), 1 deletion(-)

diff --git a/FiniteSets/prelude.v b/FiniteSets/prelude.v
index 515ab6a..6326833 100644
--- a/FiniteSets/prelude.v
+++ b/FiniteSets/prelude.v
@@ -57,6 +57,55 @@ Defined.
 Class MerelyDecidablePaths A :=
   m_dec_path : forall (a b : A), Decidable(Trunc (-1) (a = b)).
 
+Definition S1_merely_decidable_equality `{Univalence} : MerelyDecidablePaths S1.
+Proof.
+  simple refine (S1_ind _ _ _) ; simpl.
+  - simple refine (S1_ind _ _ _) ; simpl.
+    * apply (inl (tr idpath)).
+    * apply path_ishprop.      
+  - apply path_forall.
+    intro z.
+    rewrite transport_forall, transport_sum.
+    destruct
+      (transportD (fun _ : S1 => S1)
+                  (fun x y : S1 => Decidable (Trunc (-1) (x = y)))
+                  loop
+                  (transport (fun _ : S1 => S1) loop^ z)
+                  (S1_ind
+                     (fun x : S1 => Decidable (Trunc (-1) (base = x)))
+                     (inl (tr 1%path))
+                     (transport_sum loop (inl (tr 1))
+                                    @
+                                    ap inl
+                                    (path_ishprop
+                                       (transport
+                                          (fun a : S1 => Trunc (-1) (base = a))
+                                          loop
+                                          (tr 1))
+                                       (tr 1)
+                                    )
+                     )
+                     (transport (fun _ : S1 => S1) loop^ z)
+                  )
+      )
+      as [t | n].
+    ** revert t.
+       revert z.
+       simple refine (S1_ind (fun _ => _) _ _) ; simpl.
+       *** intros.
+           apply path_ishprop.
+       *** apply path_forall.
+           intro z.
+           rewrite transport_forall, transport_paths_FlFr, ap_const.
+           hott_simpl.
+           apply set_path2.
+    ** contradiction n.
+       rewrite ?transport_const.
+       simple refine (S1_ind (fun q => Trunc (-1) (base = q)) _ _ z) ; simpl.
+       *** apply (tr idpath).
+       *** apply path_ishprop.
+Defined.
+
 Global Instance DecidableToMerely A (H : DecidablePaths A) : MerelyDecidablePaths A.
 Proof.
   intros x y.
diff --git a/FiniteSets/subobjects/b_finite.v b/FiniteSets/subobjects/b_finite.v
index a85102a..f24fed1 100644
--- a/FiniteSets/subobjects/b_finite.v
+++ b/FiniteSets/subobjects/b_finite.v
@@ -492,4 +492,4 @@ Proof.
       apply path_ishprop.
     * exists (fun a => (a;HY a)).
       intros b. reflexivity.
-Defined.
+Defined.
\ No newline at end of file