proposition: Corollary ump_universal_arrows `(c ⟿ F) `(h : c ~> F d) : ∃! g : arrow_obj ~> d, h ≈ fmap[F] g ∘ arrow.
proof: Proof. unfold arrow_obj, arrow; simpl. destruct (@zero _ arrow_initial ((ttt, d); h)), x. simpl in *. rewrite id_right in e. exists h1. - assumption. - intros. rewrite <- id_right in e. rewrite <- id_right in X. exact (snd (@zero_unique _ arrow_initial ((ttt, d); h) ((ttt, h1); e) ((ttt, v); X))). Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Functor Category.Theory.Adjunction Category.Structure.Initial Category.Theory.Isomorphism Category.Construction.Comma Category.Functor.Diagonal Category.Instance.Sets