Some more precat->cat, following UniMath/UniMath#1426

Author: peterlefanulumsdaine

TypeTheory/ALV1/CwF_SplitTypeCat_Cats_Standalone.v

@@ -727,33 +727,33 @@ Qed.
 Definition compat_structures_category : category
   := make_category _ has_homsets_compat_structures_precategory.
 
-Definition pr1_equiv : @adj_equivalence_of_precats
+Definition pr1_equiv : @adj_equivalence_of_cats
                          compat_structures_category
                          term_fun_category
                          compat_structures_pr1_functor.
 Proof.
-  use adj_equivalence_of_precats_ff_split.
+  use adj_equivalence_of_cats_ff_split.
   - apply compat_structures_pr1_fully_faithful.
   - apply compat_structures_pr1_split_ess_surj.
 Defined.
 
-Definition pr2_equiv : @adj_equivalence_of_precats
+Definition pr2_equiv : @adj_equivalence_of_cats
                          compat_structures_category
                          qq_structure_category
                          compat_structures_pr2_functor.
 Proof.
-  use adj_equivalence_of_precats_ff_split.
+  use adj_equivalence_of_cats_ff_split.
   - apply compat_structures_pr2_fully_faithful.
   - apply compat_structures_pr2_split_ess_surj.
 Defined.
 
-Definition pr1_equiv_inv : adj_equivalence_of_precats (right_adjoint pr1_equiv).
+Definition pr1_equiv_inv : adj_equivalence_of_cats (right_adjoint pr1_equiv).
 Proof.
-  use adj_equivalence_of_precats_inv.
+  use adj_equivalence_of_cats_inv.
 Defined.
 
-Definition equiv_of_structures : adj_equivalence_of_precats _ 
-  := @comp_adj_equivalence_of_precats _ _ _ _ _ 
+Definition equiv_of_structures : adj_equivalence_of_cats _ 
+  := @comp_adj_equivalence_of_cats _ _ _ _ _ 
                                       pr1_equiv_inv pr2_equiv.
 
 Definition equiv_of_types_of_structures 

TypeTheory/ALV1/CwF_def.v

@@ -418,7 +418,7 @@ Proof.
   apply XT.
 Defined.  
 
-Let Fopequiv : adj_equivalence_of_precats _  := equiv_Fcomp F F_ff F_es.
+Let Fopequiv : adj_equivalence_of_cats _  := equiv_Fcomp F F_ff F_es.
 
 
 Definition pp'_eta : 
@@ -495,7 +495,7 @@ Proof.
 Defined.  
 
 
-Let RCequiv : adj_equivalence_of_precats _  := Rezk_op_adj_equiv C
+Let RCequiv : adj_equivalence_of_cats _  := Rezk_op_adj_equiv C
           HSET is_univalent_HSET.
 
 Lemma has_homsets_preShv (D : category) : has_homsets (preShv D).

TypeTheory/ALV1/Transport_along_Equivs.v

@@ -88,9 +88,9 @@ Proof.
 Defined.
 
 
-Definition equiv_Fcomp : adj_equivalence_of_precats Fop_precomp.
+Definition equiv_Fcomp : adj_equivalence_of_cats Fop_precomp.
 Proof.
-  apply rad_equivalence_of_precats.
+  apply rad_equivalence_of_cats.
   - apply is_univalent_functor_category.
     apply is_univalent_HSET.
   - apply ff_Fop_precomp.
@@ -116,7 +116,7 @@ Defined.
 Definition epsinv : iso (C:=[_ , _])
                         (functor_identity (preShv C)) (ext ∙ Fop_precomp).
 Proof.
