English
For indexed families of categories I(s), if each I(s) is filtered, then the evaluation functors Pi.eval at s are final.
Русский
Для семейства категорий I(s) индексируемого типа, если каждая I(s) фильтрована, то оценочные функторы Pi.eval на s финальны.
LaTeX
$$$\forall \alpha, I : \alpha \to \mathrm{Type}, [\forall s, \mathrm{IsFiltered}(I(s))] \, (\Pi\text{-eval}\; I\; s).\mathrm{Final}$$$
Lean4
instance final_eval [∀ s, IsFiltered (I s)] (s : α) : (Pi.eval I s).Final := by
classical
apply Functor.final_of_exists_of_isFiltered
· 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 s ⟶ c')) := Function.update (fun t => ⟨c t, 𝟙 (c t)⟩) s ⟨coeq f g, coeqHom 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 coeq_condition _ _
