Tiny bit of upstreaming missed in prev commit

peterlefanulumsdaine · peterlefanulumsdaine · commit f930f16f0873 · 2022-01-04T18:04:39.000Z
diff --git a/TypeTheory/ALV2/SplitTypeCat_ComprehensionCat.v b/TypeTheory/ALV2/SplitTypeCat_ComprehensionCat.v
@@ -429,8 +429,6 @@ Section SplitTypeCat_from_DiscreteComprehensionCat.
     : typecat_structure C
     := (_ ,, typecat_structure2_from_discrete_comprehension_cat_structure).
 
-  Arguments unique_lift : simpl never. (* TODO: upstream *)
-
   Definition is_split_typecat_from_discrete_comprehension_cat_structure
     : is_split_typecat typecat_structure_from_discrete_comprehension_cat_structure.
   Proof.
diff --git a/TypeTheory/Auxiliary/DisplayedCategories.v b/TypeTheory/Auxiliary/DisplayedCategories.v
@@ -149,6 +149,8 @@ Section Discrete_Fibrations.
     : ∃! d' : D c', d' -->[f] d
   := pr1 H_D c c' f d.
 
+  Arguments unique_lift : simpl never.
+
   Definition lift_source {C} {D : disp_cat C} (H_D : is_discrete_fibration D)
       {c c'} (f : c' --> c) (d : D c)
     : D c'
