proposition: Lemma restr_comp : forall u v, composable a u v -> restr (comp a u v) = comp b (restr u) (restr v).
proof: Proof. ir. assert (mu : mor a u). rwi composable_facts_rw H; lu. assert (mv : mor a v). rwi composable_facts_rw H; lu. assert (sutv : source u = target v). rwi composable_facts_rw H; lu. uf restr. assert (osu : ob a (source u)). rww ob_source. assert (otu : ob a (target u)). rww ob_target. assert (osv : ob a (source v)). rww ob_source. assert (otv : ob a (target v)). rww ob_target. transitivity (comp (cone_target (pointl (target u))) (cone_to_limit (newcone u) (pointl (target u))) (cone_to_limit (newcone v) (pointl (target v)))). wr cone_to_limit_cone_compose. rw target_comp. assert (lem1 : (newcone (comp a u v)) = (cone_compose (newcone u) (cone_to_limit (newcone v) (pointl (target v))))). uf newcone. set (uu := htrans_right (point_trans a b u) f). set (vv := htrans_right (point_trans a b v) f). set (uv := htrans_right (point_trans a b (comp a u v)) f). assert (uuax : Nat_Trans.axioms uu). uf uu. ap htrans_right_axioms. am. app point_trans_axioms. rw osource_point_trans. sy; am. assert (vvax : Nat_Trans.axioms vv). uf vv. ap htrans_right_axioms. am. app point_trans_axioms. rw osource_point_trans. sy; am. assert (suu : source uu = pointf (source u)). uf uu; rw source_htrans_right. rw source_point_trans. reflexivity. assert (tuu : target uu = pointf (target u)). uf uu; rw target_htrans_right. rw target_point_trans. reflexivity. assert (svv : source vv = pointf (source v)). uf vv; rw source_htrans_right. rw source_point_trans. reflexivity. assert (tvv : target vv = pointf (target v)). uf vv; rw target_htrans_right. rw target_point_trans. reflexivity. rw source_comp. rw sutv. set (k:= (cone_to_limit (cone_transform vv (pointl (source v))) (pointl (target v)))). assert (cone_compose (cone_transform uu (pointl (target v))) k = cone_transform uu (cone_compose (pointl (target v)) k)). ap cone_compose_cone_transform. app is_cone_pointl. uhg; ee. app is_cone_pointl. rww cone_target_pointl. uf k. ap mor_cone_to_limit. ap is_cone_cone_transform. uhg; ee. app is_cone_pointl. am. rww socle_pointl. app is_limit_pointl. rww socle_cone_transform. rww socle_pointl. rww cone_target_pointl. uf k. rww target_cone_to_limit. app is_cone_cone_transform. uhg; ee. app is_cone_pointl. am. rww socle_pointl. app is_limit_pointl. rww socle_cone_transform. rww socle_pointl. uhg; ee. app is_cone_pointl. am. rw socle_pointl. wr sutv. am. am. rw H0. uf k. assert (cone_compose (pointl (target v)) (cone_to_limit (cone_transform vv (pointl (source v))) (pointl (target v))) = (cone_transform vv (pointl (source v)))). rw cone_compose_cone_to_limit. reflexivity. app is_cone_cone_transform. uhg; ee. app is_cone_pointl. am. rww socle_pointl. app is_limit_pointl. rww socle_cone_transform. rww socle_pointl. rw H1. assert (uv = vcompose uu vv). uf uu; uf vv. rw vcompose_htrans_right_htrans_right. assert (vcompose (point_trans a b u) (point_trans a b v) = point_trans a b (comp a u v)). app vcompose_point_trans. rw H2. reflexivity. app point_trans_axioms. app point_trans_axioms. am. reflexivity. rww source_point_trans. rw target_point_trans. rw sutv. reflexivity. rw osource_point_trans. am. rw H2. rw cone_transform_vcompose. reflexivity. app is_cone_pointl. uhg; ee. app is_cone_pointl. am. rww socle_pointl. am. rw suu. rw tvv. rw sutv. reflexivity. am. am. am. rw lem1. tv. am. am. am. ap is_limit_pointl. am. uhg; ee. app is_cone_newcone. ap mor_cone_to_limit. ap is_cone_newcone. am. ap is_limit_pointl. am. rw socle_newcone. rw socle_pointl. tv. am. am. uf cone_target. rw socle_newcone. rw socle_pointl. rw target_pointf. rw target_pointf. tv. am. am. rw target_cone_to_limit. rw vertex_newcone. rw vertex_pointl. rwi composable_facts_rw H. uh H; ee. rw H4; tv. am. ap is_cone_newcone. am. app is_limit_pointl. rw socle_newcone. rw socle_pointl. tv. am. am. rw socle_newcone. rw socle_pointl. tv. am. am. rw cone_target_pointl. tv. am. Qed.
imports: Arith colimits functor_cat