fact: Hypothesis has_op : forall C : cat, P C.1^op.
imports: Category.Core Functor.Core Category.Dual Functor.Dual Functor.Composition.Core Functor.Identity Cat.Core Functor.Paths Basics.Trunc Types.Sigma HoTT.Tactics Types.Forall