English
There is a canonical constructor that, given a morphism f: X0 → X1, produces a one-step composable arrow F in ComposableArrows C 1 with F.obj determined by X0, X1 and F.map determined by f and the induced structure of maps.
Русский
Существует канонический конструктор, который, задавая морфизм f: X0 → X1, порождает одноблоковую композицию в ComposableArrows C 1, где F.obj задаётся через X0, X1, а F.map определяется через f и индуцированную структуру отображений.
LaTeX
$$$\exists F : ComposableArrows\ C\ 1\,\exists f: X_0 \to X_1 ,\ F = mk_1\ f$$$
Lean4
/-- Constructor for `ComposableArrows C 1`. -/
@[simps]
def mk₁ {X₀ X₁ : C} (f : X₀ ⟶ X₁) : ComposableArrows C 1
where
obj := Mk₁.obj X₀ X₁
map g := Mk₁.map f _ _ (leOfHom g)
map_id := Mk₁.map_id f
map_comp g g' := Mk₁.map_comp f (leOfHom g) (leOfHom g')
