Simplified proof of extensionality

FiniteSets/disjunction.v

@@ -13,64 +13,41 @@ Section lor_props.
   Context `{Univalence}.
   Variable X Y Z : hProp.
 
+  Local Ltac lor_intros :=
+    let x := fresh in intro x
+             ; repeat (strip_truncations ; destruct x as [x | x]).
+  
+  
   Lemma lor_assoc : (X ∨ Y) ∨ Z = X ∨ Y ∨ Z.
   Proof.
-    apply path_iff_hprop ; cbn.
+    apply path_iff_hprop ; lor_intros
-    * simple refine (Trunc_ind _ _).
+    ; apply tr ; auto
-      intros [xy | z] ; cbn.
+    ; try (left ; apply tr)
-      + simple refine (Trunc_ind _ _ xy).
+    ; try (right ; apply tr) ; auto.
-        intros [x | y].
+  Defined.  
-        ++ apply (tr (inl x)).
-        ++ apply (tr (inr (tr (inl y)))).
-      + apply (tr (inr (tr (inr z)))).
-    * simple refine (Trunc_ind _ _).
-      intros [x | yz] ; cbn.
-      + apply (tr (inl (tr (inl x)))).
-      + simple refine (Trunc_ind _ _ yz).
-        intros [y | z].
-        ++ apply (tr (inl (tr (inr y)))).
-        ++ apply (tr (inr z)).
-  Defined.
 
   Lemma lor_comm : X ∨ Y = Y ∨ X.
   Proof.
-    apply path_iff_hprop ; cbn.
+    apply path_iff_hprop ; lor_intros
-    * simple refine (Trunc_ind _ _).
+    ; apply tr ; auto.
-      intros [x | y].
-      + apply (tr (inr x)).
-      + apply (tr (inl y)).
-    * simple refine (Trunc_ind _ _).
-      intros [y | x].
-      + apply (tr (inr y)).
-      + apply (tr (inl x)).
   Defined.
 
   Lemma lor_nl : False_hp ∨ X = X.
   Proof.
-    apply path_iff_hprop ; cbn.
+    apply path_iff_hprop ; lor_intros ; try contradiction
-    * simple refine (Trunc_ind _ _).
+    ; try (refine (tr(inr _))) ; auto.
-      intros [ | x].
-      + apply Empty_rec.
-      + apply x.
-    * apply (fun x => tr (inr x)).
   Defined.
 
   Lemma lor_nr : X ∨ False_hp = X.
   Proof.
-    apply path_iff_hprop ; cbn.
+    apply path_iff_hprop ; lor_intros ; try contradiction
-    * simple refine (Trunc_ind _ _).
+    ; try (refine (tr(inl _))) ; auto.
-      intros [x | ].
-      + apply x.
-      + apply Empty_rec.
-    * apply (fun x => tr (inl x)).
   Defined.
 
   Lemma lor_idem : X ∨ X = X.
   Proof.
-    apply path_iff_hprop ; cbn.
+    apply path_iff_hprop ; lor_intros
-    - simple refine (Trunc_ind _ _).
+    ; try(refine (tr(inl _))) ; auto.
-      intros [x | x] ; apply x.
-    - apply (fun x => tr (inl x)).
   Defined.
 
 End lor_props.

FiniteSets/fsets/extensionality_alt.v

@@ -6,23 +6,20 @@ Section ext.
   Context {A : Type}.
   Context `{Univalence}.
 
-  Lemma equiv_subset_l : forall (X Y : FSet A), Y ∪ X = X -> forall a, a ∈ Y -> a ∈ X.
+  Lemma equiv_subset1_l (X Y : FSet A) (H1 : Y ∪ X = X) (a : A) (Ya : a ∈ Y) : a ∈ X.
   Proof.
-    intros X Y H1 a Ya.
+    apply (transport (fun Z => a ∈ Z) H1 (tr(inl Ya))).
-    rewrite <- H1.
-    apply (tr(inl Ya)).
   Defined.
