proposition: Theorem cat_from_loop {a b c} (ab : C a b) (bc : C b c) : loop (swap >>> bimap ab bc) ⩯ ab >>> bc.
proof: Proof. rewrite bimap_slide. rewrite <- cat_assoc. rewrite <- loop_natural_right. rewrite swap_bimap. rewrite <- !cat_assoc. rewrite swap_involutive, cat_id_l. rewrite <- loop_natural_left. rewrite loop_yanking. rewrite cat_id_r. reflexivity. Qed.
imports: Coq(Setoid Morphisms) ITree.Basics(CategoryOps CategoryTheory)