proposition: Fact bimap_id_pure {A B C} (f : B -> C) : bimap (id_ A) (pure f) ⩯ pure (bimap (id_ A) f).
proof: Proof. unfold bimap, Bimap_Coproduct. rewrite !cat_id_l. rewrite <- !case_pure. rewrite <- !compose_pure. rewrite <- pure_id. rewrite !cat_id_l. reflexivity. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) ExtLib(Structures.Monad) ITree(Basics.Basics Basics.Category Basics.Monad Basics.CategoryFunctor Basics.CategoryKleisli Basics.Function)