proposition: Corollary unit_identity : to (@unit_left _ _ I) ≈ to (@unit_right _ _ I).
proof: Proof. pose proof (@bimap_id_unit_left I I I). pose proof (@triangle_identity _ _ I I). normal. rewrite id_unit_left in X0. rewrite <- X0 in X; clear X0. apply tensor_id_left_inj in X. apply tensor_id_right_inj in X. apply X. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Functor.Bifunctor Category.Structure.Monoidal