English
Given two index families f1 and f2 and binary cofan bc on their cocone points, one can define a canonical family of morphisms from the sum ι1 ⊕ ι2 to bc.pt by sending inl a to c1.inj a ≫ bc.inl and inr a to c2.inj a ≫ bc.inr.
Русский
Даны две семейства индексов f1 и f2 и бинарный кофан bc на их ко-конечных точках; существует каноническая семья морфизмов из суммы индексов ι1 ⊕ ι2 в bc.pt: в случае inl a отправляем в c1.inj a ≫ bc.inl, в случае inr a — в c2.inj a ≫ bc.inr.
LaTeX
$$$\text{combPairHoms} : (i : ι_1 \oplus ι_2) \to bc.pt$ given by
\begin{cases} c_1.inj a \circ bc.inl & i = \mathsf{inl} \, a, \\ c_2.inj a \circ bc.inr & i = \mathsf{inr} \, a. \end{cases}$$$
Lean4
/-- For cofans on maps `f₁ : ι₁ → C`, `f₂ : ι₂ → C` and a binary cofan on their
cocone points, construct one family of morphisms indexed by `ι₁ ⊕ ι₂` -/
@[simp]
abbrev combPairHoms : (i : ι₁ ⊕ ι₂) → Sum.elim f₁ f₂ i ⟶ bc.pt
| .inl a => c₁.inj a ≫ bc.inl
| .inr a => c₂.inj a ≫ bc.inr
