diff --git a/FiniteSets/implementations/interface.v b/FiniteSets/implementations/interface.v
index 9eeeff0..5d5cc6e 100644
--- a/FiniteSets/implementations/interface.v
+++ b/FiniteSets/implementations/interface.v
@@ -19,69 +19,179 @@ Section interface.
       f_filter : forall A φ X, f A (filter φ X) = {| f A X & φ |};
       f_member : forall A a X, member a X = a ∈ (f A X)
     }.
+  
+  Global Instance f_surjective A `{sets} : IsSurjection (f A).
+  Proof.
+    unfold IsSurjection.
+    hinduction ; try (intros ; apply path_ishprop).
+    - simple refine (BuildContr _ _ _).
+      * refine (tr(∅;_)). 
+        apply f_empty.
+      * intros ; apply path_ishprop.
+    - intro a.
+      simple refine (BuildContr _ _ _).
+      * refine (tr({|a|};_)).
+        apply f_singleton.
+      * intros ; apply path_ishprop.
+    - intros Y1 Y2 HY1 HY2.
+      destruct HY1 as [X1' HX1].
+      destruct HY2 as [X2' HX2].
+      simple refine (BuildContr _ _ _).
+      * simple refine (Trunc_rec _ X1') ; intro X1.
+        simple refine (Trunc_rec _ X2') ; intro X2.
+        destruct X1 as [X1 fX1].
+        destruct X2 as [X2 fX2].
+        refine (tr(X1 ∪ X2;_)).
+        rewrite f_union, fX1, fX2.
+        reflexivity.
+      * intros ; apply path_ishprop.
+  Defined.
+
 End interface.
 
-Section properties.
-  Context `{Univalence}.
-  Variable (T : Type -> Type) (f : forall A, T A -> FSet A).
+Section quotient_surjection.
+  Variable (A B : Type)
+           (f : A -> B)
+           (H : IsSurjection f).
+  Context `{IsHSet B} `{Univalence}.
+
+  Definition f_eq : relation A := fun a1 a2 => f a1 = f a2.
+  Definition quotientB : Type := quotient f_eq.
+  
+  Global Instance quotientB_recursion : HitRecursion quotientB :=
+    {
+      indTy := _;
+      recTy :=
+        forall (P : Type) (HP: IsHSet P) (u : A -> P),
+          (forall x y : A, f_eq x y -> u x = u y) -> quotientB -> P;
+      H_inductor := quotient_ind f_eq ;
+      H_recursor := @quotient_rec _ f_eq _
+    }.
+
+  Global Instance R_refl : Reflexive f_eq.
+  Proof.
+    intro.
+    reflexivity.
+  Defined.
+
+  Global Instance R_sym : Symmetric f_eq.
+  Proof.
+    intros a b Hab.
+    apply (Hab^).
+  Defined.
+
+  Global Instance R_trans : Transitive f_eq.
+  Proof.
+    intros a b c Hab Hbc.
+    apply (Hab @ Hbc).
+  Defined.
+
+  Definition quotientB_to_B : quotientB -> B.
+  Proof.
+    hrecursion.
+    - apply f.
+    - done.
+  Defined.
+
+  Instance quotientB_emb : IsEmbedding (quotientB_to_B).
+  Proof.
+    apply isembedding_isinj_hset.
+    unfold isinj.
+    simpl.
+    hrecursion ; [ | intros; apply path_ishprop ].
+    intro.
+    hrecursion ; [ | intros; apply path_ishprop ].
+    intros.
+      by apply related_classes_eq.
+  Defined.
+  
+  Instance quotientB_surj : IsSurjection (quotientB_to_B).
+  Proof.
+    apply BuildIsSurjection.
+    intros Y.
+    destruct (H Y).
+    simple refine (Trunc_rec _ center) ; intro X.
+    apply tr.
+    destruct X as [a fa].
+    apply (class_of _ a;fa).
+  Defined.
+
+  Definition quotient_iso : quotientB <~> B.
+  Proof.
+    refine (BuildEquiv _ _ quotientB_to_B _).
+    apply isequiv_surj_emb; apply _.
+  Defined.
+
+  Definition reflect_eq : forall (X Y : A),
+      f X = f Y -> f_eq X Y.
+  Proof.
+    done.
+  Defined.
+
+  Lemma same_class : forall (X Y : A),
+      class_of f_eq X = class_of f_eq Y -> f_eq X Y.
+  Proof.
+    intros.
+    simple refine (classes_eq_related _ _ _ _) ; assumption.
+  Defined.
+
+End quotient_surjection.
+
+Ltac reduce T :=
+  intros ;
+  repeat (rewrite (f_empty T _)
+          || rewrite (f_singleton T _)
+          || rewrite (f_union T _)
+          || rewrite (f_filter T _)
+          || rewrite (f_member T _)).
+Ltac simplify T := intros ; autounfold in * ; apply reflect_eq ; reduce T.
+Ltac reflect_equality T := simplify T ; eauto with lattice_hints typeclass_instances.
+Ltac reflect_eq T := autounfold
+                     ; repeat (hinduction ; try (intros ; apply path_ishprop) ; intro)
+                     ; apply related_classes_eq
+                     ; reflect_equality T.
+
+Section quotient_properties.
+  Variable (T : Type -> Type).
+  Variable (f : forall {A : Type}, T A -> FSet A).
   Context `{sets T f}.
 
-  Definition set_eq : forall A, T A -> T A -> hProp :=
-    fun A X Y => (BuildhProp (f A X = f A Y)).
-
-  Definition set_subset : forall A, T A -> T A -> hProp :=
-    fun A X Y => (f A X) ⊆ (f A Y).
-
-  Ltac reduce :=
-    intros ;
-    repeat (rewrite (f_empty T _)
-         || rewrite (f_singleton T _)
-         || rewrite (f_union T _)
-         || rewrite (f_filter T _)
-         || rewrite (f_member T _)).
-
-  Definition empty_isIn : forall (A : Type) (a : A),
-    a ∈ ∅ = False_hp.
+  Definition set_eq A := f_eq (T A) (FSet A) (f A).
+  Definition View A : Type := quotientB (T A) (FSet A) (f A).
+  
+  Definition View_rec2 {A} (P : Type) (HP : IsHSet P) (u : T A -> T A -> P) :
+    (forall (x x' : T A), set_eq A x x' -> forall (y y' : T A), set_eq A y y' -> u x y = u x' y')     ->
+    forall (x y : View A), P.
   Proof.
-    by reduce.
+    intros Hresp.
+    assert (resp1 : forall x y y', set_eq A y y' -> u x y = u x y').
+    { intros x y y'.
+      apply (Hresp _ _ idpath).
+    }
+    assert (resp2 : forall x x' y, set_eq A x x' -> u x y = u x' y).
+    { intros x x' y Hxx'.
+      apply Hresp. apply Hxx'.
+      reflexivity. }
+    unfold View.
+    hrecursion.
+    - intros a.
+      hrecursion.
+      + intros b.
+        apply (u a b).
+      + intros b b' Hbb'. simpl.
+          by apply resp1.
+    - intros a a' Haa'. simpl.
+      apply path_forall. red.
+      hinduction.
+      + intros b. apply resp2. apply Haa'.
+      + intros; apply HP.
   Defined.
 
-  Definition singleton_isIn : forall (A : Type) (a b : A),
-    a ∈ {|b|} = merely (a = b).
-  Proof.
-    by reduce.
-  Defined.
-
-  Definition union_isIn : forall (A : Type) (a : A) (X Y : T A),
-    a ∈ (X ∪ Y) = lor (a ∈ X) (a ∈ Y).
-  Proof.
-    by reduce.
-  Defined.
-
-  Definition filter_isIn : forall (A : Type) (a : A) (ϕ : A -> Bool) (X : T A),
-    member a (filter ϕ X) = if ϕ a then member a X else False_hp.
-  Proof.
-    reduce.
-    apply properties.comprehension_isIn.
-  Defined.
-
-  Definition reflect_eq : forall (A : Type) (X Y : T A),
-    f A X = f A Y -> set_eq A X Y.
-  Proof. done. Defined.
-
-  Definition reflect_subset : forall (A : Type) (X Y : T A),
-    subset (f A X) (f A Y) -> set_subset A X Y.
-  Proof. done. Defined.
-
-  Hint Unfold set_eq set_subset.
-
-  Ltac simplify := intros ; autounfold in * ; apply reflect_eq ; reduce.
-
   Definition well_defined_union (A : Type) (X1 X2 Y1 Y2 : T A) :
     set_eq A X1 Y1 -> set_eq A X2 Y2 -> set_eq A (union X1 X2) (union Y1 Y2).
   Proof.
     intros HXY1 HXY2.
-    simplify.
+    simplify T.
     by rewrite HXY1, HXY2.
   Defined.
 
@@ -89,241 +199,153 @@ Section properties.
     set_eq A X Y -> set_eq A (filter ϕ X) (filter ϕ Y).
   Proof.
     intros HXY.
-    simplify.
+    simplify T.
     by rewrite HXY.
   Defined.
 
-  Ltac reflect_equality := simplify ; eauto with lattice_hints typeclass_instances.
-
-  Lemma union_comm : forall A (X Y : T A),
-      set_eq A (X ∪ Y) (Y ∪ X).
+  Global Instance View_member A: hasMembership (View A) A.
   Proof.
-    reflect_equality.
+    intros a ; unfold View.
+    hrecursion.
+    - apply (member a).
+    - intros X Y HXY.
+      reduce T.
+      rewrite HXY.
+      reflexivity.
   Defined.
 
-  Lemma union_assoc : forall A (X Y Z : T A),
-    set_eq A ((X ∪ Y) ∪ Z) (X ∪ (Y ∪ Z)).
+  Global Instance View_empty A: hasEmpty (View A).
   Proof.
-    reflect_equality.
+    apply (class_of _ ∅).
   Defined.
 
-  Lemma union_idem : forall A (X : T A),
-    set_eq A (X ∪ X) X.
+  Global Instance View_singleton A: hasSingleton (View A) A.
   Proof.
-    reflect_equality.
+    intros a.
+    apply (class_of _ {|a|}).
   Defined.
 
-  Lemma union_neutral : forall A (X : T A),
-    set_eq A (∅ ∪ X) X.
+  Instance View_max A : maximum (View A).
   Proof.
-    reflect_equality.
+    simple refine (View_rec2 _ _ _ _).
+    - intros a b.
+      apply (class_of _ (union a b)).
+    - intros x x' Hxx' y y' Hyy' ; simpl.
+      apply related_classes_eq.
+      eapply well_defined_union; eauto.
   Defined.
 
-End properties.
+  Global Instance View_union A: hasUnion (View A).
+  Proof.
+    apply max_L.
+  Defined.
 
-Section quot.
-Variable (T : Type -> Type).
-Variable (f : forall {A : Type}, T A -> FSet A).
-Context `{sets T f}.
+  Global Instance View_comprehension A: hasComprehension (View A) A.
+  Proof.
+    intros ϕ ; unfold View.
+    hrecursion.
+    - intros X.
+      apply (class_of _ (filter ϕ X)).
+    - intros X X' HXX' ; simpl.
+      apply related_classes_eq.
+      eapply well_defined_filter; eauto.
+  Defined.
 
