proposition: Lemma ple_commutation : forall u, mor c u -> vcompose (fmor f u) (ple (source u)) = ple (target u).
proof: Proof. ir. assert (ob c (source u)). rww ob_source. assert (ob c (target u)). rww ob_target. ap Nat_Trans.axioms_extensionality. rww vcompose_axioms. app axioms_fmor_f. app nat_trans_axioms_ple. rww target_ple. rww source_fmor. app nat_trans_axioms_ple. rw source_vcompose. rw source_ple. rw source_ple. tv. rw target_vcompose. rw target_ple. rw target_fmor. tv. am. am. ir. rwi osource_vcompose H2. rwi osource_ple H2. rww ntrans_vcompose. rww otarget_fmor_f. rww ntrans_ple. rww ntrans_ple. assert (b = cone_target (pointl x)). rww cone_target_pointl. assert (ntrans (fmor f u) x = fmor (socle (pointl x)) u). rw socle_pointl. uf pointf. rw fmor_fcompose. rw fmor_point_functor. tv. wr F2; app mor_fmor. app point_functor_axioms. am. rww source_point_functor. sy; am. am. am. rw H3. rw H4. rw Limit.commutativity. tv. rww cone_source_pointl. app is_cone_pointl. rww osource_ple. Qed.
imports: Arith colimits functor_cat