proposition: Corollary Cat_Iso_from_Full `(iso : C ≅ D) : 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)) -> Full (from iso).
proof: Proof. apply (Cat_Iso_to_Full (iso_sym iso)). Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor