English
For indexed families I(s) of categories with IsCofiltered, the evaluation functors are initial.
Русский
Для семейства категорий I(s) с IsCofiltered оценочные функторы являются начальными.
LaTeX
$$$\forall \alpha, I : \alpha \to \mathrm{Type}, [\forall s, \mathrm{IsCofiltered}(I(s))] \, (\Pi\text{-eval}\; I\; s).\mathrm{Initial}$$$
Lean4
instance initial_eval [∀ s, IsCofiltered (I s)] (s : α) : (Pi.eval I s).Initial := by
classical
apply Functor.initial_of_exists_of_isCofiltered
· exact fun i => ⟨Function.update (fun t => nonempty.some) s i, ⟨by simpa using 𝟙 _⟩⟩
· intro d c f g
let c't : (∀ s, (c' : I s) × (c' ⟶ c s)) := Function.update (fun t => ⟨c t, 𝟙 (c t)⟩) s ⟨eq f g, eqHom f g⟩
refine ⟨fun t => (c't t).1, fun t => (c't t).2, ?_⟩
dsimp only [Pi.eval_obj, Pi.eval_map, c't]
rw [Function.update_self]
simpa using eq_condition _ _
