Adapting to UniMath refactoring precategories: fixed Cubical; all now compiling again.

Author: peterlefanulumsdaine

TypeTheory/Cubical/FillFromComp.v

@@ -110,12 +110,12 @@ Arguments isPullback {_ _ _ _ _ _ _ _ _} _.
 
 Section cubical.
 
-Context {C : precategory} (hsC : has_homsets C) (BPC : BinProducts C).
+Context {C : category} (BPC : BinProducts C).
 
 (* Setup notations *)
 Local Notation "Γ ⊢" := (PreShv (∫ Γ)) (at level 50).
 Local Notation "Γ ⊢ A" := (@TermIn _ Γ A) (at level 50).
-Local Notation "A ⦃ s ⦄" := (subst_type hsC A s) (at level 40, format "A ⦃ s ⦄").
+Local Notation "A ⦃ s ⦄" := (subst_type A s) (at level 40, format "A ⦃ s ⦄").
 Local Notation "Γ ⋆ A" := (@ctx_ext _ Γ A) (at level 30).
 Local Notation "c '⊗' d" :=
   (BinProductObject _ (@BinProducts_PreShv C c d)) : cat.
@@ -292,14 +292,14 @@ Lemma isPullback_pF_e₀ I J (f : J --> I) :
   isPullback (nat_trans_ax p_F f) → isPullback (nat_trans_ax e₀ f).
 Proof.
 intros H.
-apply (isPullback_two_pullback hsC _ _ _ _ _ _ H).
+apply (isPullback_two_pullback (homset_property _) _ _ _ _ _ _ H).
 intros K g h Hgh.
 use (unique_exists h); simpl in *.
 - rewrite <- Hgh.
   set (HI := nat_trans_eq_pointwise Hpe₀ I).
   set (HJ := nat_trans_eq_pointwise Hpe₀ J); cbn in HI, HJ.
   now rewrite HI, HJ, !id_right.
-- now intros HH; apply isapropdirprod; apply hsC.
+- now intros HH; apply isapropdirprod; apply homset_property.
 - intros h' [H1 H2].
   rewrite <- H2.
   set (HH := nat_trans_eq_pointwise Hpe₀ J); cbn in HH.
@@ -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 hsC.
+Let yon := yoneda_functor_data C.
 
 Definition p_PreShv (I : C) : yon (I+) --> yon I := # yon (p_F I).
 
@@ -391,15 +391,15 @@ use make_nat_trans.
   now apply funextsec; intro x; cbn; rewrite assoc.
 Defined.
 
-Lemma isMonic_e₀_PreShv I : isMonic (e₀_PreShv I).
+Lemma isMonic_e₀_PreShv I : @isMonic (PreShv C) _ _ (e₀_PreShv I).
 Proof.
 intros Γ σ τ H.
 apply (nat_trans_eq has_homsets_HSET); intros J; apply funextsec; intro ρ.
 generalize (eqtohomot (nat_trans_eq_pointwise H J) ρ).
 now apply isMonic_e₀.
 Qed.
 
-Lemma isMonic_e₁_PreShv I : isMonic (e₁_PreShv I).
+Lemma isMonic_e₁_PreShv I : @isMonic (PreShv C) _ _ (e₁_PreShv I).
 Proof.
 intros Γ σ τ H.
 apply (nat_trans_eq has_homsets_HSET); intros J; apply funextsec; intro ρ.