This repository was archived by the owner on Jul 24, 2024. It is now read-only.
File tree Expand file tree Collapse file tree 2 files changed +3
-3
lines changed Expand file tree Collapse file tree 2 files changed +3
-3
lines changed Original file line number Diff line number Diff line change @@ -355,7 +355,7 @@ begin
355
355
haveI : preserves_finite_limits F :=
356
356
begin
357
357
apply preserves_finite_limits_of_preserves_finite_limits_of_size.{u₁},
358
- intros, resetI, apply preserves_limit_of_Lan_presesrves_limit
358
+ intros, resetI, apply preserves_limit_of_Lan_preserves_limit
359
359
end ,
360
360
apply flat_of_preserves_finite_limits
361
361
end ⟩
@@ -371,7 +371,7 @@ def preserves_finite_limits_iff_Lan_preserves_finite_limits (F : C ⥤ D) :
371
371
inv_fun := λ _,
372
372
begin
373
373
apply preserves_finite_limits_of_preserves_finite_limits_of_size.{u₁},
374
- intros, resetI, apply preserves_limit_of_Lan_presesrves_limit
374
+ intros, resetI, apply preserves_limit_of_Lan_preserves_limit
375
375
end ,
376
376
left_inv := λ x,
377
377
begin
Original file line number Diff line number Diff line change @@ -99,7 +99,7 @@ instance whiskering_right_preserves_limits {C : Type u} [category C]
99
99
100
100
/-- If `Lan F.op : (Cᵒᵖ ⥤ Type*) ⥤ (Dᵒᵖ ⥤ Type*)` preserves limits of shape `J`, so will `F`. -/
101
101
noncomputable
102
- def preserves_limit_of_Lan_presesrves_limit {C D : Type u} [small_category C] [small_category D]
102
+ def preserves_limit_of_Lan_preserves_limit {C D : Type u} [small_category C] [small_category D]
103
103
(F : C ⥤ D) (J : Type u) [small_category J]
104
104
[preserves_limits_of_shape J (Lan F.op : _ ⥤ (Dᵒᵖ ⥤ Type u))] :
105
105
preserves_limits_of_shape J F :=
You can’t perform that action at this time.
0 commit comments