-
+  
-  Lemma equiv_subset_r : forall (X Y : FSet A), (forall a, a ∈ Y -> a ∈ X) -> Y ∪ X = X.
+  Lemma equiv_subset1_r X : forall (Y : FSet A), (forall a, a ∈ Y -> a ∈ X) -> Y ∪ X = X.
   Proof.
-    intros X.
+    hinduction ; try (intros ; apply path_ishprop).
-    hinduction ; try (intros ; apply path_forall ; intro ; apply path_ishprop).
     - intros.
       apply nl.
     - intros b sub.
       specialize (sub b (tr idpath)).
       revert sub.
-      hinduction X ; try (intros ; apply path_forall ; intro ; apply path_ishprop).
+      hinduction X ; try (intros ; apply path_ishprop).
       * contradiction.
       * intros.
         strip_truncations.
@@ -30,45 +27,42 @@ Section ext.
         apply union_idem.
       * intros X Y subX subY mem.
         strip_truncations.
-        destruct mem.
+        destruct mem as [t | t].
-        ** rewrite assoc.
+        ** rewrite assoc, (subX t).
-           rewrite (subX t).
            reflexivity.
-        ** rewrite (comm X).
+        ** rewrite (comm X), assoc, (subY t).
-           rewrite assoc.
-           rewrite (subY t).
            reflexivity.
     - intros Y1 Y2 H1 H2 H3.
       rewrite <- assoc.
       rewrite (H2 (fun a HY => H3 a (tr(inr HY)))).
-      rewrite (H1 (fun a HY => H3 a (tr(inl HY)))).
+      apply (H1 (fun a HY => H3 a (tr(inl HY)))).
-      reflexivity.
+  Defined.
-  Defined.        
 
-  Lemma eq_subset' (X Y : FSet A) : X = Y <~> (Y ∪ X = X) * (X ∪ Y = Y).
+  Lemma eq_subset1 X Y : (Y ∪ X = X) * (X ∪ Y = Y) <~> forall (a : A), a ∈ X = a ∈ Y.
+  Proof.    
+    eapply equiv_iff_hprop_uncurried ; split.
+    - intros [H1 H2] a.
+      apply path_iff_hprop ; apply equiv_subset1_l ; assumption.
+    - intros H1.
+      split ; apply equiv_subset1_r ; intros.
+      * rewrite H1 ; assumption.
+      * rewrite <- H1 ; assumption.
+  Defined.
+
+  Lemma eq_subset2 (X Y : FSet A) : X = Y <~> (Y ∪ X = X) * (X ∪ Y = Y).
   Proof.
-    unshelve eapply BuildEquiv.
+    eapply equiv_iff_hprop_uncurried ; split.
-    { intro H'. rewrite H'. split; apply union_idem. }
+    - intro Heq.
-    unshelve esplit.
+      split.
-    { intros [H1 H2]. etransitivity. apply H1^.
+      * apply (ap (fun Z => Z ∪ X) Heq^ @ union_idem X).
-      rewrite comm. apply H2. }
+      * apply (ap (fun Z => Z ∪ Y) Heq @ union_idem Y).
-    intro; apply path_prod; apply set_path2.
+    - intros [H1 H2].
-    all: intro; apply set_path2.
+      apply (H1^ @ comm Y X @ H2).
   Defined.
   
   Theorem fset_ext (X Y : FSet A) :
-    X = Y <~> (forall (a : A), a ∈ X = a ∈ Y).
+    X = Y <~> forall (a : A), a ∈ X = a ∈ Y.
   Proof.
-    refine (@equiv_compose' _ _ _ _ _) ; [ | apply eq_subset' ].
+    apply (equiv_compose' (eq_subset1 X Y) (eq_subset2 X Y)).
-    eapply equiv_iff_hprop_uncurried ; split.
-    - intros [H1 H2 a].
-      apply path_iff_hprop ; apply equiv_subset_l ; assumption.
-    - intros H1.
-      split ; apply equiv_subset_r.
-      * intros a Ya.
-        rewrite (H1 a) ; assumption.
-      * intros a Xa.
-        rewrite <- (H1 a) ; assumption.
   Defined.
-
 End ext.