Definition Judgments_Category_monoidal_endofunctor_fobj : Judgments_Category ×× Judgments_Category -> Judgments_Category :=
fun xy => (fst_obj _ _ xy),,(snd_obj _ _ xy).
Definition Judgments_Category_monoidal_endofunctor_fmor :
Definition Judgments_Category_monoidal_endofunctor_fobj : Judgments_Category ×× Judgments_Category -> Judgments_Category :=
fun xy => (fst_obj _ _ xy),,(snd_obj _ _ xy).
Definition Judgments_Category_monoidal_endofunctor_fmor :