proposition: Proposition UniversalArrowIsUniversalProperty : IsUniversalProperty D (fun a : D => AUniversalArrow c U a) _.
proof: Proof. exists ((Curried_Hom C c) ◯ U). intro a. repeat(unshelve econstructor; try intro). - simpl in *. destruct X. auto with cat. - abstract(auto with cat). - abstract(auto with cat). - abstract(auto with cat). - simpl in *. destruct X. now apply universal_arrow_universal. - abstract(simpl; intros; apply uniqueness; rewrite (unique_property universal_arrow_universal); easy). - abstract(simpl; intros; symmetry; apply uniqueness; autorewrite with categories; now rewrite (unique_property universal_arrow_universal)). - abstract(simpl; intros; destruct X; simpl; apply uniqueness; autorewrite with categories; apply compose_respects; [ reflexivity |]; apply (unique_property (universal_arrow_universal _ _))). - abstract(simpl; intros; rewrite (unique_property universal_arrow_universal); auto with cat). - abstract(auto with cat). - abstract(auto with cat). - abstract(simpl; intros; apply uniqueness; simpl in X; now rewrite X, (unique_property (universal_arrow_universal ))). - exact (((to X) a) id). - now apply (from X d). - abstract(simpl; set (M := @preyoneda D^op _ d _ (to X)); simpl in M; rewrite <- M; clear M; assert (K := (@iso_to_from _ _ _ X)); simpl in K; rewrite K; now autorewrite with categories). - try( simpl; assert (M := @preyoneda D^op _ d _ (to X)); simpl in M; intro A; rewrite <- M in A; clear M; apply (proper_morphism (from X d)) in A; set (B := (iso_from_to X)); simpl in B; now rewrite B , id_left in A); admit. - abstract(simpl; intros; destruct X as [e ?]; simpl in e; apply e). - abstract(simpl; intro; assert (M := @preyoneda D^op _ x0 _ (to x)); simpl in M; now rewrite <- M). - abstract (auto with cat). - abstract(auto with cat). Defined.
imports: Category.Lib Category.Lib.Tactics2 Category.Theory.Category Category.Theory.Isomorphism Category.Construction.Opposite Category.Theory.Functor Category.Theory.Natural.Transformation Category.Functor.Hom Category.Instance.Sets Category.Structure.UniversalProperty Category.Theory.Universal.Arrow