fact: Definition are_finverse f g := Functor.axioms f & Functor.axioms g & source f = target g & source g = target f & fcompose f g = fidentity (source g) & fcompose g f = fidentity (source f).
imports: Arith category