Made more args of [toforallpaths] implicit

Author: peterlefanulumsdaine

TypeTheory/ALV1/CwF_SplitTypeCat_Cats_Standalone.v

@@ -80,7 +80,7 @@ Proof.
   intros Γ'; simpl in Γ'.
   unfold yoneda_objects_ob. apply funextsec; intros f.
   etrans. 
-    use (toforallpaths _ _ _ (nat_trans_ax (term_fun_mor_TM FF) _)).
+    use (toforallpaths (nat_trans_ax (term_fun_mor_TM FF) _)).
   cbn. apply maponpaths, term_fun_mor_te.
 Qed.
 
@@ -106,7 +106,7 @@ Lemma term_to_section_naturality {Y} {Y'}
   {Γ : C} (t : Tm Y Γ) (A := (pp Y : nat_trans _ _) _ t)
   : pr1 (term_to_section ((term_fun_mor_TM FY : nat_trans _ _) _ t))
   = pr1 (term_to_section t) 
-   ;; Δ (!toforallpaths _ _ _ (nat_trans_eq_pointwise (term_fun_mor_pp FY) Γ) t).
+   ;; Δ (!toforallpaths (nat_trans_eq_pointwise (term_fun_mor_pp FY) Γ) t).
 Proof.
   set (t' := (term_fun_mor_TM FY : nat_trans _ _) _ t).
   set (A' := (pp Y' : nat_trans _ _) _ t').
@@ -123,7 +123,7 @@ Proof.
     etrans. apply Q_comp_ext_compare.
     etrans. apply @pathsinv0.
       set (H1 := nat_trans_eq_pointwise (term_fun_mor_Q FY A) Γ).
-      exact (toforallpaths _ _ _ H1 _).
+      exact (toforallpaths H1 _).
     cbn. apply maponpaths. apply term_to_section_recover.
 Qed.
 
@@ -336,7 +336,7 @@ Proof.
   - etrans. apply qq_π.
     apply pathsinv0, qq_π.
   - etrans. cbn. apply maponpaths, @pathsinv0, (term_fun_mor_te FY).
-    etrans. use (toforallpaths _ _ _ (!nat_trans_ax (term_fun_mor_TM _) _)).
+    etrans. use (toforallpaths (!nat_trans_ax (term_fun_mor_TM _) _)).
     etrans. cbn. apply maponpaths, @pathsinv0, W.
     etrans. apply term_fun_mor_te.
     apply W'.
@@ -601,8 +601,8 @@ Proof.
     apply funextsec; intros A.
     etrans. apply transportf_pshf.
     etrans.
-      refine (toforallpaths _ _ _ _ (te _ _)).
-      refine (toforallpaths _ _ _ _ _).
+      refine (toforallpaths _ (te _ _)).
+      refine (toforallpaths _ _).
       apply maponpaths, idtoiso_iso_to_TM_eq.
     apply term_fun_mor_te.
 Qed.

TypeTheory/ALV1/CwF_SplitTypeCat_Defs.v

@@ -210,9 +210,9 @@ Section Obj_Ext_Structures_Disp_Utility_Lemmas.
   Proof.
     etrans.
     { unfold φ. apply maponpaths.
-      refine (toforallpaths _ _ _ _ _).
+      refine (toforallpaths _ _).
       etrans.
-      { refine (toforallpaths _ _ _ _ _); refine (transportf_forall _ _ _). }
+      { refine (toforallpaths _ _); refine (transportf_forall _ _ _). }
       simpl. refine (transportf_forall _ _ _).
     } 
     etrans. { use (pr1_transportf (nat_trans _ _)). }
@@ -494,7 +494,7 @@ Proof.
   set (Pb := isPullback_preShv_to_pointwise (isPullback_Q_pp Y A) Γ).
   simpl in Pb.
   apply (pullback_HSET_univprop_elements _ Pb).
-  exact (toforallpaths _ _ _ (functor_id (TY X) _) A).
+  exact (toforallpaths (functor_id (TY X) _) A).
 Qed.
 
 Lemma term_to_section {Y : term_fun_structure} {Γ:C} (t : Tm Y Γ) 
@@ -597,12 +597,12 @@ Definition qq_morphism_axioms (Z : qq_morphism_data) : UU
   := 
     (∏ Γ A,
     qq Z (identity Γ) A
-    = Δ (toforallpaths _ _ _ (functor_id (TY X) _ ) _ ))
+    = Δ (toforallpaths (functor_id (TY X) _ ) _ ))
   ×
     (∏ Γ Γ' Γ'' (f : C⟦Γ', Γ⟧) (g : C ⟦Γ'', Γ'⟧) (A : (TY X:functor _ _ ) Γ : hSet),
     qq Z (g ;; f) A
     = Δ
-           (toforallpaths _ _ _ (functor_comp (TY X) _ _) A)
+           (toforallpaths (functor_comp (TY X) _ _) A)
       ;; qq Z g (A [f]) 
       ;; qq Z f A).
 
@@ -618,14 +618,14 @@ Coercion qq_morphism_data_from_structure :
 Definition qq_id (Z : qq_morphism_structure)
     {Γ} (A : Ty X Γ)
   : qq Z (identity Γ) A
-  = Δ (toforallpaths _ _ _ (functor_id (TY X) _ ) _ )
+  = Δ (toforallpaths (functor_id (TY X) _ ) _ )
 := pr1 (pr2 Z) _ _.
 
 Definition qq_comp (Z : qq_morphism_structure)
     {Γ Γ' Γ'' : C}
     (f : C ⟦ Γ', Γ ⟧) (g : C ⟦ Γ'', Γ' ⟧) (A : Ty X Γ)
   : qq Z (g ;; f) A
-  = Δ (toforallpaths _ _ _ (functor_comp (TY X) _ _) A)
+  = Δ (toforallpaths (functor_comp (TY X) _ _) A)
     ;; qq Z g (A [f]) ;; qq Z f A
 := pr2 (pr2 Z) _ _ _ _ _ _.
 

TypeTheory/ALV1/CwF_SplitTypeCat_Equivalence.v

@@ -49,8 +49,8 @@ Proof.
   apply funextsec; intros [A [s e]].
   unfold canonical_TM_to_given_data; cbn.
   etrans. apply maponpaths, (pr2 Y).
-  etrans. apply (toforallpaths _ _ _ (!functor_comp (TM Y) _ _ ) _).
-  etrans. 2: { apply (toforallpaths _ _ _ (functor_comp (TM Y) _ _ ) _). }
+  etrans. apply (toforallpaths (!functor_comp (TM Y) _ _ ) _).
+  etrans. 2: { apply (toforallpaths (functor_comp (TM Y) _ _ ) _). }
   apply maponpaths_2. 
   apply (@PullbackArrow_PullbackPr2 C _ _ _ _ _ (make_Pullback _ _)).
 Qed.
@@ -86,11 +86,11 @@ Proof.
   apply nat_trans_eq. apply homset_property.
   intros Γ; simpl in Γ. apply funextsec; intros [A [s e]].
   cbn. unfold canonical_TM_to_given_data.
-  etrans. apply (toforallpaths _ _ _ (nat_trans_ax (pp Y) s)). 
+  etrans. apply (toforallpaths (nat_trans_ax (pp Y) s)). 
   etrans. cbn. apply maponpaths, pp_te.
-  etrans. apply (toforallpaths _ _ _ (!functor_comp (TY X) _ _) _).
+  etrans. apply (toforallpaths (!functor_comp (TY X) _ _) _).
   etrans. apply maponpaths_2, e.
-  apply (toforallpaths _ _ _ (functor_id (TY X) _ ) _).
+  apply (toforallpaths (functor_id (TY X) _ ) _).
 Qed.
 
 (* Functions between sets [f : X <--> Y : g] are inverse iff they are _adjoint_, in that [ f x = y <-> x = f y ] for all x, y.
@@ -104,9 +104,8 @@ Proof.
   intros H.
   (* This [assert] is to enable the [destruct eA] below. *)
   assert (eA : (pp Y : nat_trans _ _) _ t = A). {
-    etrans. apply maponpaths, (!H).
-    use (toforallpaths _ _ _ 
-      (nat_trans_eq_pointwise pp_canonical_TM_to_given _)).
+    etrans. { apply maponpaths, (!H). }
+    use (toforallpaths (nat_trans_eq_pointwise pp_canonical_TM_to_given _)).
   }
   use total2_paths_f.
   exact (!eA).
@@ -175,17 +174,17 @@ Lemma canonical_TM_to_given_te {Γ:C} A
 Proof.
   cbn. unfold canonical_TM_to_given_data. cbn.
   etrans. apply maponpaths, (pr2 Y).
-  etrans. use (toforallpaths _ _ _ (!functor_comp (TM Y) _ _ )).
+  etrans. use (toforallpaths (!functor_comp (TM Y) _ _ )).
   etrans. apply maponpaths_2; cbn.
     apply (PullbackArrow_PullbackPr2 (make_Pullback _ _)). 
-  apply (toforallpaths _ _ _ (functor_id (TM Y) _) _).
+  apply (toforallpaths (functor_id (TM Y) _) _).
 Qed.
 
 Lemma given_TM_to_canonical_te {Γ:C} A
   : (given_TM_to_canonical : nat_trans _ _) (Γ ◂ A) (te Y A) = (te_from_qq Z A).
 Proof.
   etrans.
-  2: { exact (toforallpaths _ _ _ (canonical_to_given_to_canonical _) _). }
+  2: { exact (toforallpaths (canonical_to_given_to_canonical _) _). }
   cbn. apply maponpaths, @pathsinv0, canonical_TM_to_given_te.
 Qed.
 
@@ -227,10 +226,10 @@ Proof.
       etrans. apply transportf_isotoid_pshf.
       cbn. unfold canonical_TM_to_given_data. cbn.
       etrans. apply maponpaths, YH.
-      etrans. use (toforallpaths _ _ _ (!functor_comp tm _ _ )).
+      etrans. use (toforallpaths (!functor_comp tm _ _ )).
       etrans. apply maponpaths_2; cbn.
         apply (PullbackArrow_PullbackPr2 (make_Pullback _ _)). 
-      apply (toforallpaths _ _ _ (functor_id tm _) _).
+      apply (toforallpaths (functor_id tm _) _).
 Defined.
 
 (** * Every compatible q-morphism structure is equal to the canonical one *)

TypeTheory/ALV1/CwF_SplitTypeCat_Maps.v

@@ -90,12 +90,12 @@ Proof.
     intros Γ''. cbn. unfold yoneda_objects_ob, yoneda_morphisms_data.
     apply funextsec; intros g.
     etrans. apply maponpaths, H.
-    use (toforallpaths _ _ _ (!functor_comp (TM Y) _ _)).
+    use (toforallpaths (!functor_comp (TM Y) _ _)).
   - assert (H' := nat_trans_eq_pointwise H); clear H.
-    assert (H'' := toforallpaths _ _ _ (H' _) (identity _)); clear H'.
+    assert (H'' := toforallpaths (H' _) (identity _)); clear H'.
     cbn in H''; unfold yoneda_morphisms_data in H''.
     refine (_ @ H'' @ _).
-    + use (toforallpaths _ _ _ (!functor_id (TM Y) _)).
+    + use (toforallpaths (!functor_id (TM Y) _)).
     + apply maponpaths_2, id_left.
 Qed.
 
@@ -127,7 +127,7 @@ Proof.
     etrans. 2: { apply id_left. }
     apply maponpaths_2.
     exact (pr2 (term_to_section _)).
-  - etrans. refine (!toforallpaths _ _ _ (nat_trans_eq_pointwise (W' _ _ _ _) _) _).
+  - etrans. refine (!toforallpaths (nat_trans_eq_pointwise (W' _ _ _ _) _) _).
     etrans. apply Q_comp_ext_compare.
     apply term_to_section_recover.
 Qed.
@@ -223,14 +223,14 @@ Proof.
   split; [unfold functor_idax | unfold functor_compax].
   - intro Γ; apply funextsec; intro t. destruct t as [A [s e]]; cbn.
     use tm_from_qq_eq; simpl.
-    + exact (toforallpaths _ _ _ (functor_id (TY X) _ ) A).
+    + exact (toforallpaths (functor_id (TY X) _ ) A).
     + etrans. apply maponpaths, @pathsinv0, qq_id.
       etrans. apply (PullbackArrow_PullbackPr2 (make_Pullback _ _)). 
       apply id_left.
   - intros Γ Γ' Γ'' f g; apply funextsec; intro t.
     destruct t as [A [s e]]; cbn in *.
     use tm_from_qq_eq; simpl.
-    + exact (toforallpaths _ _ _ (functor_comp (TY X) _ _) A).
+    + exact (toforallpaths (functor_comp (TY X) _ _) A).
     + {
       apply PullbackArrowUnique; cbn.
       - rewrite <- assoc.
@@ -390,7 +390,7 @@ Proof.
     use tm_from_qq_eq. cbn. 
     + etrans.
         apply @pathsinv0.
-        use (toforallpaths _ _ _ (functor_comp (TY X) _ _ ) A).
+        use (toforallpaths (functor_comp (TY X) _ _ ) A).
       apply maponpaths_2.
       cbn.
       etrans. apply @pathsinv0, assoc. 
@@ -471,8 +471,8 @@ Proof.
   intros ? ? ? ?.
   (* TODO: use [tm_from_qq_eq'] here *)
   use tm_from_qq_eq; simpl.
-  - etrans. apply (toforallpaths _ _ _ (!functor_comp (TY X) _ _ ) A).
-    etrans. 2: { apply (toforallpaths _ _ _ (functor_comp (TY X) _ _ ) A). }
+  - etrans. apply (toforallpaths (!functor_comp (TY X) _ _ ) A).
+    etrans. 2: { apply (toforallpaths (functor_comp (TY X) _ _ ) A). }
     apply maponpaths_2; cbn.
     apply @pathsinv0, qq_π.
   - apply PullbackArrowUnique.

TypeTheory/ALV1/CwF_def.v

@@ -137,11 +137,11 @@ Lemma cwf_square_comm_converse {Γ : C} {A : Ty pp Γ : hSet}
   : ((pp : _ --> _) : nat_trans _ _) _ t = # (Ty pp) π A.
 Proof.
   etrans.
-    apply maponpaths, @pathsinv0.
-    apply (toforallpaths _ _ _ (functor_id (Tm pp) _)).
+  { apply maponpaths, pathsinv0, (toforallpaths (functor_id (Tm pp) _)). }
   etrans. 
-    assert (e' := nat_trans_eq_pointwise e ΓA); clear e; cbn in e'.
-    use (toforallpaths _ _ _ (!e') (identity _)).
+  { assert (e' := nat_trans_eq_pointwise e ΓA); clear e; cbn in e'.
+    refine (toforallpaths (!e') (identity _)).
+  }
   unfold yoneda_morphisms_data.
   apply maponpaths_2, id_left.
 Qed.
@@ -215,8 +215,8 @@ Proof.
     rewrite id_right.
     etrans. { apply yoneda_postcompose. }
     etrans. {
-      refine (toforallpaths _ _ _ _ (identity _)). 
-      refine (toforallpaths _ _ _ _ _). 
+      refine (toforallpaths _ (identity _)). 
+      refine (toforallpaths _ _). 
       apply maponpaths,
         (PullbackArrow_PullbackPr1 (make_Pullback _ (pr22 x))).
     }

TypeTheory/ALV2/CwF_Cats.v

@@ -283,7 +283,7 @@ Section CwF_structure_cat.
         set (A' := (F_TY : nat_trans _ _) _ A).
         unfold cwf_structure_mor_term_axiom in f3, g3. simpl in f3, g3.
         refine (maponpaths _ (f3 Γ A) @ _).
-        etrans. apply (toforallpaths _ _ _ (nat_trans_ax F_TM' _)).
+        etrans. apply (toforallpaths (nat_trans_ax F_TM' _)).
         refine (maponpaths _ (g3 Γ A') @ _).
         rewrite <- compose_ap, <- (functor_comp (TM Z)).
         apply idpath.

TypeTheory/ALV2/CwF_SplitTypeCat_Cats.v

@@ -155,9 +155,9 @@ Proof.
 (* Insert [cbn] to see what’s actually happening; removed for compile speed. *)
   unfold yoneda_objects_ob. apply funextsec; intros f.
   etrans. 
-    use (toforallpaths _ _ _ (nat_trans_ax (term_fun_mor_TM FF) _)).
+    use (toforallpaths (nat_trans_ax (term_fun_mor_TM FF) _)).
   etrans. cbn. apply maponpaths, term_fun_mor_te.
-  use (toforallpaths _ _ _ (!functor_comp (TM Y') _ _ )).
+  use (toforallpaths (!functor_comp (TM Y') _ _ )).
 Qed.
 
 (* TODO: inline in [isaprop_term_fun_mor]? *)
@@ -182,7 +182,7 @@ Lemma term_to_section_naturality {X X'} {Y} {Y'}
   {Γ : C} (t : Tm Y Γ) (A := (pp Y : nat_trans _ _) _ t)
   : pr1 (term_to_section ((term_fun_mor_TM FY : nat_trans _ _) _ t))
   = pr1 (term_to_section t) ;; φ F _
-   ;; Δ (!toforallpaths _ _ _ (nat_trans_eq_pointwise (term_fun_mor_pp FY) Γ) t).
+   ;; Δ (!toforallpaths (nat_trans_eq_pointwise (term_fun_mor_pp FY) Γ) t).
 Proof.
   set (t' := (term_fun_mor_TM FY : nat_trans _ _) _ t).
   set (A' := (pp Y' : nat_trans _ _) _ t').
@@ -202,7 +202,7 @@ Proof.
     etrans. apply Q_comp_ext_compare.
     etrans. apply @pathsinv0.
       set (H1 := nat_trans_eq_pointwise (term_fun_mor_Q FY A) Γ).
-      exact (toforallpaths _ _ _ H1 _).
+      exact (toforallpaths H1 _).
     cbn. apply maponpaths. apply term_to_section_recover.
 Qed.
 
@@ -249,7 +249,7 @@ Proof.
     exists (identity _). apply tpair.
     + etrans. apply id_left. apply pathsinv0, id_right.
     + intros Γ A; cbn.
-      use (toforallpaths _ _ _ (!functor_id (TM _) _)).
+      use (toforallpaths (!functor_id (TM _) _)).
   - intros X0 X1 X2 F G Y0 Y1 Y2 FF GG.
     exists (term_fun_mor_TM FF ;; term_fun_mor_TM GG). apply tpair.
     + etrans. apply @pathsinv0. apply assoc.
@@ -259,10 +259,10 @@ Proof.
       apply pathsinv0. apply assoc.
     + intros Γ A.
       etrans. cbn. apply maponpaths, term_fun_mor_te.
-      etrans. use (toforallpaths _ _ _
+      etrans. use (toforallpaths
                         (nat_trans_ax (term_fun_mor_TM _) _)).
       etrans. cbn. apply maponpaths, term_fun_mor_te.
-      use (toforallpaths _ _ _ (!functor_comp (TM _) _ _)).
+      use (toforallpaths (!functor_comp (TM _) _ _)).
 Defined.
 
 Definition term_fun_data : disp_cat_data (obj_ext_cat C)

TypeTheory/ALV2/CwF_SplitTypeCat_Equiv_Cats.v

@@ -140,7 +140,7 @@ Lemma comp_ext_compare_te
   : # (TM Y : functor _ _) (Δ e) (te Y A') = te Y A.
 Proof.
   destruct e; cbn.
-  exact (toforallpaths _ _ _ (functor_id (TM _) _) _). 
+  exact (toforallpaths (functor_id (TM _) _) _). 
 Qed.
 
 Lemma qq_from_term_mor {X X' : obj_ext_cat C} {F : X --> X'}
@@ -166,16 +166,16 @@ Proof.
     etrans. apply @pathsinv0, assoc.
     etrans. apply maponpaths. apply comp_ext_compare_π.
     apply obj_ext_mor_ax.
-  - etrans. exact (toforallpaths _ _ _ (functor_comp (TM _) _ _) _).
+  - etrans. exact (toforallpaths (functor_comp (TM _) _ _) _).
     etrans. cbn. apply maponpaths, @pathsinv0, (term_fun_mor_te FY).
-    etrans. use (toforallpaths _ _ _
+    etrans. use (toforallpaths
                       (!nat_trans_ax (term_fun_mor_TM _) _)).
     etrans. cbn. apply maponpaths, @pathsinv0, W.
     etrans. apply term_fun_mor_te.
     apply pathsinv0.
-    etrans. exact (toforallpaths _ _ _ (functor_comp (TM _) _ _) _).
+    etrans. exact (toforallpaths (functor_comp (TM _) _ _) _).
     etrans. cbn. apply maponpaths, @pathsinv0, W'.
-    etrans. exact (toforallpaths _ _ _ (functor_comp (TM _) _ _) _).
+    etrans. exact (toforallpaths (functor_comp (TM _) _ _) _).
     cbn. apply maponpaths. 
     apply comp_ext_compare_te.
 Time Qed.
@@ -239,7 +239,7 @@ Proof.
   intros Γ Γ' f; cbn in Γ, Γ', f.
   apply funextsec; intros [A [s e]].
   use tm_from_qq_eq.
-  - cbn. exact (toforallpaths _ _ _
+  - cbn. exact (toforallpaths
                   (nat_trans_ax (obj_ext_mor_TY _) _) _).
   - cbn. apply PullbackArrowUnique. 
     + etrans. cbn. apply @pathsinv0, assoc.
@@ -286,9 +286,9 @@ Proof.
   use tm_from_qq_eq_reindex.
   - cbn.
   (* Putting these equalities under [abstract] shaves a couple of seconds off the overall Qed time, but makes the proof script rather less readable. *) 
-    etrans. 2: { exact (toforallpaths _ _ _ (functor_comp (TY _) _ _) _). }
+    etrans. 2: { exact (toforallpaths (functor_comp (TY _) _ _) _). }
     etrans. 2: { cbn. apply maponpaths_2, @pathsinv0, obj_ext_mor_ax. }
-    exact (toforallpaths _ _ _ (nat_trans_ax (obj_ext_mor_TY F) _) _).
+    exact (toforallpaths (nat_trans_ax (obj_ext_mor_TY F) _) _).
   - etrans. 2: { apply @pathsinv0, 
         (postCompWithPullbackArrow _ _ _ _ (make_Pullback _ _)). }
     apply PullbackArrowUnique.
@@ -364,7 +364,7 @@ Proof.
     cbn.
     etrans. apply maponpaths, maponpaths, given_TM_to_canonical_te.
     etrans. apply maponpaths, (tm_from_qq_mor_te FZ).
-    etrans. apply (toforallpaths _ _ _
+    etrans. apply (toforallpaths
                      (nat_trans_ax (canonical_TM_to_given _ _ (_,,_)) _) _).
     cbn. apply maponpaths. apply (canonical_TM_to_given_te _ _ (_,,_)).
 Defined.

TypeTheory/ALV2/CwF_SplitTypeCat_Univalent_Cats.v

@@ -262,11 +262,11 @@ Proof.
     apply funextsec; intros A.
     etrans. apply transportf_pshf.
     etrans.
-      refine (toforallpaths _ _ _ _ (te _ _)).
-      refine (toforallpaths _ _ _ _ _).
+      refine (toforallpaths _ (te _ _)).
+      refine (toforallpaths _ _).
       apply maponpaths, idtoiso_iso_disp_to_TM_eq.
     etrans. apply term_fun_mor_te.
-    exact (toforallpaths _ _ _ (functor_id (TM _) _) _).
+    exact (toforallpaths (functor_id (TM _) _) _).
 Qed.
 
 Theorem is_univalent_term_fun_structure