Refactored precategories + has_homsets to categories in a few places

Author: peterlefanulumsdaine

TypeTheory/ALV1/Transport_along_Equivs.v

@@ -143,8 +143,7 @@ Proof.
   set (XTT := ff_Fop_precomp).
   specialize (T XTT).
   set (XR := iso_from_iso_with_postcomp).
-  apply (XR _ _ _ (functor_category_has_homsets _ _ _ )
-                  (functor_category_has_homsets _ _ _ )  _ _ _ XTT).
+  apply (XR _ _ _ _ _ _ XTT).
   eapply iso_comp.
      apply functor_assoc_iso.
   eapply iso_comp.

TypeTheory/Auxiliary/Auxiliary.v

@@ -499,8 +499,8 @@ Proof.
       apply id_left.
 Defined.
 
-Definition iso_ob {C D : precategory} (hsD : has_homsets D)
-          {F G : functor C D} (a : iso (C:= [C, D, hsD]) F G)
+Definition iso_ob {C : precategory} {D : category}
+          {F G : functor C D} (a : iso (C:= [C, D]) F G)
   : ∏ c, iso (F c) (G c).
 Proof.
   intro c.
@@ -523,9 +523,9 @@ Proof.
     + cbn. destruct p as [[a b] f].
       apply pathsdirprod; cbn. 
       * apply (isotoid _ isC). 
-        apply iso_inv_from_iso. apply (iso_ob _ eta).
+        apply iso_inv_from_iso. apply (iso_ob eta).
       * apply (isotoid _ isC).
-        apply iso_inv_from_iso. apply (iso_ob _ eta).
+        apply iso_inv_from_iso. apply (iso_ob eta).
     + cbn. destruct p as [[a b] f]. cbn in *.
       etrans. apply (transportf_pair (λ x : C × C, C ⟦ pr2 x, pr1 x ⟧)).
       cbn.
@@ -544,9 +544,9 @@ Proof.
     + cbn. destruct p as [[a b] f].
       apply pathsdirprod; cbn. 
       * apply (isotoid _ isD). 
-        apply (iso_ob _ eps).
+        apply (iso_ob eps).
       * apply (isotoid _ isD).
-        apply (iso_ob _ eps).
+        apply (iso_ob eps).
     + cbn. destruct p as [[a b] f]. cbn in *.
       etrans. apply (transportf_pair (λ x : D × D, D ⟦ pr2 x, pr1 x ⟧)).
       cbn.
@@ -834,18 +834,6 @@ Qed.
 
 Coercion univalent_category_is_univalent : univalent_category >-> is_univalent.
 
-(* TODO: raise issue in [CategoryTheory.Categories]: delete [category_has_homsets], since now redundant with [homset_property], since [category] coerces to [category]. *)
-
-(* TODO: raise issue: should the [HSET] provided be this by default, and current [HSET] be renamed to [HSET_precategory]? *)
-(* This def exists in UniMath/UniMath
-Definition HSET_univalent_category : univalent_category.
-Proof.
-  exists HSET; split.
-  - apply is_univalent_HSET.
-  - apply has_homsets_HSET.
-Defined.
- *)
-
 Definition functor_univalent_category (C : precategory) (D : univalent_category)
   : univalent_category.
 Proof.
@@ -884,7 +872,7 @@ Lemma yy_comp_nat_trans {C : category}
   : yy v ;; p = yy ((p : nat_trans _ _ )  _ v).
 Proof.
   apply nat_trans_eq.
-  - apply has_homsets_HSET.
+  - apply homset_property.
   - intro c. simpl. 
     apply funextsec. intro f. cbn.
     assert (XR := toforallpaths _ _ _ (nat_trans_ax p _ _ f) v ).
@@ -1000,9 +988,8 @@ Proof.
   apply id_right.
 Defined.
 
-Definition nat_iso_from_pointwise_iso (D E : precategory)
-  (hsE : has_homsets E)
-  (F G : [D, E, hsE])
+Definition nat_iso_from_pointwise_iso (D : precategory) (E : category)
+  (F G : [D, E])
   (a : ∏ d, iso ((F : functor _ _) d) ((G : functor _ _) d))
   (H : is_nat_trans _ _ a)
   : iso F G.
