proposition: Lemma nat_trans_axioms_ple : forall x, ob c x -> Nat_Trans.axioms (ple x).
proof: Proof. ir. assert (ob (functor_cat a b) (fob f x)). wr F2. app ob_fob. cp H0. rwi ob_functor_cat H1; try am. uh H1; ee. uhg; ee. uf ple. ap create_like. rww osource_ple. rww otarget_ple. rww source_ple. app plv_axioms. rw target_ple. am. rw target_ple. rw H2. rww osource_ple. rw source_ple. rw target_plv. rww otarget_ple. ir. rwi osource_ple H4. rww otarget_ple. rww ntrans_ple. assert (b = cone_target (pointl x0)). rww cone_target_pointl. rw H5. app mor_edge. rww cone_source_pointl. app is_cone_pointl. ir. rwi osource_ple H4. rww source_ple. rww ntrans_ple. rww source_edge. rww vertex_pointl. rww fob_plv. rww cone_source_pointl. app is_cone_pointl. ir. rwi osource_ple H4. rww target_ple. rww ntrans_ple. rww target_edge. rww socle_pointl. uf pointf. rw fob_fcompose. rw fob_point_functor. tv. am. am. am. am. app point_functor_axioms. am. rww source_point_functor. sy; am. am. rww cone_source_pointl. app is_cone_pointl. ir. rwi osource_ple H4. rww otarget_ple. rww target_ple. rw source_ple. rw ntrans_ple. rw ntrans_ple. rw fmor_plv. sy; ap fmor_edge_edge_restr. am. am. am. am. rww ob_source. am. rww ob_target. Qed.
imports: Arith colimits functor_cat