English
Naturality for pushforward along locally full functors between presheaves of types.
Русский
Натуральность для перемещения по отображениям вдоль локально полных функторов между предобразными типами.
LaTeX
$$$\\text{naturality (Types)}$$$
Lean4
/-- (Implementation). The `pushforwardFamily` defined is compatible. -/
theorem pushforwardFamily_compatible {X} (x : ℱ.obj (op X)) : (pushforwardFamily α x).Compatible :=
by
suffices
∀ {Z W₁ W₂} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁) (iZW₂ : Z ⟶ G.obj W₂),
iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
ℱ'.1.map iZW₁.op (α.app _ (ℱ.map iWX₁.op x)) = ℱ'.1.map iZW₂.op (α.app _ (ℱ.map iWX₂.op x))
by
rintro Y₁ Y₂ Z iZY₁ iZY₂ f₁ f₂ h₁ h₂ e
simp only [pushforwardFamily, ← FunctorToTypes.map_comp_apply, ← op_comp]
generalize Nonempty.some h₁ = l₁
generalize Nonempty.some h₂ = l₂
obtain ⟨W₁, iYW₁, iWX₁, rfl⟩ := l₁
obtain ⟨W₂, iYW₂, iWX₂, rfl⟩ := l₂
exact this _ _ _ _ (by simpa only [Category.assoc] using e)
introv e
refine ext G _ _ fun V iVZ ↦ ?_
simp only [← op_comp, ← FunctorToTypes.map_comp_apply, naturality_apply, Category.assoc, e]
