English
There is an induction principle for morphisms in the sum C ⊕ D: any property P of morphisms is determined by its behavior on morphisms coming from C (via inl) or from D (via inr).
Русский
Существует принцип индукции по морфизмам в сумме C ⊕ D: свойство P морфизмов определяется по его поведению на морфизмах, получаемых через inl из C и через inr из D.
LaTeX
$$$$ \forall P,\; (\forall x,y: C, f: x\to y \Rightarrow P((\mathrm{inl}\; C D).map f)) \, \land \, (\forall x,y: D, g: x\to y \Rightarrow P((\mathrm{inr}\; C D).map g)) \Rightarrow \forall X,Y:\, C\oplus D, (f:X\to Y) \Rightarrow P(f). $$$$
Lean4
/-- `inl_` is the functor `X ↦ inl X`. -/
@[simps! obj]
def inl_ : C ⥤ C ⊕ D where
obj X := inl X
map f := ULift.up f
