fact: Definition iso_arrows {x y: X} (a: x ⟶ y) (b: y ⟶ x): Prop := a ◎ b = cat_id ∧ b ◎ a = cat_id.
imports: MathClasses.interfaces.abstract_algebra MathClasses.theory.setoids MathClasses.interfaces.functors MathClasses.theory.jections