proposition: Theorem Category_is_Enriched_over_Set : Enriched Sets ↔ Category.
proof: Proof. split; intros. - unshelve refine {| obj := eobj ; hom := @ehom _ _ X ; homset := @ehom _ _ X ; id := fun x => @eid _ _ X x ttt ; compose := fun x y z f g => @ecompose _ _ X x y z (f, g) |}. + intros. proper. destruct X. simpl in *. destruct (ecompose0 x y z). simpl in *. now apply proper_morphism; simpl; auto. + intros. destruct X. simpl in *. now sapply (eid_left0 x y (ttt, f)). + intros. destruct X. simpl in *. now sapply (eid_right0 x y (f, ttt)). + intros. destruct X. simpl in *. symmetry. now sapply (ecompose_assoc0 x y z w ((f, g), h)). + intros. destruct X. simpl in *. now sapply (ecompose_assoc0 x y z w ((f, g), h)). - unshelve refine (@Build_Enriched Sets Sets_Product_Monoidal obj (fun x y : X => {| carrier := x ~> y |}) (fun x => {| morphism := fun _ => id[x] |}) (fun x y z => {| morphism := fun p => fst p ∘ snd p |}) _ _ _). + now apply homset. + now proper. + proper; simpl. apply compose_respects; now match goal with [ H : _ ≈ _ |- _ ] => apply H end. + now simpl; intros; cat. + now simpl; intros; cat. + now simpl; intros; cat. Defined.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Structure.Monoidal Category.Instance.Sets