English
There is a natural transformation map₂NatTrans F between map₂Functor F x₁ and map₂Functor F x₂ parameterized by a morphism x₁ ⟶ x₂.
Русский
Существует естественная трансформация map₂NatTrans F между map₂Functor F x₁ и map₂Functor F x₂ через f: x₁⟶x₂.
LaTeX
$$map₂NatTrans (F) : {x₁ x₂ : ThinSkeleton C} → (x₁ ⟶ x₂) → (map₂Functor F x₁ ⟶ map₂Functor F x₂)$$
Lean4
/-- This provides natural transformations `map₂Functor F x₁ ⟶ map₂Functor F x₂` given
`x₁ ⟶ x₂` -/
def map₂NatTrans (F : C ⥤ D ⥤ E) : {x₁ x₂ : ThinSkeleton C} → (x₁ ⟶ x₂) → (map₂Functor F x₁ ⟶ map₂Functor F x₂) :=
fun {x₁} {x₂} =>
@Quotient.recOnSubsingleton₂ C C (isIsomorphicSetoid C) (isIsomorphicSetoid C)
(fun x x' : ThinSkeleton C => (x ⟶ x') → (map₂Functor F x ⟶ map₂Functor F x')) _ x₁ x₂
(fun X₁ X₂ f =>
{ app := fun y => Quotient.recOnSubsingleton y fun Y => homOfLE (f.le.elim fun f' => ⟨(F.map f').app Y⟩) })
-- TODO: state the lemmas about what happens when you compose with `toThinSkeleton`
