proposition: Lemma versal_summary : source our_map = otherv & target our_map = plv & mor (functor_cat a b) our_map & cone_compose plc our_map = other.
proof: Proof. ee. ap source_our_map. ap target_our_map. ap mor_our_map. ap cone_compose_our_map. Qed.
imports: Arith colimits functor_cat