clean up

Author: Marc Bezem

theories/Cubical/PathSquare.v

@@ -713,23 +713,6 @@ Defined.
 
 (* Interchange playground *)
 
-Definition experimental {A}
-(a : A)
-(P : A -> Type)
-(f : forall (x : A), (a = x) -> P(x))
-(g : forall (x : A), P(x) -> (a = x))
-(fxgxid: forall (x : A) (p : P x), (p = f x (g x p)))
-:
-forall (x : A)(p : P x), p = transport P (g x p) (f a 1).
-
-Proof.
-  intros.
-  remember (g x p) as gxp eqn:H.
-  destruct gxp. (* Syntax error: destruct (g x p) as gxp eqn:H.  *)
-  simpl. (* Here you see that p = f a 1 if g a p = 1 *)
-  destruct H.
-  apply fxgxid.
-Defined.
 
 Definition interchange {A}
   {a00 a10 a20 a01 a11 a21 a02 a12 a22 : A} (* 9 points in big square of 2x2 squares *)
@@ -759,10 +742,8 @@ Definition interchange {A}
   sq_concat_v (sq_concat_h sq00 sq01) (sq_concat_h sq10 sq11).
 Proof.
   destruct sq00, sq11.
-  destruct vi2, h2i. revert vj0 sq10. 
+  destruct vi2, h2i. 
+  revert vj0 sq10. 
   rapply pathsquare_ind_l. 
   reflexivity.
-(*  revert vj0 sq10; rapply pathsquare_ind_l; simpl.
-  revert h0j sq01; rapply pathsquare_ind_t; simpl.
-  reflexivity. *)
 Defined.