fact: Record Isomorphism_FullyFaithful `(iso : C ≅ D) := { to_full : Full (to iso); to_faithful : Faithful (to iso); from_full : Full (from iso); from_faithful : Faithful (from iso) }.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor