proposition: Lemma empty_functor_axioms : forall a, Category.axioms a -> Functor.axioms (empty_functor a).
proof: Proof. ir. uf empty_functor. ap Functor.create_axioms. sh (fun (x:E) => x). uhg; ee. ap empty_cat_axioms. am. ir. rwi ob_empty_cat H0; nin H0. ir. rwi ob_empty_cat H0; elim H0. ir. rwi mor_empty_cat H0; elim H0. ir. rwi mor_empty_cat H0; elim H0. ir. rwi mor_empty_cat H0; elim H0. ir. rwi mor_empty_cat H0; elim H0. Qed.
imports: Arith ordinal nat_trans