Further cleaning

FiniteSets/Sub.v

@@ -1,5 +1,5 @@
 Require Import HoTT.
-Require Import disjunction lattice notation.
+Require Import disjunction lattice notation plumbing.
 
 Section subobjects.
   Variable A : Type.
@@ -57,17 +57,7 @@ End isIn.
 Section intersect.
   Variable A : Type.
   Variable C : (Sub A) -> hProp.
-  Context `{Univalence}.
-
-  Global Instance hprop_lem : forall (T : Type) (Ttrunc : IsHProp T), IsHProp (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.
-
-  Context
+  Context `{Univalence}
     {HI : closedIntersection C} {HE : closedEmpty C}
     {HS : closedSingleton C} {HDE : hasDecidableEmpty C}.
 
@@ -85,4 +75,4 @@ Section intersect.
       strip_truncations.
       apply (inl (tr (t2^ @ t1))).
   Defined.
-End intersect.
+End intersect.

FiniteSets/plumbing.v

@@ -14,3 +14,10 @@ Defined.
 Lemma ap_equiv {A B} (f : A <~> B) {x y : A} (p : x = y) :
   ap (f^-1 o f) p = eissect f x @ p @ (eissect f y)^.
 Proof. destruct p. hott_simpl. Defined.
+
+Global Instance hprop_lem `{Univalence} (T : Type) (Ttrunc : IsHProp T) : IsHProp (T + ~T).
+  Proof.
+    apply (equiv_hprop_allpath _)^-1.
+    intros [x | nx] [y | ny] ; try f_ap ; try (apply Ttrunc) ; try contradiction.
+    - apply equiv_hprop_allpath. apply _.
+  Defined.

FiniteSets/representations/T.v

@@ -15,11 +15,6 @@ Section TR.
     | inr tt, inr tt => Unit_hp
     end.
 
-  Global Instance R_mere : is_mere_relation _ R.
-  Proof.
-    intros x y ; destruct x ; destruct y ; apply _.
-  Defined.
-
   Global Instance R_refl : Reflexive R.
   Proof.
     intro x ; destruct x as [[ ] | [ ]] ; apply tt.