fact: Definition Cat_Iso_FullyFaithful `(iso : C ≅ D) : let φ := to iso in let ψ := from iso in let η x := to (`1 (iso_from_to iso) x) in let μ x := to (`1 (iso_to_from iso) x) in (∀ x, fmap[φ] (η x) ≈ μ (φ x)) -> (∀ x, fmap[ψ] (μ x) ≈ η (ψ x)) -> Isomorphism_FullyFaithful iso := fun H0 H1 => {| to_full := Cat_Iso_to_Full iso H0 ; from_full := Cat_Iso_from_Full iso H1 ; to_faithful := Cat_Iso_to_Faithful iso ; from_faithful := Cat_Iso_from_Faithful iso |}.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor