proposition: Corollary swap_involutive {SwapInvolutive_C : SwapInvolutive} : forall a b, swap >>> swap ⩯ id_ (bif a b).
proof: Proof. intros; apply semi_iso, SwapInvolutive_C. Qed.
imports: Coq(Setoid Morphisms) ITree.Basics(CategoryOps CategoryFunctor)