proposition: Lemma fmor_edge_edge_restr : forall x u, ob c x -> mor a u -> comp b (fmor (fob f x) u) (edge (pointl (source u)) x) = comp b (edge (pointl (target u)) x) (restr u).
proof: Proof. ir. uf restr. transitivity (edge (cone_compose (pointl (target u)) (cone_to_limit (newcone u) (pointl (target u)))) x). rw cone_compose_cone_to_limit. uf newcone. rw edge_cone_transform. rw ntrans_htrans_right. rw ntrans_point_trans. rw cone_target_pointl. tv. rww ob_source. am. wr F2. app ob_fob. rww F1. rw osource_htrans_right. rww F1. uhg; ee. app is_cone_pointl. rww ob_source. app htrans_right_axioms. app point_trans_axioms. rww osource_point_trans. sy; am. rw source_htrans_right. rw source_point_trans. rw socle_pointl. tv. rww ob_source. app is_cone_newcone. app is_limit_pointl. rww ob_target. rw socle_newcone. rww socle_pointl. rww ob_target. am. rw edge_cone_compose. rw cone_target_pointl. tv. rww ob_target. rw cone_source_pointl. am. rww ob_target. uhg; ee. app is_cone_pointl. rww ob_target. rw cone_target_pointl. app mor_cone_to_limit. app is_cone_newcone. app is_limit_pointl. rww ob_target. rww socle_newcone. rww socle_pointl. rww ob_target. rww cone_target_pointl. rww ob_target. rww ob_target. rww target_cone_to_limit. app is_cone_newcone. app is_limit_pointl. rww ob_target. rww socle_newcone. rww socle_pointl. rww ob_target. Qed.
imports: Arith colimits functor_cat