English
For each C ⥤ D ⥤ E, map₂Functor F x₁ ⟶ map₂Functor F x₂ is a natural transformation, giving a functorial structure on ThinSkeleton.
Русский
Для F: C ⥤ D ⥤ E отображение map₂Functor F x₁ ⟶ map₂Functor F x₂ образует натуральную трансформацию и задаёт функторную структуру на тонком скелете.
LaTeX
$$map₂Functor (F) : ThinSkeleton C → ThinSkeleton D ⥤ ThinSkeleton E$$
Lean4
/-- For each `x : ThinSkeleton C`, we promote `map₂ObjMap F x` to a functor -/
def map₂Functor (F : C ⥤ D ⥤ E) : ThinSkeleton C → ThinSkeleton D ⥤ ThinSkeleton E := fun x =>
{ obj := fun y => map₂ObjMap F x y
map := fun {y₁} {y₂} =>
@Quotient.recOnSubsingleton C (isIsomorphicSetoid C)
(fun x => (y₁ ⟶ y₂) → (map₂ObjMap F x y₁ ⟶ map₂ObjMap F x y₂)) _ x fun X =>
Quotient.recOnSubsingleton₂ y₁ y₂ fun _ _ hY => homOfLE (hY.le.elim fun g => ⟨(F.obj X).map g⟩) }
