make_product =
fun (C_Ob : Type) (C_Hom : C_Ob -> C_Ob -> Type)
  (C_Hom_eq : forall X Y : C_Ob, Relation (C_Hom X Y))
  (C : Category C_Hom C_Hom_eq) (A B : C_Ob)
  (AxB : Comma_Ob (DiagonalFunctor TWO C)
           (Constant_Functor ONE (Funct TWO C) (F C A B)))
  (AxB_is_product : Product AxB) (X : C_Ob) (f : C_Hom X A)
  (g : C_Hom X B) =>
pi1
  (pi1
     (proj1
        (AxB_is_product
           (witness
              (fun X0 : C_Ob =>
               Sigma
                 (fun Y : True =>
                  NaturalTransformation (DiagonalFunctor TWO C @ X0)
                    (Constant_Functor ONE (Funct TWO C) (F C A B) @ Y))) X
              (witness
                 (fun Y : True =>
                  NaturalTransformation (DiagonalFunctor TWO C @ X)
                    (Constant_Functor ONE (Funct TWO C) (F C A B) @ Y)) I
                 (atrlatrsouasdr C A B X f g))))))
     : forall (C_Ob : Type) (C_Hom : C_Ob -> C_Ob -> Type)
         (C_Hom_eq : forall X Y : C_Ob, Relation (C_Hom X Y))
         (C : Category C_Hom C_Hom_eq) (A B : C_Ob)
         (AxB : Comma_Ob (DiagonalFunctor TWO C)
                  (Constant_Functor ONE (Funct TWO C) (F C A B))),
       Product AxB ->
       forall X : C_Ob, C_Hom X A -> C_Hom X B -> C_Hom X (pi1 AxB)