From Categories Require Export Basic_Cons.Facts.Init_Prod.
From Categories Require Export Basic_Cons.Facts.Term_Prod.
From Categories Require Export Basic_Cons.Facts.Equalizer_Monic.
From Categories Require Export Basic_Cons.Facts.Adjuncts.

