fact: Definition is_cocone c := cocone_like c & Nat_Trans.axioms (coedge_nt c) & ob (cocone_target c) (vertex c) & target (coedge_nt c) = constant_functor (cocone_source c) (cocone_target c) (vertex c).
imports: Arith limits