proposition: Lemma swap_pair (a b c: obj) (f: C a b) (g: C a c) : pair_ f g >>> swap ⩯ pair_ g f.
proof: Proof. intros; unfold swap, Swap_Product. rewrite pair_cat, pair_fst, pair_snd. reflexivity. Qed.
imports: Coq(Setoid Morphisms) ITree.Basics(CategoryOps CategoryTheory)