proposition: Lemma is_cocone_cocone_create2 : forall f v e, Functor.axioms f-> ob (target f) v-> (forall x, ob (source f) x -> mor (target f) (e x)) -> (forall x, ob (source f) x -> target (e x) = v) -> (forall x, ob (source f) x -> source (e x) = (fob f x)) -> (forall u, mor (source f) u -> comp (target f) (e (target u)) (fmor f u) = e (source u)) -> is_cocone (cocone_create2 f v e).
proof: Proof. ir. uf cocone_create2. uhg; ee. ap cocone_like_cocone_create. rw coedge_nt_cocone_create. app Nat_Trans.create_axioms. uhg; ee. am. app constant_functor_axioms. uh H; ee; am. uh H; ee; am. rww source_constant_functor. rww target_constant_functor. ir. rw target_constant_functor. au. ir. au. ir. rw fob_constant_functor. au. am. am. ir. rw target_constant_functor. rww fmor_constant_functor. rww H4. rww left_id. ap H1. rww ob_source. rw H2. tv. rww ob_source. rw vertex_cocone_create. uf cocone_target. uf cosocle. rw coedge_nt_cocone_create. rw source_create. am. rw coedge_nt_cocone_create. rw target_create. rw vertex_cocone_create. uf cocone_source; uf cocone_target; uf cosocle; rw coedge_nt_cocone_create. rw source_create. tv. Qed.
imports: Arith limits