English
A formula expressing that unitCompPartialBijective is equal to the transitive composition of unitCompPartialBijectiveAux with the appropriate isomorphisms from essImage witnesses and reflector adjunction.
Русский
Формула, выражающая равенство unitCompPartialBijective и композиции через unitCompPartialBijectiveAux и соответствующие izomorphisms
LaTeX
$$unitCompPartialBijective A hB = Equiv.instTrans.trans (Equiv.instTrans.trans ((Iso.refl A).homCongr hB.getIso.symm) (unitCompPartialBijectiveAux A hB.witness)) ((Iso.refl (i.obj ((reflector i).obj A))).homCongr hB.getIso)$$
Lean4
theorem unitCompPartialBijective_natural [Reflective i] (A : C) {B B' : C} (h : B ⟶ B') (hB : i.essImage B)
(hB' : i.essImage B') (f : A ⟶ B) :
(unitCompPartialBijective A hB') (f ≫ h) = unitCompPartialBijective A hB f ≫ h := by
rw [← Equiv.eq_symm_apply, unitCompPartialBijective_symm_natural A h hB, Equiv.symm_apply_apply]
