proposition: Lemma otarget_ple : forall x, ob c x -> otarget (ple x) = b.
proof: Proof. ir. uf otarget. rw target_ple. assert (ob (functor_cat a b) (fob f x)). wr F2. app ob_fob. rwi ob_functor_cat H0. uh H0; ee. am. am. am. Qed.
imports: Arith colimits functor_cat