fact: Definition e (x y: Object): Equiv (x ⟶ y) := λ f g, ∀ i, f i = g i.
imports: MathClasses.interfaces.abstract_algebra Coq.Logic.ChoiceFacts MathClasses.interfaces.functors MathClasses.theory.categories MathClasses.categories.categories