Adapting to UniMath refactoring precategories: Got all Initiality compiling again

Author: peterlefanulumsdaine

TypeTheory/Initiality/SplitTypeCat_Contextual.v

@@ -12,13 +12,13 @@ Require Import TypeTheory.Initiality.SplitTypeCat_General.
 (* These two lemmas should be upstreamed to UniMath/CategoryTheory/limits/terminal.v and initial.v *)
 Section upstream.
 
-  Lemma isaprop_isTerminal {C : precategory} (x : C) : isaprop (isTerminal C x).
+  Lemma isaprop_isTerminal {C : category} (x : C) : isaprop (isTerminal C x).
   Proof.
     repeat (apply impred; intro).
     apply isapropiscontr.
   Qed.
 
-  Lemma isaprop_isInitial {C : precategory} (x : C) : isaprop (isInitial C x).
+  Lemma isaprop_isInitial {C : category} (x : C) : isaprop (isInitial C x).
   Proof.
     repeat (apply impred; intro).
     apply isapropiscontr.

TypeTheory/Initiality/SplitTypeCat_General.v

@@ -11,7 +11,7 @@ Require Import TypeTheory.Auxiliary.CategoryTheoryImports.
 Require Import TypeTheory.Auxiliary.Auxiliary.
 Require Import TypeTheory.ALV1.TypeCat.
 
-(* This should be upstreamed *)
+(* TODO: upstream? *)
 Arguments nat_trans_ax {C C'} {F F'} a {x x'} f.
 
 Local Open Scope cat.
@@ -161,7 +161,7 @@ Section Terms.
     : reind_tm f a ;; q_typecat A f = f ;; a.
   Proof.
     simpl.
-    set (pb := make_Pullback _ _ _ _ _ _ _).
+    set (pb := make_Pullback _ _).
     now rewrite (PullbackArrow_PullbackPr2 pb).
   Qed.
 
@@ -230,9 +230,9 @@ Section Terms.
       = tm_transportb (reind_id_type_typecat _ _) a.
   Proof.
     apply subtypePath; [ intros x; apply homset_property|]; simpl.
-    set (pb := make_Pullback _ _ _ _ _ _ _).
+    set (pb := make_Pullback _ _).
     (* Why is there a ' version of this lemma??? *)
-    apply pathsinv0, (PullbackArrowUnique' _ _ pb).
+    apply pathsinv0, (PullbackArrowUnique' _ _ _ pb).
     - rewrite <-assoc.
       etrans; [eapply maponpaths, idtoiso_dpr_typecat|].
       exact (pr2 a).
@@ -257,10 +257,10 @@ Section Terms.
           (reind_tm g (reind_tm f a)).
   Proof.
     apply subtypePath; [ intros x; apply homset_property|]; simpl.
-    set (pb := make_Pullback _ _ _ _ _ _ _).
-    set (pb' := make_Pullback _ _ _ _ _ _ _).
-    set (pb'' := make_Pullback _ _ _ _ _ _ _).
-    apply pathsinv0, (PullbackArrowUnique' _ _ pb).
+    set (pb := make_Pullback _ _).
+    set (pb' := make_Pullback _ _).
+    set (pb'' := make_Pullback _ _).
+    apply pathsinv0, (PullbackArrowUnique' _ _ _ pb).
     - rewrite <- assoc.
       etrans; [eapply maponpaths, idtoiso_dpr_typecat|].
       apply (PullbackArrow_PullbackPr1 pb').
@@ -329,8 +329,8 @@ Section Terms.
     apply pathsinv0, PullbackArrowUnique.
     { apply (section_property (tm_transportb _ _)). }
     apply pathsinv0.
-    etrans. { refine (postCompWithPullbackArrow _ _ _
-                                       (make_Pullback _ _ _ _ _ _ _) _ _ _). }
+    etrans. { refine (postCompWithPullbackArrow _ _ _ _
+                                       (make_Pullback _ _) _ _ _). }
     apply pathsinv0, PullbackArrowUnique; cbn; refine (_ @ ! id_right _).
     - rewrite <- assoc.
       etrans. { apply maponpaths, dpr_q_typecat. }
@@ -378,7 +378,7 @@ Section Terms.
     + now induction e; rewrite <-assoc, id_left.
     + unfold map_into_Pb.
       set (pb := Auxiliary.Pbb _ _ _ _ _ _ _ _ _ _ _).
-      rewrite <-assoc, (postCompWithPullbackArrow _ _ _ pb).
+      rewrite <-assoc, (postCompWithPullbackArrow _ _ _ _ pb).
       apply PullbackArrowUnique; cbn.
     - rewrite <-!assoc, dpr_q_typecat; induction e.
       now rewrite id_left, assoc, af, id_left, id_right.
@@ -505,4 +505,4 @@ Section Types_with_Terms.
       apply tm_transportf_irrelevant.
   Qed.
 
-End Types_with_Terms.
+End Types_with_Terms.

TypeTheory/Initiality/SplitTypeCat_Maps.v

@@ -262,7 +262,7 @@ Section Derived_Actions.
     reind_tm (# F f) (fmap_tm F a).
   Proof.
     apply paths_tm, PullbackArrowUnique; cbn; simpl;
-      set (pb := make_Pullback _ _ _ _ _ _ _); rewrite <-!assoc.
+      set (pb := make_Pullback _ _); rewrite <-!assoc.
     - etrans; [apply maponpaths, maponpaths, comp_ext_compare_dpr_typecat|].
       etrans; [apply maponpaths, (!typecat_mor_triangle F (A ⦃f⦄))|].
       now rewrite <- functor_comp, (PullbackArrow_PullbackPr1 pb), functor_id.
@@ -328,8 +328,7 @@ Section Derived_Actions.
         etrans. { apply assoc. }
         etrans. { apply maponpaths_2, assoc. }
         etrans. { apply maponpaths_2, maponpaths_2.
-                  refine (PullbackArrow_PullbackPr2
-                            (make_Pullback _ _ _ _ _ _ _) _ _ _ _). }
+          refine (PullbackArrow_PullbackPr2 (make_Pullback _ _) _ _ _ _). }
         simpl pr1.
         etrans. { apply maponpaths_2, maponpaths_2, assoc. }
         etrans. { apply pathsinv0, assoc. }
@@ -343,8 +342,7 @@ Section Derived_Actions.
           etrans. { apply pathsinv0, functor_comp. }
           etrans.
           { apply maponpaths.
-            refine (PullbackArrow_PullbackPr2
-                            (make_Pullback _ _ _ _ _ _ _) _ _ _ _).
+            refine (PullbackArrow_PullbackPr2 (make_Pullback _ _) _ _ _ _).
           }
           apply functor_id.
         }