instCoeFunForallToTypeObjOppositeOpY

English

There is an instance giving CoeFun from Meq P S to the dependent type family over arrows in S.

Русский

Существует экземпляр, задающий отображение "коэффициент функции" из Meq P S в зависимую семью типов по стрелкам в S.

LaTeX

$${Meq}.instCoeFun: CoeFun (Meq P S) (∀ I:S.Arrow, ToType (P.obj (op I.Y)))$$

Lean4

instance {X} (P : Cᵒᵖ ⥤ D) (S : J.Cover X) : CoeFun (Meq P S) fun _ => ∀ I : S.Arrow, ToType (P.obj (op I.Y)) :=
  ⟨fun x => x.1⟩

Похожие утверждения