proposition: Proposition id_unit_right {x} : unit_right ⨂ id ≈ @unit_right _ _ (x ⨂ I).
proof: Proof. assert (unit_right ∘ unit_right ⨂ id << (x ⨂ I) ⨂ I ~~> x >> unit_right ∘ unit_right) by (rewrite to_unit_right_natural; reflexivity). symmetry. do 2 (rewrite <- id_left; symmetry). rewrite <- (iso_from_to unit_right). rewrite <- !comp_assoc. rewrites; reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Functor.Bifunctor Category.Structure.Monoidal