fact: Definition IterPairing : Prop := forall a b c (f : C a (bif (bif a b) c)) (g : C b (bif (bif a b) c)), let h : C b (bif b c) := g >>> assoc_r >>> case_ (iter (f >>> assoc_r)) (id_ _) in iter (case_ f g) ⩯ iter (case_ (iter (f >>> assoc_r) >>> case_ (iter h) (id_ _) >>> inr_) (h >>> bimap inr_ (id_ _))).
imports: Coq(Setoid Morphisms) ITree.Basics(CategoryOps CategoryFunctor)