proposition: Lemma cone_pushdown_point_functor_plc : forall y, ob a y -> cone_pushdown (point_functor a b y) plc = pointl y.
proof: Proof. ir. ap cone_extensionality. ap is_cone_cone_pushdown. ap is_cone_plc. app point_functor_axioms. rw source_point_functor. rww cone_target_plc. app is_cone_pointl. rw vertex_cone_pushdown. rw fob_point_functor. rw vertex_pointl. rw vertex_plc. rw fob_plv. tv. am. am. am. rw vertex_plc. rw ob_functor_cat. uhg; ee. ap plv_axioms. rww source_plv. rww target_plv. am. am. am. rw socle_cone_pushdown. rw socle_pointl. rw socle_plc. tv. am. ir. rwi cone_source_cone_pushdown H0. rwi cone_source_plc H0. rw edge_cone_pushdown. rw edge_plc. rw fmor_point_functor. rw ntrans_ple. tv. am. am. rw mor_functor_cat. uhg; ee. app nat_trans_axioms_ple. rww osource_ple. rww otarget_ple. am. am. am. rww cone_source_plc. app is_cone_plc. Qed.
imports: Arith colimits functor_cat