Factored out a few more [has_homsets]

Author: peterlefanulumsdaine

TypeTheory/ALV1/CwF_def.v

@@ -425,8 +425,6 @@ Let TY' : preShv D := Ty (pr1 T').
 Let pp : _ ⟦ TM , TY ⟧ := pr1 T.
 Let pp' : _ ⟦ TM' , TY' ⟧ := pr1 T'.
 
-Let hsDop : has_homsets (opp_precat D) := has_homsets_opp (homset_property _).
-
 Let ηη : functor (preShv D) (preShv C) :=
   pre_composition_functor C^op D^op _ (functor_opp F).
 
@@ -520,8 +518,6 @@ Let TY' : preShv RC := Ty (pr1 T').
 Let pp : _ ⟦ TM , TY ⟧ := pr1 T.
 Let pp' : _ ⟦ TM' , TY' ⟧ := pr1 T'.
 
-Let hsRCop : has_homsets (opp_precat RC) := has_homsets_opp (homset_property _).
-
 Let ηη : functor (preShv RC) (preShv C) :=
   pre_composition_functor C^op RC^op _ (functor_opp (Rezk_eta C)).
 

TypeTheory/ALV1/TypeCat.v

@@ -188,17 +188,16 @@ Definition is_split_typecat {CC : precategory} (C : typecat_structure CC)
                ;; q_typecat (A{{f}}) g
                ;; q_typecat A f).
 
-Lemma isaprop_is_split_typecat (CC : precategory) (hs : has_homsets CC)
+Lemma isaprop_is_split_typecat (CC : category)
        (C : typecat_structure CC) : isaprop (is_split_typecat C).
 Proof.
   repeat (apply isofhleveltotal2; intros).
   - apply impred; intro; apply isapropisaset.
   - repeat (apply impred; intro). apply x.
-  - repeat (apply impred; intro). apply hs.
+  - repeat (apply impred; intro). apply homset_property.
   - repeat (apply impred; intro). apply x.
-  - intros.  
-    repeat (apply impred; intro).
-    apply hs.
+  - intros.
+    repeat (apply impred; intro). apply homset_property.
 Qed.
 
 Definition typecat := ∑ (C : category), (typecat_structure C).

TypeTheory/ALV2/SplitTypeCat_ComprehensionCat.v

@@ -901,8 +901,6 @@ Section SplitTypeCat_DiscreteComprehensionCat_Equiv.
              apply funextsec. intros ?.
              apply isaprop_isPullback.
       + apply isaprop_is_split_typecat.
-        apply homset_property.
-
     - intros DC.
       use total2_paths_f.
       2: use total2_paths_f.