proposition: Lemma eq_discrete_functor : forall z a f g, Functor.axioms g -> discrete_functor_property z a f -> source g = discrete_cat z -> target g = a -> (forall x, inc x z -> fob g x = f x) -> g = discrete_functor z a f.
proof: Proof. ir. assert (forall x, inc x z -> fmor g (id (discrete_cat z) x) = id a (f x)). ir. rw fmor_id. rww H3. rww H2. am. am. rww ob_discrete_cat. ap Functor.axioms_extensionality. am. ap discrete_functor_axioms. am. rww source_discrete_functor. rww target_discrete_functor. ir. rww fmor_discrete_functor. rwi H1 H5. rwi mor_discrete_cat3 H5. ee. rw H9. rw H4. rw source_id. tv. rww ob_source. rw mor_discrete_cat; ee; am. am. wrr H1. Qed.
imports: Arith ordinal nat_trans