@@ -1014,12 +1001,12 @@ Proof.
   - intro d. apply (pr2 (a d)).
 Defined.
 
-Lemma iso_from_iso_with_postcomp (D E E' : precategory) hsE hsE'
+Lemma iso_from_iso_with_postcomp (D E E' : category)
   (F G : functor D E) (H : functor E E')
   (Hff : fully_faithful H) : 
-  iso (C:=[D, E', hsE']) (functor_composite F H) (functor_composite G H)
+  iso (C:=[D, E']) (functor_composite F H) (functor_composite G H)
   ->
-  iso (C:=[D, E, hsE]) F G.
+  iso (C:=[D, E]) F G.
 Proof.
   intro a.
   use nat_iso_from_pointwise_iso.
@@ -1044,9 +1031,9 @@ Proof.
 Defined.
 
 
-Definition functor_assoc_iso (D1 D2 D3 D4 : precategory) hsD4
+Definition functor_assoc_iso (D1 D2 D3 : precategory) (D4 : category)
      (F : functor D1 D2) (G : functor D2 D3) (H : functor D3 D4) :
-    iso (C:=[D1,D4,hsD4])
+    iso (C:=[D1,D4])
          (functor_composite (functor_composite F G) H)
          (functor_composite F (functor_composite G H)).
 Proof.
@@ -1060,9 +1047,9 @@ Proof.
      ).
 Defined.
 
-Definition functor_comp_id_iso (D1 D2 : precategory) hsD2
+Definition functor_comp_id_iso (D1 : precategory) (D2 : category)
      (F : functor D1 D2) :
-  iso (C:=[D1,D2,hsD2]) (functor_composite F (functor_identity _ )) F.
+  iso (C:=[D1,D2]) (functor_composite F (functor_identity _ )) F.
 Proof.
   use nat_iso_from_pointwise_iso.
   - intro. apply identity_iso.
@@ -1074,10 +1061,10 @@ Proof.
     ).
 Defined.
 
-Definition functor_precomp_iso (D1 D2 D3 : precategory)  hsD3
+Definition functor_precomp_iso (D1 D2 : precategory) (D3 : category)
     (F : functor D1 D2) (G H : functor D2 D3) :
-    iso (C:=[D2,D3,hsD3]) G H ->
-    iso (C:=[D1,D3,hsD3]) (functor_composite F G)
+    iso (C:=[D2,D3]) G H ->
+    iso (C:=[D1,D3]) (functor_composite F G)
                           (functor_composite F H).
 Proof.
   intro a.
@@ -1231,8 +1218,7 @@ End Square_Transfers.
 Section on_pullbacks.
 
 (* TODO: make all these implicit *)
-  Variable C : precategory.
-  Variable hs : has_homsets C.
+  Variable C : category.
   Variables a b c d : C.
   Variables (f : a --> b) (g : a --> c) (k : b --> d) (h : c --> d).
 
@@ -1316,11 +1302,7 @@ Section on_pullbacks.
   Lemma postcomp_pb_with_iso (y : C) (r : y --> d) (i : iso b y) (Hi : i ;; r = k) :
     ∑ H : f ;; i ;; r = g ;; h, isPullback H.
   Proof.
-    simple refine (@commutes_and_is_pullback_transfer_iso (C,,hs)
-              _ _ _ _  _ _ _ _
-              _ _ _ _  _ _ _ _
-              _ _ _ _  _ _ _ _
-              _ Pb);
+    simple refine (commutes_and_is_pullback_transfer_iso _ _ _ _ _ Pb);
     try apply identity_iso;
     try rewrite id_left;
     try rewrite id_right;
@@ -1339,13 +1321,13 @@ Section on_pullbacks.
   Lemma is_symmetric'_isPullback
     : isPullback (!sqr_comm) -> isPullback sqr_comm.
   Proof.
-    refine (is_symmetric_isPullback hs _).
+    use is_symmetric_isPullback; apply homset_property.
   Defined.
 
 End on_pullbacks.
 
-Arguments map_into_Pb {_ _ _ _ _ _ _ _ _ } _ _ {_} _ _ _ .
-Arguments map_into_Pb_unique {_ _ _ _ _ _ _ _ _} _ _ {_} _ _ _ _   .
+Arguments map_into_Pb {_ _ _ _ _ _ _ _ _ } _ Pb {_} _ _ _.
+Arguments map_into_Pb_unique {_ _ _ _ _ _ _ _ _} _ Pb {_} _ _ _ _.
 
 Section Pullbacks_hSet.
 
@@ -1501,7 +1483,7 @@ Proof.
     + apply (pr2 (pr1 XR) Three).
   - intro t.
     apply subtypePath.
-    + intro. apply isapropdirprod; apply has_homsets_HSET.
+    + intro. apply isapropdirprod; apply homset_property.
     + simpl.
       apply path_to_ctr.
       destruct t as [t [H1 H2]].

TypeTheory/Cubical/FillFromComp.v

@@ -359,7 +359,7 @@ now rewrite <-!assoc, H2, H3, assoc, H4, id_left, id_right.
 Qed.
 
 (* We can lift the above operations to presheaves using yoneda *)
-Let yon := yoneda_functor_data C.
+Let yon := yoneda_functor_data C : functor_data C (PreShv C).
 
 Definition p_PreShv (I : C) : yon (I+) --> yon I := # yon (p_F I).
 
@@ -515,8 +515,7 @@ Qed.
 
 Lemma e₀_f_pb {I J} (f : J --> I) : isPullback (e₀_f f).
 Proof.
-apply Auxiliary.is_symmetric'_isPullback.
-apply functor_category_has_homsets.
+apply is_symmetric'_isPullback.
 apply pb_if_pointwise_pb; intros K.
 apply Auxiliary.isPullback_HSET; intros L f1 f2.
 now apply e₀_pb.

TypeTheory/OtherDefs/CwF_Pitts_to_DM.v

@@ -96,14 +96,11 @@ Proof.
     + apply (π _ ). 
     + simpl. unfold dm_sub_struct_of_CwF.
       simpl.
-      set (T:= postcomp_pb_with_iso CC).
-      set (T':= T (homset_property _) _ _ _ _ (q_cwf A f) _ _ f _ (is_pullback_reindx_cwf (homset_property _) _ _ _ _ )).
-      refine (pr1 (T' _ _ _ _ )).
+      refine (pr1 (postcomp_pb_with_iso CC _ _ _ _ (q_cwf A f) _ _ f _
+            (is_pullback_reindx_cwf (homset_property _) _ _ _ _ ) _ _ _ _)).
       sym. assumption.
-    + 
-      set (T:= postcomp_pb_with_iso CC (homset_property _)).
-      set (T':= T _ _ _ _  (q_cwf A f) _ _ f _ (is_pullback_reindx_cwf (homset_property _) _ _ _ _ )).
-      eapply (pr2 (T' _ _ _ _ )).
+    + eapply (pr2 ( postcomp_pb_with_iso CC _ _ _ _  (q_cwf A f) _ _ f _
+              (is_pullback_reindx_cwf (homset_property _) _ _ _ _ ) _ _ _ _ )).
   - simpl.
     apply hinhpr.
     unfold iso_to_dpr.

TypeTheory/OtherDefs/TypeCat_to_DM.v

@@ -83,13 +83,12 @@ Proof.
     + apply (dpr_typecat _ ).
     + simpl. unfold dm_sub_struct_of_TypeCat.
       simpl.
-      set (T:= postcomp_pb_with_iso CC (homset_property _)).
-      refine (pr1 (T _ _ _ _ (q_typecat A f) _ _ f _ _ _ _ _ _)).
+      (* TODO: improve implicit arguments of [postcomp_pb_with_iso] *)
+      refine (pr1 (postcomp_pb_with_iso CC _ _ _ _ _ _ _ _ _ _ _ _ _ _)).
       apply is_symmetric_isPullback. { apply homset_property. }
       apply reind_pb_typecat.
       sym. assumption.
-    + set (T:= postcomp_pb_with_iso CC (homset_property _)).
-      eapply (pr2 (T _ _ _ _ _ _ _ _ _ _ _ _ _ _)).
+    + eapply (pr2 (postcomp_pb_with_iso CC _ _ _ _ _ _ _ _ _ _ _ _ _ _)).
  - simpl.
     apply hinhpr.
     unfold iso_to_dpr.