proposition: Lemma our_mval_carre : forall u, mor a u -> comp b (fmor plv u) (our_mval (source u)) = comp b (our_mval (target u)) (fmor otherv u).
proof: Proof. ir. uf our_mval. rw fmor_plv. assert (ob_src : ob a (source u)). rww ob_source. assert (ob_trg : ob a (target u)). rww ob_target. assert (mor_restr_u : mor b (restr u)). ap mor_restr. am. assert (mor_fmor_otherv : mor b (fmor otherv u)). app weak_mor_fmor. ap axioms_otherv. rww target_otherv. rww source_otherv. assert (lem1: is_limit (pointl (target u))). ap is_limit_pointl. am. cp lem1. uh H0; ee. uh H0; ee. ap H2. uhg; ee. app is_cone_pointl. rww cone_target_pointl. rw mor_comp. tv. am. ap mor_cone_to_limit. app is_cone_other_pt. app is_limit_pointl. rww socle_other_pt. rww socle_pointl. rww cone_target_pointl. rww source_restr. rw target_cone_to_limit. rw vertex_pointl. tv. app is_cone_other_pt. app is_limit_pointl. rww socle_other_pt. rww socle_pointl. tv. rw target_comp. rww target_restr. am. ap mor_cone_to_limit. app is_cone_other_pt. app is_limit_pointl. rww socle_other_pt. rww socle_pointl. rww cone_target_pointl. rww source_restr. rw target_cone_to_limit. rww vertex_pointl. app is_cone_other_pt. app is_limit_pointl. rww socle_other_pt. rww socle_pointl. uhg; ee. app is_cone_pointl. rww cone_target_pointl. rw mor_comp. tv. ap mor_cone_to_limit. app is_cone_other_pt. app is_limit_pointl. rww socle_other_pt. rww socle_pointl. rww cone_target_pointl. assert (b = (target otherv)). rww target_otherv. rw H3. app mor_fmor. app axioms_otherv. rw source_otherv. am. rw source_cone_to_limit. rw vertex_other_pt. rw target_fmor. tv. ap axioms_otherv. rww source_otherv. am. app is_cone_other_pt. app is_limit_pointl. rww socle_other_pt. rww socle_pointl. tv. rw target_comp. rw target_cone_to_limit. tv. app is_cone_other_pt. app is_limit_pointl. rww socle_other_pt. rww socle_pointl. ap mor_cone_to_limit. app is_cone_other_pt. am. rww socle_other_pt. rww socle_pointl. rww cone_target_pointl. app weak_mor_fmor. app axioms_otherv. rww target_otherv. rww source_otherv. rw source_cone_to_limit. rww vertex_other_pt. rw target_fmor. tv. ap axioms_otherv. rww source_otherv. app is_cone_other_pt. am. rww socle_other_pt. rww socle_pointl. assert (lem2 : b = cone_target (pointl (target u))). rw cone_target_pointl. tv. am. rw lem2. wr cone_compose_cone_compose. wr cone_compose_cone_compose. rw cone_compose_cone_to_limit. uf restr. rw cone_compose_cone_to_limit. uf newcone. rw cone_compose_cone_transform. assert (cone_compose (pointl (source u)) (cone_to_limit (other_pt (source u)) (pointl (source u))) = other_pt (source u)). rw cone_compose_cone_to_limit. tv. app is_cone_other_pt. app is_limit_pointl. rww socle_other_pt. rww socle_pointl. rw H3. uf other_pt. ap cone_extensionality. ap is_cone_cone_transform. uhg; ee. ap is_cone_cone_pushdown. am. app point_functor_axioms. rww source_point_functor. rww cone_target_other. ap htrans_right_axioms. am. app point_trans_axioms. rww osource_point_trans. sy; am. rw source_htrans_right. rw source_point_trans. rw socle_cone_pushdown. rww socle_other. rww is_cone_cone_compose. uhg; ee. app is_cone_cone_pushdown. app point_functor_axioms. rww source_point_functor. sy; rww cone_target_other. rww cone_target_cone_pushdown. rww target_point_functor. rw vertex_cone_pushdown. rw fob_point_functor. rw target_fmor. tv. ap axioms_otherv. rww source_otherv. am. am. rw ob_functor_cat. uhg; ee. ap axioms_otherv. ap source_otherv. ap target_otherv. am. am. am. rw vertex_cone_transform. rw vertex_cone_pushdown. rw vertex_cone_compose. rw fob_point_functor. rw source_fmor. tv. ap axioms_otherv. rww source_otherv. am. am. rw ob_functor_cat. uhg; ee. ap axioms_otherv. ap source_otherv. ap target_otherv. am. am. am. rw socle_cone_transform. rw target_htrans_right. rw socle_cone_compose. rw socle_cone_pushdown. rw target_point_trans. rww socle_other. ir. rwi cone_source_cone_transform H4. rwi cone_source_cone_pushdown H4. rwi cone_source_other H4. assert (lem3 : source (edge other x) = otherv). rw source_edge. tv. rw cone_source_other. am. am. assert (lem4 : target (edge other x) = fob f x). rww target_edge. rw socle_other. tv. rww cone_source_other. assert (lem5 : otarget (edge other x) = b). uf otarget. rw lem4. rw target_fob_f. tv. am. assert (lem6 : osource (edge other x) = a). uf osource. rw lem3. rw source_otherv. tv. assert (lem7 : Nat_Trans.axioms (edge other x)). assert (nt2hom a b (edge other x)). wr mor_functor_cat. wr F2. wr socle_other. change (mor (cone_target other) (edge other x)). ap mor_edge. rww cone_source_other. am. am. am. lu. assert (lem8 : mor (functor_cat a b) (edge other x)). rw mor_functor_cat. uhg; ee. am. am. am. am. am. assert (lem9 : ob (functor_cat a b) (fob f x)). rw ob_functor_cat. uhg; ee. app axioms_fob_f. rww source_fob_f. rww target_fob_f. am. am. rw edge_cone_transform. rw cone_target_cone_pushdown. rw target_point_functor. rw ntrans_htrans_right. rw ntrans_point_trans. rw edge_cone_pushdown. rw fmor_point_functor. rw edge_cone_compose. rw cone_target_cone_pushdown. rw target_point_functor. rw edge_cone_pushdown. rw fmor_point_functor. wr lem5; wr lem4; wr lem3; sy. ap carre. am. rww lem6. wr F2. wr socle_other. change (mor (cone_target other) (edge other x)). ap mor_edge. rww cone_source_other. am. rww cone_source_other. am. rw cone_source_cone_pushdown. rww cone_source_other. uhg; ee. app is_cone_cone_pushdown. app point_functor_axioms. rww source_point_functor. rww cone_target_other. rww cone_target_cone_pushdown. rww target_point_functor. rww vertex_cone_pushdown. rww fob_point_functor. rww target_fmor. ap axioms_otherv. rww source_otherv. rw ob_functor_cat. uhg; ee. ap axioms_otherv. ap source_otherv. ap target_otherv. am. am. am. rww cone_source_other. am. am. am. am. rw osource_htrans_right. am. uhg; ee. app is_cone_cone_pushdown. app point_functor_axioms. rww source_point_functor. rww cone_target_other. app htrans_right_axioms. app point_trans_axioms. rww osource_point_trans. sy; am. rw source_htrans_right. rw source_point_trans. rw socle_cone_pushdown. rww socle_other. uhg; ee. app is_cone_cone_pushdown. app point_functor_axioms. rww source_point_functor. rww cone_target_other. app htrans_right_axioms. app point_trans_axioms. rww osource_point_trans. sy; am. rw source_htrans_right. rw source_point_trans. rw socle_cone_pushdown. rww socle_other. app is_cone_pointl. uhg; ee. app is_cone_pointl. rw cone_target_pointl. ap mor_cone_to_limit. app is_cone_other_pt. app is_limit_pointl. rww socle_other_pt. rww socle_pointl. rww cone_target_pointl. am. rw target_cone_to_limit. tv. app is_cone_other_pt. app is_limit_pointl. rww socle_other_pt. rww socle_pointl. uhg; ee. app is_cone_pointl. 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. am. app is_cone_newcone. app is_limit_pointl. rw socle_newcone. rww socle_pointl. am. app is_cone_other_pt. app is_limit_pointl. rww socle_other_pt. rww socle_pointl. uhg; ee. app is_cone_pointl. rw cone_target_pointl. ap mor_cone_to_limit. app is_cone_other_pt. app is_limit_pointl. rww socle_other_pt. rww socle_pointl. rww cone_target_pointl. am. rw target_cone_to_limit. tv. app is_cone_other_pt. app is_limit_pointl. rww socle_other_pt. rww socle_pointl. ap show_composable. rw cone_target_pointl. ap mor_cone_to_limit. app is_cone_other_pt. app is_limit_pointl. rww socle_other_pt. rww socle_pointl. rww cone_target_pointl. am. rw cone_target_pointl. am. am. rw source_cone_to_limit. rw vertex_other_pt. rw target_fmor. tv. ap axioms_otherv. rww source_otherv. am. app is_cone_other_pt. app is_limit_pointl. rww socle_other_pt. rww socle_pointl. uhg; ee. app is_cone_pointl. rww cone_target_pointl. rww vertex_pointl. rww target_restr. ap show_composable. rww cone_target_pointl. rw cone_target_pointl. ap mor_cone_to_limit. app is_cone_other_pt. app is_limit_pointl. rww socle_other_pt. rww socle_pointl. rww cone_target_pointl. am. rw target_cone_to_limit. rw vertex_pointl. rww source_restr. app is_cone_other_pt. app is_limit_pointl. rww socle_other_pt. rww socle_pointl. am. Qed.
imports: Arith colimits functor_cat