English
There is an isomorphism f ≅ g between ComposableArrows C 3 given isomorphisms app0, app1, app2, app3 and coherence conditions w0,w1,w2.
Русский
Существует изоморфизм f ≅ g между ComposableArrows C 3, заданный изоморфизмами app0..app3 и когерентностями w0,w1,w2.
LaTeX
$$$\\text{isoMk}_3 : f \\cong g \\text{ with } app_0, app_1, app_2, app_3, w_0, w_1, w_2$$$
Lean4
/-- Constructor for isomorphisms in `ComposableArrows C 3`. -/
@[simps]
def isoMk₃ {f g : ComposableArrows C 3} (app₀ : f.obj' 0 ≅ g.obj' 0) (app₁ : f.obj' 1 ≅ g.obj' 1)
(app₂ : f.obj' 2 ≅ g.obj' 2) (app₃ : f.obj' 3 ≅ g.obj' 3) (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) (w₂ : f.map' 2 3 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3) : f ≅ g
where
hom := homMk₃ app₀.hom app₁.hom app₂.hom app₃.hom w₀ w₁ w₂
inv :=
homMk₃ app₀.inv 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])
(by rw [← cancel_epi app₂.hom, ← reassoc_of% w₂, app₃.hom_inv_id, comp_id, app₂.hom_inv_id_assoc])
