Switched functor-procategory notation [C,D,has_homsets D] to functor-category notation [C,D] wherever possible

Author: peterlefanulumsdaine

TypeTheory/ALV1/RelativeUniverses.v

@@ -942,8 +942,8 @@ Definition isweq_weak_relative_universe_transfer
            (R_full : full R)
            (isD : is_univalent D) (isD' : is_univalent D')
            (T : functor D' D)
-           (eta : iso (C:=[D, D, pr2 D]) (functor_identity D) (S ∙ T))
-           (eps : iso (C:=[D', D', pr2 D']) (T ∙ S) (functor_identity D'))
+           (eta : iso (C:=[D, D]) (functor_identity D) (S ∙ T))
+           (eps : iso (C:=[D', D']) (T ∙ S) (functor_identity D'))
            (S_faithful : faithful S) 
   : isweq weak_relative_universe_transfer.
 Proof.
@@ -964,8 +964,8 @@ Definition weq_weak_relative_universe_transfer
            (R_full : full R)
            (isD : is_univalent D) (isD' : is_univalent D')
            (T : functor D' D)
-           (eta : iso (C:=[D, D, pr2 D]) (functor_identity D) (S ∙ T))
-           (eps : iso (C:=[D', D', pr2 D']) (T ∙ S) (functor_identity D'))
+           (eta : iso (C:=[D, D]) (functor_identity D) (S ∙ T))
+           (eps : iso (C:=[D', D']) (T ∙ S) (functor_identity D'))
            (S_ff : fully_faithful S)
 : weak_relative_universe J ≃ weak_relative_universe J'
 := make_weq _ (isweq_weak_relative_universe_transfer R_full isD isD' T eta eps S_ff).

TypeTheory/ALV1/Transport_along_Equivs.v

@@ -113,7 +113,7 @@ Proof.
 Defined.
 
 
-Definition epsinv : iso (C:=[_ , _ , has_homsets_preShv _ ])
+Definition epsinv : iso (C:=[_ , _])
                         (functor_identity (preShv C)) (ext ∙ Fop_precomp).
 Proof.
   set (XR':= (counit_iso_from_adj_equivalence_of_precats equiv_Fcomp)).
@@ -122,7 +122,7 @@ Proof.
 Defined.
 
 
-Definition etainv : iso (C:=[ _ , _ , (has_homsets_preShv _ )]) 
+Definition etainv : iso (C:=[ _ , _]) 
                         (Fop_precomp ∙ ext) (functor_identity (preShv D)).
 Proof.
   set (XR := (unit_iso_from_adj_equivalence_of_precats equiv_Fcomp)).

TypeTheory/ALV2/RelUnivTransfer.v

@@ -334,8 +334,8 @@ Section RelUniv_Transfer.
     Context (R_ses : split_ess_surj R)
             (D'_univ : is_univalent D')
             (invS : functor D' D)
-            (eta : iso (C:=[D, D, pr2 D]) (functor_identity D) (S ∙ invS))
-            (eps : iso (C:=[D', D', pr2 D']) (invS ∙ S) (functor_identity D'))
+            (eta : iso (C:=[D, D]) (functor_identity D) (S ∙ invS))
+            (eps : iso (C:=[D', D']) (invS ∙ S) (functor_identity D'))
             (S_ff : fully_faithful S).
 
     Let E := ((S,, (invS,, (pr1 eta, pr1 eps)))
@@ -348,10 +348,10 @@ Section RelUniv_Transfer.
     Let ε' := pr2 (pr121 AE) : nat_trans (invS ∙ S) (functor_identity _).
     Let η := functor_iso_from_pointwise_iso
                 _ _ _ _ _ η' (pr12 (adjointificiation E))
-            : iso (C:=[D, D, pr2 D]) (functor_identity D) (S ∙ invS).
+            : iso (C:=[D, D]) (functor_identity D) (S ∙ invS).
     Let ε := functor_iso_from_pointwise_iso
                 _ _ _ _ _ ε' (pr22 (adjointificiation E))
-            : iso (C:=[D', D', pr2 D']) (invS ∙ S) (functor_identity D').
+            : iso (C:=[D', D']) (invS ∙ S) (functor_identity D').
 
     Let ηx := Constructions.pointwise_iso_from_nat_iso (iso_inv_from_iso η).
     Let αx := Constructions.pointwise_iso_from_nat_iso (α,,α_is_iso).
@@ -655,8 +655,8 @@ Section WeakRelUniv_Transfer.
 
   (* S is an equivalence *)
   Context (T : functor D' D).
-  Context (η : iso (C := [D, D, pr2 D]) (functor_identity D) (S ∙ T)).
-  Context (ε : iso (C := [D', D', pr2 D']) (T ∙ S) (functor_identity D')).
+  Context (η : iso (C := [D, D]) (functor_identity D) (S ∙ T)).
+  Context (ε : iso (C := [D', D']) (T ∙ S) (functor_identity D')).
   Context (S_full : full S).
   Context (S_faithful : faithful S).
 

TypeTheory/Auxiliary/Auxiliary.v

@@ -11,7 +11,6 @@ Possibly some should be upstreamed to “UniMath” eventually.
 
 *)
 
-
 Require Import UniMath.Foundations.PartD.
 Require Import UniMath.Foundations.Sets.
 Require Import UniMath.Combinatorics.StandardFiniteSets.

TypeTheory/OtherDefs/CwF_Pitts_natural.v

@@ -30,12 +30,10 @@ Local Notation "C '^op'" := (opp_precat C) (at level 3, format "C ^op").
 (** * A "preview" of the definition *)
 
 Module Preview.
-
-Let hsHSET := has_homsets_HSET.
 
 Variable C : precategory.
 Variable hs : has_homsets C. 
-Variable Ty Tm: [C^op, HSET, hsHSET]. (* functor C^op HSET. *)
+Variable Ty Tm: [C^op, HSET]. (* functor C^op HSET. *)
 Variable p : _ ⟦Tm, Ty⟧. (* needs to be written as mor in a precat *)
 
 Variable comp : forall (Γ : C) (A : pr1hSet ((Ty : functor _ _ ) Γ)), C.
@@ -74,17 +72,15 @@ End Preview.
 
 Section definition.
 
-Let hsHSET := has_homsets_HSET.
-
 Variable C : precategory.
 Variable hsC : has_homsets C.
 
 Definition tt_structure : UU :=
-  ∑ TyTm : [C^op, HSET, hsHSET] × [C^op, HSET, hsHSET],
+  ∑ TyTm : [C^op, HSET] × [C^op, HSET],
            _ ⟦pr2 TyTm, pr1 TyTm⟧.
 
-Definition Ty (X : tt_structure) : [C^op, HSET, hsHSET] := pr1 (pr1 X).
-Definition Tm (X : tt_structure) : [C^op, HSET, hsHSET] := pr2 (pr1 X).
+Definition Ty (X : tt_structure) : [C^op, HSET] := pr1 (pr1 X).
+Definition Tm (X : tt_structure) : [C^op, HSET] := pr2 (pr1 X).
 Definition p (X : tt_structure) :  _ ⟦Tm X, Ty X⟧ := pr2 X.
 
 Definition comp_structure (X : tt_structure) : UU :=
@@ -135,4 +131,4 @@ Coercion pullback_structure_from_is_natural_CwF (X : is_natural_CwF) :
   pullback_structure (comp_structure_from_is_natural_CwF X) := pr2 (pr2 X).
 
 
-End definition.
+End definition.