fact: Structure Product : Type := {Pi : C; Proj : forall i : I, Pi --> a i; Pd_diese : forall r : C, (forall i : I, r --> a i) -> (r --> Pi); Prf_pd_law1 : Product_law1 Proj Pd_diese; Prf_pd_law2 : Product_law2 Proj Pd_diese}.
imports: Category BasicTypes