proposition: Lemma oppf'_constant_functor : forall a b x, Category.axioms a -> ob b x -> oppf' (constant_functor a b x) = constant_functor (opp a) (opp b) x.
proof: Proof. ir. assert (Category.axioms b). lu. ap constant_functor_criterion. rw source_oppf'. rw source_constant_functor. tv. rw target_oppf'. rw target_constant_functor. tv. ap oppf'_axioms. ap constant_functor_axioms. am. am. am. rww ob_opp. ir. rw fmor_oppf'. rw fmor_constant_functor. rw id_opp. tv. rw ob_opp. am. wr mor_opp. am. rw source_oppf'. rw source_constant_functor. am. Qed.
imports: Arith category