proposition: Lemma all_functors_discrete : forall z g, Functor.axioms g -> source g = discrete_cat z -> g = discrete_functor z (target g) (fob g).
proof: Proof. ir. app eq_discrete_functor. app discrete_functor_property_fob. Qed.
imports: Arith ordinal nat_trans