English
Extensionality for morphisms in the category of sheafed spaces: if two morphisms α, β: X → Y have the same base map and their structure maps agree after adjusting by the equality of bases, then α = β.
Русский
Эскстенциалность морфизмов в категории расслоенных пространств: если два морфизма α, β: X → Y имеют одинаковую базовую карту и их структуры согласованы после поправки на равенство оснований, то α = β.
LaTeX
$$$\forall X,Y:\mathrm{SheafedSpace}(C),\forall \alpha,\beta:X\to Y,\;\alpha.base=\beta.base\Rightarrow\Big(\alpha.c \gg \mathrm{whiskerRight}(\mathrm{eqToHom}(\mathrm{by rw [w]}))\_ = \beta.c\Big)\Rightarrow \alpha=\beta$$$
Lean4
@[ext (iff := false)]
theorem ext {X Y : SheafedSpace C} (α β : X ⟶ Y) (w : α.base = β.base)
(h : α.c ≫ whiskerRight (eqToHom (by rw [w])) _ = β.c) : α = β :=
PresheafedSpace.ext α β w h
