proposition: Lemma fmor_discrete_functor : forall z a f u, mor (discrete_cat z) u -> fmor (discrete_functor z a f) u = id a (f (source u)).
proof: Proof. ir. uf discrete_functor. rww fmor_create. Qed.
imports: Arith ordinal nat_trans