proposition: Lemma loop_dinatural {a b c c'} (f : C (bif c a) (bif c' b)) (g : C c' c) : loop (f >>> bimap g (id_ _)) ⩯ loop (bimap g (id_ _) >>> f).
proof: Proof. unfold loop. transitivity (inr_ >>> iter (bimap g (id_ a) >>> inl_ >>> case_ (f >>> bimap inl_ (id_ b)) inr_)). - rewrite iter_dinatural. cat_auto. do 2 cat_auto_step. cat_auto. - cat_auto. Qed.
imports: Coq(Setoid Morphisms) ITree.Basics(CategoryOps CategoryTheory)