proposition: Theorem Diagonal_Product_Two (C : Category) : (∀ x, Diagonal_Product C x ≅ (Diagonal Two_Discrete x TwoDX, Diagonal Two_Discrete x TwoDY)) * (∀ x y (f : x ~> y), fmap[Diagonal_Product C] f ≈ (transform[fmap[Diagonal Two_Discrete] f] TwoDX, transform[fmap[Diagonal Two_Discrete] f] TwoDY)).
proof: Proof. split; intros. - isomorphism; simpl; intros; try exact (id, id); cat. - reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Natural.Transformation Category.Construction.Product Category.Instance.Fun Category.Instance.One Category.Instance.Two.Discrete