proposition: Lemma eq_empty_functor : forall a f, Functor.axioms f -> source f = empty_cat -> target f = a -> f = empty_functor a.
proof: Proof. ir. ap Functor.axioms_extensionality. am. ap empty_functor_axioms. wr H1. rww category_axioms_target. rww source_empty_functor. rww target_empty_functor. ir. rwi H0 H2. rwi mor_empty_cat H2. elim H2. Qed.
imports: Arith ordinal nat_trans