Merge pull request #201 from peterlefanulumsdaine/housekeeping

Housekeeping

Author: benediktahrens

TypeTheory/ALV1/CwF_SplitTypeCat_Cats_Standalone.v

@@ -23,7 +23,8 @@ Main definitions:
 
 *)
 
-Require Import UniMath.Foundations.Sets.
+Require Import UniMath.Foundations.All.
+Require Import UniMath.MoreFoundations.All.
 Require Import TypeTheory.Auxiliary.CategoryTheoryImports.
 Require Import UniMath.CategoryTheory.Equivalences.CompositesAndInverses.
 Require Import TypeTheory.Auxiliary.Auxiliary.
@@ -79,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.
 
@@ -105,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').
@@ -122,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.
 
@@ -335,8 +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.
@@ -727,33 +727,33 @@ Qed.
 Definition compat_structures_category : category
   := make_category _ has_homsets_compat_structures_precategory.
 
-Definition pr1_equiv : @adj_equivalence_of_precats
+Definition pr1_equiv : @adj_equivalence_of_cats
                          compat_structures_category
                          term_fun_category
                          compat_structures_pr1_functor.
 Proof.
-  use adj_equivalence_of_precats_ff_split.
+  use adj_equivalence_of_cats_ff_split.
   - apply compat_structures_pr1_fully_faithful.
   - apply compat_structures_pr1_split_ess_surj.
 Defined.
 
-Definition pr2_equiv : @adj_equivalence_of_precats
+Definition pr2_equiv : @adj_equivalence_of_cats
                          compat_structures_category
                          qq_structure_category
                          compat_structures_pr2_functor.
 Proof.
-  use adj_equivalence_of_precats_ff_split.
+  use adj_equivalence_of_cats_ff_split.
   - apply compat_structures_pr2_fully_faithful.
   - apply compat_structures_pr2_split_ess_surj.
 Defined.
 
-Definition pr1_equiv_inv : adj_equivalence_of_precats (right_adjoint pr1_equiv).
+Definition pr1_equiv_inv : adj_equivalence_of_cats (right_adjoint pr1_equiv).
 Proof.
-  use adj_equivalence_of_precats_inv.
+  use adj_equivalence_of_cats_inv.
 Defined.
 
-Definition equiv_of_structures : adj_equivalence_of_precats _ 
-  := @comp_adj_equivalence_of_precats _ _ _ _ _ 
+Definition equiv_of_structures : adj_equivalence_of_cats _ 
+  := @comp_adj_equivalence_of_cats _ _ _ _ _ 
                                       pr1_equiv_inv pr2_equiv.
 
 Definition equiv_of_types_of_structures 

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 _ _)). }
@@ -390,7 +390,7 @@ Components of [Y : term_fun_structure X]:
 - [pp Y : TM Y --> TY X]
 - [Q Y A :  Yo (Γ ◂ A) --> TM Y]
 - [Q_pp Y A : #Yo (π A) ;; yy A = Q Y A ;; pp Y]
-- [isPullback_Q_pp Y A : isPullback _ _ _ _ (Q_pp Y A)]
+- [isPullback_Q_pp Y A : isPullback (Q_pp Y A)]
 
  See: Marcelo Fiore, slides 32–34 of _Discrete Generalised Polynomial Functors_ , from talk at ICALP 2012,
   #(<a href="http://www.cl.cam.ac.uk/~mpf23/talks/ICALP2012.pdf">link</a>)#
@@ -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 Γ) 
@@ -545,7 +545,7 @@ Components of [Z : qq_morphism_structure X]:
 
 - [qq Z f A : Γ' ◂ A[f] --> Γ ◂ A]
 - [qq_π Z f A : qq Z f A ;; π A = π _ ;; f]
-- [qq_π_Pb Z f A : isPullback _ _ _ _ (!qq_π Z f A)]
+- [qq_π_Pb Z f A : isPullback (!qq_π Z f A)]
 - [qq_id], [qq_comp]: functoriality for [qq]
 *)
 
@@ -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

@@ -4,15 +4,14 @@
   Part of the [TypeTheory] library (Ahrens, Lumsdaine, Voevodsky, 2015–present).
 *)
 
-Require Import UniMath.Foundations.Sets.
+Require Import UniMath.Foundations.All.
+Require Import UniMath.MoreFoundations.All.
 Require Import TypeTheory.Auxiliary.CategoryTheoryImports.
 
 Require Import TypeTheory.Auxiliary.Auxiliary.
 Require Import TypeTheory.ALV1.CwF_SplitTypeCat_Defs.
 Require Import TypeTheory.ALV1.CwF_SplitTypeCat_Maps.
 
-Open Scope mor_scope.
-
 
 Section Fix_Context.
 
@@ -50,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.
@@ -87,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.
@@ -105,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).
@@ -176,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.
 
@@ -228,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

@@ -11,7 +11,8 @@
 *)
 
 
-Require Import UniMath.Foundations.Sets.
+Require Import UniMath.Foundations.All.
+Require Import UniMath.MoreFoundations.All.
 Require Import TypeTheory.Auxiliary.CategoryTheoryImports.
 
 Require Import TypeTheory.Auxiliary.Auxiliary.
@@ -89,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.
 
@@ -126,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.
@@ -194,7 +195,7 @@ Proof.
   use total2_paths_f; simpl.
     apply eA.
   apply subtypePath. intro; apply homset_property.
-  simpl. eapply pathscomp0. use (pr1_transportf _ _ _ _ _ eA).
+  simpl. eapply pathscomp0. use (pr1_transportf (Ty X Γ)).
   simpl. eapply pathscomp0. apply functtransportf.
   eapply pathscomp0. eapply pathsinv0. apply idtoiso_postcompose.
   exact es.
@@ -222,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.
@@ -389,15 +390,15 @@ 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. 
       etrans. apply maponpaths, qq_π.
       etrans. apply assoc.
       etrans. apply maponpaths_2, e.
       apply id_left.
-    + use (map_into_Pb_unique _ (qq_π_Pb Z _ _  )).
+    + use (map_into_Pb_unique (qq_π_Pb Z _ _  )).
       * cbn.
         use (_ @ !e).
         etrans. apply @pathsinv0, assoc.
@@ -470,16 +471,16 @@ 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.
     + cbn.
       etrans. apply @pathsinv0, assoc.
       etrans. apply maponpaths, comp_ext_compare_π.
       apply (PullbackArrow_PullbackPr1 (make_Pullback _ _)). 
-    + apply (map_into_Pb_unique _ (qq_π_Pb Z _ _)). 
+    + apply (map_into_Pb_unique (qq_π_Pb Z _ _)).
       * cbn.
         etrans. apply @pathsinv0, assoc.
         etrans. apply maponpaths, qq_π.