proposition: Lemma discrete_functor_axioms : forall z a f, discrete_functor_property z a f -> Functor.axioms (discrete_functor z a f).
proof: Proof. ir. uf discrete_functor. ap Functor.create_axioms. sh (fob (discrete_functor z a f)). cp H. uh H0; ee. uhg; ee. ap discrete_cat_axioms. am. ir. cp H2. rwi ob_discrete_cat H3. rww fob_discrete_functor. au. ir. cp H2. rwi ob_discrete_cat H3. rww fob_discrete_functor. rww source_id. ir. cp H2. rwi mor_discrete_cat3 H3. ee. ap mor_id. ap H1. am. ir. cp H2. rwi mor_discrete_cat3 H3. ee. rww source_id. rww fob_discrete_functor. app H1. ir. cp H2. rwi mor_discrete_cat3 H3. ee. rww target_id. rww fob_discrete_functor. rww H5. au. ir. cp H2; cp H3. rwi mor_discrete_cat3 H5; rwi mor_discrete_cat3 H6. ee. rw left_id. rww source_comp. au. app mor_id. au. rww target_id. rww H4. rww H8. au. tv. Qed.
imports: Arith ordinal nat_trans