proposition: Lemma is_cone_cone_pullback : forall f c, is_cone c -> Functor.axioms f -> cone_source c = target f -> is_cone (cone_pullback f c).
proof: Proof. ir. uhg; ee. uf cone_pullback. ap cone_like_cone_create. rw edge_nt_cone_pullback. app htrans_right_axioms. uh H; ee. am. rww osource_edge_nt. rw cone_target_cone_pullback. rw vertex_cone_pullback. app ob_vertex. rw edge_nt_cone_pullback. rw source_htrans_right. rw source_edge_nt. rw fcompose_left_constant_functor. rw cone_source_cone_pullback. rw cone_target_cone_pullback. rw vertex_cone_pullback. tv. am. sy; am. app cone_target_axioms. app ob_vertex. am. Qed.
imports: Arith nat_trans