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