proposition: Lemma map_inl_case_kleisli: forall (a1 b1 b2 c1 c2 : Type) (f1 : Kleisli m a1 b1) (g1 : Kleisli m b1 c1) (g2 : Kleisli m b2 c2), map inl f1 >>> case_ (map inl g1) (map inr g2) ⩯ map inl (f1 >>> g1).
proof: Proof. intros a1 b1 b2 c1 c2 f1 g1 g2. unfold cat, Cat_Kleisli, case_, Case_Kleisli, case_sum. unfold map. unfold cat, Cat_Kleisli. setoid_rewrite bind_bind. unfold pure. setoid_rewrite bind_ret_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)