proposition: Lemma arrows_between_isomorphic_objects (a b c d: X) (ab: a ⟶ b) (ba: b ⟶ a) (cd: c ⟶ d) (dc: d ⟶ c) (ac: a ⟶ c) (bd: b ⟶ d): iso_arrows ab ba → iso_arrows cd dc → ac ◎ ba = dc ◎ bd → bd ◎ ab = cd ◎ ac.
proof: Proof. intros [H1 H4] [H2 H5] H3. rewrite <- (left_identity (bd ◎ ab)). rewrite <- H2. rewrite <- associativity. rewrite (associativity dc bd ab). rewrite <- H3. rewrite <- associativity. rewrite H4. rewrite right_identity. reflexivity. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.theory.setoids MathClasses.interfaces.functors MathClasses.theory.jections