From 97002d119b4780e9b83506b6aa6d9d172adcf815 Mon Sep 17 00:00:00 2001
From: Niels van der Weide <n.vanderweide@science.ru.nl>
Date: Mon, 9 Oct 2017 14:00:16 +0200
Subject: [PATCH] Added refinement

---
 FiniteSets/interfaces/set_interface.v | 30 ++++++++++++++++++++++++++-
 1 file changed, 29 insertions(+), 1 deletion(-)

diff --git a/FiniteSets/interfaces/set_interface.v b/FiniteSets/interfaces/set_interface.v
index 26fed60..9ce119f 100644
--- a/FiniteSets/interfaces/set_interface.v
+++ b/FiniteSets/interfaces/set_interface.v
@@ -348,4 +348,32 @@ Section properties.
     via_quotient.
   Defined.
   
-End properties.
\ No newline at end of file
+End properties.
+
+Section refinement.
+  Variable (T S : Type -> Type).
+  Variable (f : forall {A : Type}, T A -> FSet A).
+  Variable (g : forall {A : Type}, S A -> FSet A).
+  Context `{sets T f} `{sets S g}.
+
+  Theorem transfer
+          (A B : Type)
+          `{IsHSet B}
+          (h : T A -> B)
+          (hresp : forall x y : T A, set_eq f x y -> h x = h y)
+    : S A -> B.
+  Proof.
+    intros X.
+    simple refine (@quotient_rec (T A) (set_eq f) _ _ _ h hresp _).
+    pose (quotient_iso (f A))^-1.
+    apply q.
+    apply (quotient_iso (g A) (class_of _ X)).
+  Defined.
+
+  Definition refine
+          (A B : Type)
+          `{IsHSet B}
+          (h : FSet A -> B)
+    : T A -> B
+  := fun X => h(quotient_iso (f A) (class_of _ X)).
+End refinement.
\ No newline at end of file