-  set (XR':= (counit_iso_from_adj_equivalence_of_precats equiv_Fcomp)).
+  set (XR':= (counit_iso_from_adj_equivalence_of_cats equiv_Fcomp)).
   apply iso_inv_from_iso.
   apply XR'.
 Defined.
@@ -125,7 +125,7 @@ Defined.
 Definition etainv : iso (C:=[ _ , _]) 
                         (Fop_precomp ∙ ext) (functor_identity (preShv D)).
 Proof.
-  set (XR := (unit_iso_from_adj_equivalence_of_precats equiv_Fcomp)).
+  set (XR := (unit_iso_from_adj_equivalence_of_cats equiv_Fcomp)).
   apply iso_inv_from_iso.
   apply XR.
 Defined.
@@ -148,7 +148,7 @@ Proof.
      apply functor_assoc_iso.
   eapply iso_comp.
      eapply functor_precomp_iso.
-     apply (counit_iso_from_adj_equivalence_of_precats equiv_Fcomp).
+     apply (counit_iso_from_adj_equivalence_of_cats equiv_Fcomp).
   eapply iso_comp.
     apply functor_comp_id_iso.
 

TypeTheory/ALV2/CwF_SplitTypeCat_Equiv_Cats.v

@@ -632,10 +632,10 @@ Proof.
 Defined.
 
 Definition term_struc_to_qq_struc_is_equiv
-  : adj_equivalence_of_precats
+  : adj_equivalence_of_cats
       term_struc_to_qq_struc_fiber_functor.
 Proof.
-  use comp_adj_equivalence_of_precats.
+  use comp_adj_equivalence_of_cats.
   - apply fiber_equiv.
     apply is_equiv_of_equiv_over_id.
   - apply fiber_equiv.

TypeTheory/ALV2/FullyFaithfulDispFunctor.v

@@ -620,7 +620,7 @@ Section FullyFaithfulDispFunctor.
     Definition disp_cat_path_precat
                {C : category}
                (D D' : disp_cat C)
-      : D = D' ≃ disp_cat_data_from_disp_precat D = D'.
+      : D = D' ≃ disp_cat_data_from_disp_cat D = D'.
     Proof.
       apply path_sigma_hprop, isaprop_disp_cat_axioms.
     Defined.

TypeTheory/ALV2/RelUnivTransfer.v

@@ -341,7 +341,7 @@ Section RelUniv_Transfer.
     Let E := ((S,, (invS,, (pr1 eta, pr1 eps)))
                 ,, ((λ d,  (pr2 (Constructions.pointwise_iso_from_nat_iso eta d )))
                     , (λ d', (pr2 (Constructions.pointwise_iso_from_nat_iso eps d')))))
-            : equivalence_of_precats D D'.
+            : equivalence_of_cats D D'.
 
     Let AE := adjointificiation E.
     Let η' := pr1 (pr121 AE) : nat_trans (functor_identity _) (S ∙ invS).

TypeTheory/ALV2/SplitTypeCat_ComprehensionCat.v

@@ -453,13 +453,9 @@ Section DiscreteComprehensionCat_from_SplitTypeCat.
     - intros. apply isasetaprop. apply (pr1 (pr2 TC)).
   Qed.
 
-  Definition disp_precat_from_split_typecat_structure
-    : disp_precat C
-    := (_ ,, disp_cat_axioms_from_split_typecat_structure).
-
   Definition disp_cat_from_split_typecat_structure
     : disp_cat C
-    := disp_precat_from_split_typecat_structure.
+    := (_ ,, disp_cat_axioms_from_split_typecat_structure).
 
   Definition disp_cat_from_split_typecat_structure_is_univalent
     : is_univalent_disp disp_cat_from_split_typecat_structure.

TypeTheory/Articles/ALV_2018.v

@@ -60,27 +60,27 @@ Admitted.
 (** ** Equivalence between two versions of cwf structures *)
 
 Definition equiv_cat_cwf_cwf'_structure (C : category)
-  : equivalence_of_precats (cwf_structure_cat C) (cwf'_structure_cat C).
+  : equivalence_of_cats (cwf_structure_cat C) (cwf'_structure_cat C).
 Admitted.
 
 (** ** Equivalence between two versions of split typecat structures *)
 
 Definition equiv_cat_standalone_to_regrouped (C : category)
-  : equivalence_of_precats
+  : equivalence_of_cats
       (split_typecat_structure_cat C) (split_typecat'_structure_cat C).
 Admitted.
 
 (** ** Auxiliary equivalence between the reordered structures *)
 
 Definition weq_cwf'_sty' (C : category)
-  : equivalence_of_precats
+  : equivalence_of_cats
       (cwf'_structure_cat C) (split_typecat'_structure_cat C).
 Admitted.
 
 (** ** Main construction: equivalence between split typecat structures and cwf structures *)
 
 Definition weq_sty_cwf (C : category)
-  : equivalence_of_precats
+  : equivalence_of_cats
       (split_typecat_structure_cat C) (cwf_structure_cat C).
 Admitted.
 
@@ -97,7 +97,7 @@ Proposition fully_faithful_cwf_to_rep (C : category)
 Admitted.
 
 Definition isweq_from_cwf_to_rep {C : category} (C_univ : is_univalent C)
-  : adj_equivalence_of_precats (functor_cwf_to_rep C).
+  : adj_equivalence_of_cats (functor_cwf_to_rep C).
 Admitted.
 
 (** * Transfer of [cwf_structure]s along weak equivalences *)
@@ -114,13 +114,13 @@ Admitted.
 Definition transfer_rep_map_weak_equivalence
   {C D : category} (F : C ⟶ D) 
   : fully_faithful F → essentially_surjective F
-  → equivalence_of_precats (rep_map_cat C) (rep_map_cat D).
+  → equivalence_of_cats (rep_map_cat C) (rep_map_cat D).
 Admitted.
 
 (** * Equivalence between [rep_map C] and [cwf (Rezk_completion C)] *)
 
 Definition equiv_cat_rep_map_cwf_Rezk (C : category)
-  : equivalence_of_precats
+  : equivalence_of_cats
       (rep_map_cat C)
       (cwf_structure_cat (Rezk_completion C)).
 Admitted.

TypeTheory/Auxiliary/Auxiliary.v

@@ -551,7 +551,7 @@ Defined.
 
 Definition isweq_left_adj_equivalence_on_mor_total {C D : category} (F : functor C D) 
            (isC : is_univalent C) (isD : is_univalent D)
-           (H : adj_equivalence_of_precats F) 
+           (H : adj_equivalence_of_cats F) 
 : isweq (functor_on_mor_total F).
 Proof.
   use (gradth _ _ _ _ ).
@@ -656,15 +656,15 @@ Defined.
 (** Specifically: the composition of (adjoint) equivalences of precats. *)
 
 Coercion left_adj_from_adj_equiv (X Y : category) (K : functor X Y)
-         (HK : adj_equivalence_of_precats K)
+         (HK : adj_equivalence_of_cats K)
   : is_left_adjoint K
 := pr1 HK.
 
 Section about_equivalences.
 
 Variables D1 D2 : category.
 Variable F : functor D1 D2.
-Variable GG : adj_equivalence_of_precats F.
+Variable GG : adj_equivalence_of_cats F.
 
 Let G : functor D2 D1 := right_adjoint GG.
 Let η := unit_from_left_adjoint GG.
@@ -846,7 +846,7 @@ Lemma form_adjunction_ff_split
     apply iso_inv_after_iso.
 Qed.
 
-Definition adj_equivalence_of_precats_ff_split : adj_equivalence_of_precats F.
+Definition adj_equivalence_of_cats_ff_split : adj_equivalence_of_cats F.
 Proof.
   use tpair.
   - exists G_ff_split.
@@ -891,7 +891,7 @@ Proof.
 Qed.
 
 Lemma right_adj_equiv_is_full {D1 D2 : category}
-  (F : functor D1 D2) (GG : adj_equivalence_of_precats F)
+  (F : functor D1 D2) (GG : adj_equivalence_of_cats F)
   : full (right_adjoint GG).
 Proof.
   apply full_from_ff, right_adj_equiv_is_ff.
@@ -1052,8 +1052,8 @@ Proof.
 Defined.
 
 Definition adj_from_equiv (D1 D2 : category) (F : functor D1 D2):
-    adj_equivalence_of_precats F → is_left_adjoint F := fun x => pr1 x.
-Coercion adj_from_equiv : adj_equivalence_of_precats >-> is_left_adjoint.
+    adj_equivalence_of_cats F → is_left_adjoint F := fun x => pr1 x.
+Coercion adj_from_equiv : adj_equivalence_of_cats >-> is_left_adjoint.
 
 (** ** Functors and isomorphisms *)
 

TypeTheory/Auxiliary/CategoryTheory.v

@@ -5,6 +5,10 @@ TODO: upstream this to UniMath, and possibly propose improvements there as in th
 Require Import UniMath.Foundations.All.
 Require Import UniMath.CategoryTheory.All.
 
+(* TODO: remove this once renamed to this upstream (from erroneous “…precats…”) *)
+Coercion adj_equiv_of_cats_from_adj {A B : category} (E : adj_equiv A B)
+  : adj_equivalence_of_cats E := pr2 E.
+
 Definition adj_equiv_from_adjunction
     {C D : category}
     (FG : adjunction C D)
@@ -32,8 +36,8 @@ Definition compose_adj_equiv
   : adj_equiv C E.
 Proof.
   exists (functor_composite F G).
-  apply comp_adj_equivalence_of_precats;
-    apply adj_equiv_of_precats_from_adj.
+  apply comp_adj_equivalence_of_cats;
+    apply adj_equiv_of_cats_from_adj.
 Defined.
 
 Definition inv_adj_equiv
@@ -42,7 +46,7 @@ Definition inv_adj_equiv
   : adj_equiv D C.
 Proof.
   exists (adj_equivalence_inv F).
-  apply adj_equivalence_of_precats_inv.
+  apply adj_equivalence_of_cats_inv.
 Defined.
 
 Definition nat_trans_from_nat_iso
@@ -151,19 +155,19 @@ Defined.
 (* TODO: Notes towards some possible improvements in UniMath’s treatment of adjunctions, equivalences (and a few other unrelated things in the library):
 
   One really confusing point is having
-  [adj_equivalence_of_precats] for the property of (or structure on) a functor,
+  [adj_equivalence_of_cats] for the property of (or structure on) a functor,
   while
-  [equivalence_of_precats] is the sigma-type of this over functors.
+  [equivalence_of_cats] is the sigma-type of this over functors.
 
   Suggestion:
   - [equivalence] changes to [equiv] throughout (this seems unambiguous?)
 
-  - [adj_equivalence_of_precats]
+  - [adj_equivalence_of_cats]
     changes to either
     [is_adj_equiv] or [adj_equiv_structure]
-    (possible also [_of_precats], but this seems reasonably implicit since it’s on a functor) 
-  - [equivalence_of_precats]
-    changes to [adj_equiv_of_precats]
+    (possible also [_of_cats], but this seems reasonably implicit since it’s on a functor) 
+  - [equivalence_of_cats]
+    changes to [adj_equiv_of_cats]
   - lemmas about them are renamed as consistently as possible, following these.
 
   - consolidate with the material from [DisplayedCats.Equivalences_bis], including its adj_equiv.