Merge pull request #904 from SimonBoulier/sigma_notations

Add notations (x ; y ; z) to ( x ; y ; z ; t ; u ; v )

theories/Basics/Overture.v

@@ -144,7 +144,12 @@ Open Scope core_scope.
 Definition const {A B} (b : B) := fun x : A => b.
 
 (** We define notation for dependent pairs because it is too annoying to write and see [existT P x y] all the time.  However, we put it in its own scope, because sometimes it is necessary to give the particular dependent type, so we'd like to be able to turn off this notation selectively. *)
+(* We define notations for nested pairs as we can't define a recursive notations; see https://github.com/coq/coq/issues/6032 (should be solved in Coq 8.8). *)
 Notation "( x ; y )" := (existT _ x y) : fibration_scope.
+Notation "( x ; y ; z )" := (x ; ( y ; z)) : fibration_scope.
+Notation "( x ; y ; z ; t )" := (x ; ( y ; (z ; t))) : fibration_scope.
+Notation "( x ; y ; z ; t ; u )" := (x ; ( y ; (z ; (t ; u)))) : fibration_scope.
+Notation "( x ; y ; z ; t ; u ; v )" := (x ; ( y ; (z ; (t ; (u ; v))))) : fibration_scope.
 (** We bind [fibration_scope] with [sigT] so that we are automatically in [fibration_scope] when we are passing an argument of type [sigT]. *)
 Bind Scope fibration_scope with sigT.
 

theories/Pullback.v

@@ -26,7 +26,7 @@ Definition pullback_corec {A B C D}
            {f : A -> B} {g : C -> D} {h : A -> C} {k : B -> D}
            (p : k o f == g o h)
 : A -> Pullback k g
-:= fun a => (f a ; (h a ; p a)).
+:= fun a => (f a ; h a ; p a).
 
 (** Symmetry of the pullback *)
 Definition equiv_pullback_symm {A B C} (f : B -> A) (g : C -> A)
@@ -44,7 +44,7 @@ Definition equiv_pullback_unit_prod (A B : Type)
 Proof.
   simple refine (equiv_adjointify _ _ _ _).
   - intros [a [b _]]; exact (a , b).
-  - intros [a b]; exact (a ; (b ; 1)).
+  - intros [a b]; exact (a ; b ; 1).
   - intros [a b]; exact 1.
   - intros [a [b p]]; simpl.
     apply (path_sigma' _ 1); simpl.

theories/Types/Record.v

@@ -60,7 +60,7 @@ Ltac issig3 build pr1 pr2 pr3 :=
                     (BuildIsEquiv
                        A B
                        (fun u => build u.1 u.2.1 u.2.2)
-                       (fun v => (pr1 v; (pr2 v; pr3 v)))
+                       (fun v => (pr1 v; pr2 v; pr3 v))
                        (fun v => let (v1, v2, v3) as v' return (build (pr1 v') (pr2 v') (pr3 v') = v') := v in 1)
                        eta2_sigma
                        (fun _ => 1))).
@@ -77,7 +77,7 @@ Ltac issig4 build pr1 pr2 pr3 pr4 :=
                     (BuildIsEquiv
                        A B
                        (fun u => build u.1 u.2.1 u.2.2.1 u.2.2.2)
-                       (fun v => (pr1 v; (pr2 v; (pr3 v; pr4 v))))
+                       (fun v => (pr1 v; pr2 v; pr3 v; pr4 v))
                        (fun v => let (v1, v2, v3, v4) as v' return (build (pr1 v') (pr2 v') (pr3 v') (pr4 v') = v') := v in 1)
                        eta3_sigma
                        (fun _ => 1))).
@@ -94,7 +94,7 @@ Ltac issig5 build pr1 pr2 pr3 pr4 pr5 :=
                     (BuildIsEquiv
                        A B
                        (fun u => build u.1 u.2.1 u.2.2.1 u.2.2.2.1 u.2.2.2.2)
-                       (fun v => (pr1 v; (pr2 v; (pr3 v; (pr4 v ; pr5 v)))))
+                       (fun v => (pr1 v; pr2 v; pr3 v; pr4 v ; pr5 v))
                        (fun v => let (v1, v2, v3, v4, v5) as v' return (build (pr1 v') (pr2 v') (pr3 v') (pr4 v') (pr5 v') = v') := v in 1)
                        (fun u => 1)
                        (fun _ => 1))).
@@ -110,7 +110,7 @@ Ltac issig6 build pr1 pr2 pr3 pr4 pr5 pr6 :=
                     (BuildIsEquiv
                        A B
                        (fun u => build u.1 u.2.1 u.2.2.1 u.2.2.2.1 u.2.2.2.2.1 u.2.2.2.2.2)
-                       (fun v => (pr1 v; (pr2 v; (pr3 v; (pr4 v ; (pr5 v ; pr6 v))))))
+                       (fun v => (pr1 v; pr2 v; pr3 v; pr4 v ; pr5 v ; pr6 v))
                        (fun v => let (v1, v2, v3, v4, v5, v6) as v' return (build (pr1 v') (pr2 v') (pr3 v') (pr4 v') (pr5 v') (pr6 v') = v') := v in 1)
                        (fun u => 1)
                        (fun _ => 1))).

theories/Types/Sigma.v

@@ -37,14 +37,14 @@ Arguments eta_sigma / .
 
 Definition eta2_sigma `{P : forall (a : A) (b : B a), Type}
            (u : sigT (fun a => sigT (P a)))
-  : (u.1; (u.2.1; u.2.2)) = u
+  : (u.1; u.2.1; u.2.2) = u
   := 1.
 
 Arguments eta2_sigma / .
 
 Definition eta3_sigma `{P : forall (a : A) (b : B a) (c : C a b), Type}
            (u : sigT (fun a => sigT (fun b => sigT (P a b))))
-  : (u.1; (u.2.1; (u.2.2.1; u.2.2.2))) = u
+  : (u.1; u.2.1; u.2.2.1; u.2.2.2) = u
   := 1.
 
 Arguments eta3_sigma / .
@@ -383,7 +383,7 @@ Definition transport_sigma_' {A : Type} {B C : A -> Type}
            {x1 x2 : A} (p : x1 = x2)
            (yzw : { y : B x1 & { z : C x1 & D x1 y z } })
 : transport (fun x => { y : B x & { z : C x & D x y z } }) p yzw
-  = (p # yzw.1 ; (p # yzw.2.1 ; transportD2 _ _ _ p yzw.1 yzw.2.1 yzw.2.2)).
+  = (p # yzw.1 ; p # yzw.2.1 ; transportD2 _ _ _ p yzw.1 yzw.2.1 yzw.2.2).
 Proof.
   destruct p. reflexivity.
 Defined.