proposition: Lemma for_uni_plc : forall u, cone_composable plc u -> u = our_map (cone_compose plc u).
proof: Proof. ir. assert (is_cone (cone_compose plc u)). rww is_cone_cone_compose. assert (socle (cone_compose plc u) = f). rw socle_cone_compose. rw socle_plc. tv. ap (another_same H0 H1). uh H; ee. rwi cone_target_plc H2. am. uf otherv. rw vertex_cone_compose. tv. uh H; ee. rw H3. rw vertex_plc. tv. tv. Qed.
imports: Arith colimits functor_cat