Fibration categories, the propositional J rule and setoids