proposition: Lemma edge_plc : forall x, ob c x -> edge plc x = ple x.
proof: Proof. ir. uf plc; uf cone_create2. uf edge. rw edge_nt_cone_create. rw ntrans_create. tv. rw source_constant_functor. change (is_ob c x). lu. Qed.
imports: Arith colimits functor_cat