English
Given isomorphisms app0: f.obj'0 ≅ g.obj'0, app1: f.obj'1 ≅ g.obj'1, app2: f.obj'2 ≅ g.obj'2 and compatibility relations w0, w1, there is an isomorphism f ≅ g built from homMk₂
Русский
Даны изоморфизмы между соответствующими компонентами и когерентности; существует изоморфизм f ≅ g конструктором isoMk₂.
LaTeX
$$$\\exists \\text{iso } f \\cong g \\text{ with } \\text{hom} = \\text{homMk₂} \\;\\text{and } \\text{inv} = \\text{homMk₂} ...$$$
Lean4
/-- Constructor for isomorphisms in `ComposableArrows C 2`. -/
@[simps]
def isoMk₂ {f g : ComposableArrows C 2} (app₀ : f.obj' 0 ≅ g.obj' 0) (app₁ : f.obj' 1 ≅ g.obj' 1)
(app₂ : f.obj' 2 ≅ g.obj' 2) (w₀ : f.map' 0 1 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1)
(w₁ : f.map' 1 2 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2) : f ≅ g
where
hom := homMk₂ app₀.hom app₁.hom app₂.hom w₀ w₁
inv :=
homMk₂ app₀.inv app₁.inv app₂.inv
(by rw [← cancel_epi app₀.hom, ← reassoc_of% w₀, app₁.hom_inv_id, comp_id, app₀.hom_inv_id_assoc])
(by rw [← cancel_epi app₁.hom, ← reassoc_of% w₁, app₂.hom_inv_id, comp_id, app₁.hom_inv_id_assoc])
