Refactored precategories + has_homsets to categories in CwF_Pitts

Author: peterlefanulumsdaine

TypeTheory/OtherDefs/CwF_Pitts.v

@@ -676,7 +676,7 @@ Proof.
   apply idpath.
 Qed.
 
-Definition dpr_q_pbpairing_cwf_unique (hs : has_homsets CC)
+Definition dpr_q_pbpairing_cwf_unique
   {Γ} (A : C⟨Γ⟩)
   {Γ'} (f : Γ' --> Γ)
   {X} (h : X --> Γ ∙ A) (k : X --> Γ') (H : h ;; π A = k ;; f)
@@ -687,10 +687,10 @@ Proof.
   destruct t as [hk [e2 e1]]. 
   refine (@total2_paths_f _ _ (tpair _ hk (tpair _ e2 e1)) _ 
     (dpr_q_pbpairing_cwf_mapunique A f H hk e2 e1) _).
-  unshelve refine (total2_paths_f _ _); apply hs.
+  unshelve refine (total2_paths_f _ _); apply homset_property.
 Qed.
 
-Lemma is_pullback_reindx_cwf (hs : has_homsets CC) : ∏ (Γ : CC) (A : C⟨Γ⟩) (Γ' : CC) 
+Lemma is_pullback_reindx_cwf : ∏ (Γ : CC) (A : C⟨Γ⟩) (Γ' : CC) 
    (f : Γ' --> Γ),
    isPullback (dpr_q_cwf A f).
 Proof.
@@ -699,7 +699,6 @@ Proof.
   intros e h k H.
   exists (dpr_q_pbpairing_cwf _ _ h k H).
   apply dpr_q_pbpairing_cwf_unique.
-  assumption.
 Defined.
 
 End CwF_lemmas.

TypeTheory/OtherDefs/CwF_Pitts_to_DM.v

@@ -97,10 +97,10 @@ Proof.
     + simpl. unfold dm_sub_struct_of_CwF.
       simpl.
       refine (pr1 (postcomp_pb_with_iso CC _ _ _ _ (q_cwf A f) _ _ f _
-            (is_pullback_reindx_cwf (homset_property _) _ _ _ _ ) _ _ _ _)).
+            (is_pullback_reindx_cwf _ _ _ _ ) _ _ _ _)).
       sym. assumption.
     + eapply (pr2 ( postcomp_pb_with_iso CC _ _ _ _  (q_cwf A f) _ _ f _
-              (is_pullback_reindx_cwf (homset_property _) _ _ _ _ ) _ _ _ _ )).
+              (is_pullback_reindx_cwf _ _ _ _ ) _ _ _ _ )).
   - simpl.
     apply hinhpr.
     unfold iso_to_dpr.

TypeTheory/OtherDefs/CwF_Pitts_to_TypeCat.v

@@ -84,7 +84,7 @@ Proof.
   exists (@q_cwf CC C).
   exists (@dpr_q_cwf CC C).
   intros; apply @is_symmetric_isPullback. { apply homs_sets. }
-  apply is_pullback_reindx_cwf. apply homs_sets.
+  apply is_pullback_reindx_cwf.
 Defined.
 
 (** * Splitness of the constructed TypeCat *)