instMvFunctor — Mathlib

English

The composite functor Comp F G inherits a functorial structure: it is a MvFunctor with map defined by Comp.map.

Русский

У составного функторa Comp F G наследуется структура функторности: это MvFunctor с отображением, заданным как Comp.map.

LaTeX

$$$\text{instance } : \mathrm{MvFunctor}(\mathrm{Comp} F G)\text{ where }\mathrm{map} f := \mathrm{Comp.map} f.$$$

Lean4

instance : MvFunctor (Comp F G) where map f := Comp.map f

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