-Definition R A : relation (T A) := set_eq T f A.
-Definition View A : Type := quotient (R A).
+  Hint Unfold Commutative Associative Idempotent NeutralL NeutralR.
 
-Arguments f {_} _.
+  Instance bottom_view A : bottom (View A).
+  Proof.
+    unfold bottom.
+    apply ∅.
+  Defined.
 
-Instance R_refl A : Reflexive (R A).
-Proof. intro. reflexivity. Defined.
+  Global Instance view_lattice A : JoinSemiLattice (View A).
+  Proof.
+    split ; reflect_eq T.
+  Defined.
 
-Instance R_sym A : Symmetric (R A).
-Proof. intros a b Hab. apply (Hab^). Defined.
-
-Instance R_trans A: Transitive (R A).
-Proof. intros a b c Hab Hbc. apply (Hab @ Hbc). Defined.
-
-(* Instance quotient_recursion `{A : Type} (Q : relation A) `{is_mere_relation _ Q} : HitRecursion (quotient Q) := *)
-(*   { *)
-(*     indTy := _; recTy := _;  *)
-(*     H_inductor := quotient_ind Q; H_recursor := quotient_rec Q *)
-(*   }. *)
-
-Instance View_recursion A : HitRecursion (View A) :=
-  {
-    indTy := _; recTy := forall (P : Type) (HP: IsHSet P) (u : T A -> P), (forall x y : T A, set_eq T (@f) A x y -> u x = u y) -> View A -> P;
-    H_inductor := quotient_ind (R A); H_recursor := @quotient_rec _ (R A) _
-  }.
+End quotient_properties.
 
 Arguments set_eq {_} _ {_} _ _.
 
