Cleaning in iso

FiniteSets/list_representation/isomorphism.v

@@ -5,15 +5,7 @@ Require Import list_representation list_representation.operations
 Require Import kuratowski.kuratowski_sets.
 
 Section Iso.
-  Context {A : Type}.
+  Context {A : Type} `{Univalence}.
-  Context `{Univalence}.
-
-  Definition dupl' (a : A) (X : FSet A) :
-    {|a|} ∪ {|a|} ∪ X = {|a|} ∪ X := assoc _ _ _ @ ap (∪ X) (idem _).
-  
-  Definition comm' (a b : A) (X : FSet A) :
-    {|a|} ∪ {|b|} ∪ X = {|b|} ∪ {|a|} ∪ X :=
-    assoc _ _ _ @ ap (∪ X) (comm _ _) @ (assoc _ _ _)^.
 
   Definition FSetC_to_FSet: FSetC A -> FSet A.
   Proof.
@@ -21,10 +13,10 @@ Section Iso.
     - apply E.
     - intros a x.
       apply ({|a|} ∪ x).
-    - intros. cbn.
+    - intros a X.
-      apply dupl'.
+      apply (assoc _ _ _ @ ap (∪ X) (idem _)).
-    - intros. cbn.
+    - intros a X Y.
-      apply comm'.
+      apply (assoc _ _ _ @ ap (∪ Y) (comm _ _) @ (assoc _ _ _)^).
   Defined.
 
   Definition FSet_to_FSetC: FSet A -> FSetC A.

FiniteSets/list_representation/properties.v

@@ -5,8 +5,8 @@ Require Import list_representation list_representation.operations.
 Section properties.
   Context {A : Type}.
 
-  Definition append_nl : forall (x: FSetC A), ∅ ∪ x = x
+  Definition append_nl (x: FSetC A) : ∅ ∪ x = x
-    := fun _ => idpath.
+    := idpath.
 
   Lemma append_nr : forall (x: FSetC A), x ∪ ∅ = x.
   Proof.
@@ -15,16 +15,16 @@ Section properties.
     - intros. apply (ap (fun y => a;;y) X).
   Defined.
 
-  Lemma append_assoc {H: Funext}:
+  Lemma append_assoc :
     forall (x y z: FSetC A), x ∪ (y ∪ z) = (x ∪ y) ∪ z.
   Proof.
-    hinduction
+    intros x y z.
-    ; try (intros ; apply path_forall ; intro
+    hinduction x ; try (intros ; apply path_ishprop).
-           ; apply path_forall ; intro ;  apply set_path2).
+    - cbn.
-    - reflexivity.
+      reflexivity.
-    - intros a x HR y z.
+    - intros.
-      specialize (HR y z).
+      cbn.
-      apply (ap (fun y => a;;y) HR).
+      f_ap.
   Defined.
 
   Lemma append_singleton: forall (a: A) (x: FSetC A),