proposition: Lemma is_cocone_cocone_pullback : forall f c, is_cocone c -> Functor.axioms f -> cocone_source c = target f -> is_cocone (cocone_pullback f c).
proof: Proof. ir. uhg; ee. uf cocone_pullback. ap cocone_like_cocone_create. rw coedge_nt_cocone_pullback. app htrans_right_axioms. uh H; ee. am. rw cocone_target_cocone_pullback. rw vertex_cocone_pullback. app ob_vertex. rw coedge_nt_cocone_pullback. rw target_htrans_right. rw target_coedge_nt. rw fcompose_left_constant_functor. rw cocone_source_cocone_pullback. rw cocone_target_cocone_pullback. rw vertex_cocone_pullback. tv. am. sy; am. app cocone_target_axioms. app ob_vertex. am. Qed.
imports: Arith limits