-Definition View_rec2 {A} (P : Type) (HP : IsHSet P) (u : T A -> T A -> P) :
-  (forall (x x' : T A), set_eq (@f) x x' -> forall (y y' : T A), set_eq (@f) y y' -> u x y = u x' y') ->
-  forall (x y : View A), P.
-Proof.
-intros Hresp.
-assert (resp1 : forall x y y', set_eq (@f) y y' -> u x y = u x y').
-{ intros x y y'.
-  apply Hresp.
-  reflexivity. }
-assert (resp2 : forall x x' y, set_eq (@f) x x' -> u x y = u x' y).
-{ intros x x' y Hxx'.
-  apply Hresp. apply Hxx'.
-  reflexivity. }
-hrecursion.
-- intros a.
-  hrecursion.
-  + intros b.
-    apply (u a b).
-  + intros b b' Hbb'. simpl.
-    by apply resp1.
-- intros a a' Haa'. simpl.
-  apply path_forall. red.
-  hinduction.
-  + intros b. apply resp2. apply Haa'.
-  + intros; apply HP.
-Defined.
+Section properties.
+  Context `{Univalence}.
+  Variable (T : Type -> Type) (f : forall A, T A -> FSet A).
+  Context `{sets T f}.
 
-Instance View_max A : maximum (View A).
-Proof.
-compute-[View].
-simple refine (View_rec2 _ _ _ _).
-- intros a b. apply class_of. apply (union a b).
-- intros x x' Hxx' y y' Hyy'. simpl.
-  apply related_classes_eq.
-  unfold R in *.
-  eapply well_defined_union; eauto.
-Defined.
+  Definition set_subset : forall A, T A -> T A -> hProp :=
+    fun A X Y => (f A X) ⊆ (f A Y).
 
-Ltac reduce :=
-  intros ;
-  repeat (rewrite (f_empty T _)
-          || rewrite (f_singleton T _)
-          || rewrite (f_union T _)
-          || rewrite (f_filter T _)
-          || rewrite (f_member T _)).
+  Definition empty_isIn : forall (A : Type) (a : A),
+    a ∈ ∅ = False_hp.
+  Proof.
+    by (reduce T).
+  Defined.
 
-Instance View_member A: hasMembership (View A) A.
-Proof.
-  intros a.
-  hrecursion.
-  - apply (member a).
-  - intros X Y HXY.
-    reduce.
-    unfold R, set_eq in HXY. rewrite HXY.
+  Definition singleton_isIn : forall (A : Type) (a b : A),
+    a ∈ {|b|} = merely (a = b).
+  Proof.
+    by (reduce T).
+  Defined.
+
+  Definition union_isIn : forall (A : Type) (a : A) (X Y : T A),
+    a ∈ (X ∪ Y) = lor (a ∈ X) (a ∈ Y).
+  Proof.
+    by (reduce T).
+  Defined.
+
+  Definition filter_isIn : forall (A : Type) (a : A) (ϕ : A -> Bool) (X : T A),
+    member a (filter ϕ X) = if ϕ a then member a X else False_hp.
+  Proof.
+    reduce T.
+    apply properties.comprehension_isIn.
+  Defined.
+
+  Definition reflect_f_eq : forall (A : Type) (X Y : T A),
+      class_of (set_eq f) X = class_of (set_eq f) Y -> set_eq f X Y.
+  Proof.
+    intros.
+    refine (same_class _ _ _ _ _ _) ; assumption.
+  Defined.
+
+  Lemma class_union (A : Type) (X Y : T A) :
+      class_of (set_eq f) (X ∪ Y) = (class_of (set_eq f) X) ∪ (class_of (set_eq f) Y).
+  Proof.
     reflexivity.
-Defined.
+  Defined.
 
-Instance View_empty A: hasEmpty (View A).
-Proof.
-  apply class_of.
-  apply ∅.
-Defined.
+  Lemma class_filter (A : Type) (X : T A) (ϕ : A -> Bool) :
+    class_of (set_eq f) ({|X & ϕ|}) = {|(class_of (set_eq f) X) & ϕ|}.
+  Proof.
+    reflexivity.
+  Defined.  
 
-Instance View_singleton A: hasSingleton (View A) A.
-Proof.
-  intros a.
-  apply class_of.
-  apply {|a|}.
-Defined.
+  Ltac via_quotient := intros ; apply reflect_f_eq
+                       ; rewrite ?class_union, ?class_filter
+                       ; eauto with lattice_hints typeclass_instances.
 
-Instance View_union A: hasUnion (View A).
-Proof.
-  intros X Y.
-  apply (max_L X Y).
-Defined.
+  Lemma union_comm : forall A (X Y : T A),
+      set_eq f (X ∪ Y) (Y ∪ X).
+  Proof.
+    via_quotient.
+  Defined.
 
-Instance View_comprehension A: hasComprehension (View A) A.
-Proof.
-  intros ϕ.
-  hrecursion.
-  - intros X.
-    apply class_of.
-    apply (filter ϕ X).
-  - intros X X' HXX'. simpl.
-    apply related_classes_eq.
-    eapply well_defined_filter; eauto.
-Defined.
+  Lemma union_assoc : forall A (X Y Z : T A),
+    set_eq f ((X ∪ Y) ∪ Z) (X ∪ (Y ∪ Z)).
+  Proof.
+    via_quotient.
+  Defined.
 
-Instance View_max_comm A: Commutative (@max_L (View A) _).
-Proof.
-  unfold Commutative.
-  hinduction.
-  - intros X.
-    hinduction.
-    + intros Y. cbn.
-      apply related_classes_eq.
-      eapply union_comm; eauto.
-    + intros. apply set_path2.
-  - intros. apply path_forall; intro. apply set_path2.
-Defined.
+  Lemma union_idem : forall A (X : T A),
+    set_eq f (X ∪ X) X.
+  Proof.
+    via_quotient.
+  Defined.
 
-Ltac buggeroff := intros; apply path_ishprop.
+  Lemma union_neutral : forall A (X : T A),
+    set_eq f (∅ ∪ X) X.
+  Proof.
+    via_quotient.
+  Defined.
 
-Instance View_max_assoc A: Associative (@max_L (View A) _).
-Proof.
-  unfold Associative.
-  hinduction; try buggeroff.
-  intros X.
-  hinduction; try buggeroff.
-  intros Y.
-  hinduction; try buggeroff.
-  intros Z. cbn.
-  apply related_classes_eq.
-  eapply union_assoc; eauto.
-Defined.
-
-Instance View_max_idem A: Idempotent (@max_L (View A) _).
-Proof.
-  unfold Idempotent.
-  hinduction; try buggeroff.
-  intros X; cbn.
-  apply related_classes_eq.
-  eapply union_idem; eauto.
-Defined.
-
-Instance View_max_neut A: NeutralL (@max_L (View A) _) ∅.
-Proof.
-  unfold NeutralL.
-  hinduction; try buggeroff.
-  intros X; cbn.
-  apply related_classes_eq.
-  eapply union_neutral; eauto.
-Defined.
-
-Definition View_FSet A : View A -> FSet A.
-Proof.
-hrecursion.
-- apply f.
-- done.
-Defined.
-
-Instance View_emb A : IsEmbedding (View_FSet A).
-Proof.
-apply isembedding_isinj_hset.
-unfold isinj.
-hrecursion; [ | intros; apply path_ishprop ]. intro X.
-hrecursion; [ | intros; apply path_ishprop ]. intro Y.
-intros. by apply related_classes_eq.
-Defined.
-
-Instance View_surj A: IsSurjection (View_FSet A).
-Proof.
-apply BuildIsSurjection.
-intros X. apply tr.
-hrecursion X; try (intros; apply path_ishprop).
-- exists ∅. simpl. eapply f_empty; eauto.
-- intros a. exists {|a|}; simpl. eapply f_singleton; eauto.
-- intros X Y [pX HpX] [pY HpY].
-  exists (pX ∪ pY); simpl.
-  rewrite <- HpX, <- HpY.
-  clear HpX HpY.
-  hrecursion pY; [ | intros; apply set_path2]. intro tY.
-  hrecursion pX; [ | intros; apply set_path2]. intro tX.
-  eapply f_union; eauto.
-Defined.
-
-Definition view_iso A : View A <~> FSet A.
-Proof.
-refine (BuildEquiv _ _ (View_FSet A) _).
-apply isequiv_surj_emb; apply _.
-Defined.
-
-End quot.
+End properties.
\ No newline at end of file