Merge pull request #192 from rmatthes/beautifyisos

repair work to accommodate PR #1359 for UniMath

Author: benediktahrens

TypeTheory/ALV1/RelativeUniverses.v

@@ -862,7 +862,7 @@ Proof.
       rewrite functor_comp.
       repeat rewrite assoc. apply maponpaths_2.
       apply pathsinv0. rewrite <- assoc. rewrite <- assoc.
-      apply (iso_inv_to_left D' _ _ _ (αpwiso Xf )).
+      apply (iso_inv_to_left (C:=D') _ _ _ (αpwiso Xf )).
       cbn. unfold precomp_with. rewrite id_right.
       assert (XR := nat_trans_ax α').
       apply pathsinv0. 

TypeTheory/Auxiliary/Auxiliary.v

@@ -1129,7 +1129,7 @@ Lemma commuting_square_transfer_iso {C : precategory}
    -> p1' ;; f' = p2' ;; g'.
 Proof.
   intro H.
-  refine (pre_comp_with_iso_is_inj _ _ _ _ i_d _ _ _ _).
+  refine (pre_comp_with_iso_is_inj _ _ _ i_d _ _ _ _).
   exact (pr2 i_d).  (* TODO: access function [is_iso_from_iso]? *)
   rewrite 2 assoc.
   rewrite <- i_p1, <- i_p2.
@@ -1163,7 +1163,7 @@ Proof.
       + exact (h ;; iso_inv_from_iso i_b).
       + exact (k ;; iso_inv_from_iso i_c).
       + abstract (
-          apply (post_comp_with_iso_is_inj _ _ _ i_a (pr2 _));
+          apply (post_comp_with_iso_is_inj _ _ i_a (pr2 _));
             (* TODO: access function for isos! *)
           repeat rewrite <- assoc;
           rewrite i_f, i_g;
@@ -1193,17 +1193,17 @@ Proof.
     apply subtypePath.
       intro; apply isapropdirprod; apply homset_property.
     cbn.
-    apply (post_comp_with_iso_is_inj _ _ _ (iso_inv_from_iso i_d) (pr2 _)).
+    apply (post_comp_with_iso_is_inj _ _ (iso_inv_from_iso i_d) (pr2 _)).
     eapply @pathscomp0.
     2: { rewrite <- assoc. cbn. rewrite iso_inv_after_iso. eapply pathsinv0, id_right. }
     apply PullbackArrowUnique; cbn.
-    + apply (post_comp_with_iso_is_inj _ _ _ i_b (pr2 _)).
+    + apply (post_comp_with_iso_is_inj _ _ i_b (pr2 _)).
       repeat rewrite <- assoc.
       rewrite i_p1, iso_after_iso_inv, id_right.
       eapply @pathscomp0.
         apply maponpaths. rewrite assoc, iso_after_iso_inv. apply id_left.
       apply (pr1 (pr2 hk')).
-    + apply (post_comp_with_iso_is_inj _ _ _ i_c (pr2 _)).
+    + apply (post_comp_with_iso_is_inj _ _ i_c (pr2 _)).
       repeat rewrite <- assoc.
       rewrite i_p2, iso_after_iso_inv, id_right.
       eapply @pathscomp0.

TypeTheory/Csystems/lCsystems.v

@@ -539,7 +539,7 @@ Proof.
     assert (e: f_star gt0 (ftf g2) = f_star (C0ax5a gt0 f) g1)
     by exact (! maponpaths (f_star gt0) pbeq @ ! C0ax7a gt0 f g1).
     apply (eq_par_arrow_cor_objirr (isaset_ob CC) _ _ (pnX 1) e).
-  - apply (pre_comp_with_iso_is_inj _ _ _ _ (C0eiso gt0 (ftf g2))).
+  - apply (pre_comp_with_iso_is_inj _ _ _ (C0eiso gt0 (ftf g2))).
     { apply iso_is_iso. }
     apply pathsinv0.
     etrans.

TypeTheory/OtherDefs/TypeCat_to_CwF_Pitts.v

@@ -353,7 +353,7 @@ Proof.
       = (q_typecat (reind_typecat A (dpr_typecat A)) (a;; q_typecat A γ))
           ;; (q_typecat A (dpr_typecat A))).
 
-      unshelve refine (pre_comp_with_iso_is_inj _ _ _ _ _ _ _ _ _).
+      unshelve refine (pre_comp_with_iso_is_inj _ _ _ _ _ _ _ _).
       Focus 4.
         etrans. Focus 2. symmetry; apply assoc.
         etrans. Focus 2. apply (@q_q_typecat (((CC,,homs_sets),,pr1 C),,pr2 C)).