ITree.Core.KTree
Implicit Types E : Type -> Type.
Implicit Types a b : Type.
Notation ktree E := (Kleisli (itree E)).
(*
The following line removes the warning on >=8.10, but is incompatible for <8.10
*)
(* Declare Scope ktree_scope. *)
Declare Scope ktree_scope.
Bind Scope ktree_scope with ktree.
Notation ktree_apply := (@Kleisli_apply (itree _)).
Notation lift_ktree := (@pure (itree _) _ _ _).
Notation lift_ktree_ E a b := (@pure (itree E) _ a b).
(* ktree E forms an iterative category, i.e. a cocartesian category with a
loop operator *)
(* Obj ≅ Type *)
(* Arrow: A -> B ≅ terms of type (ktree A B) *)
Traced monoidal category
+-----+
| ### |
+-###-+I
A----###----B
###