proposition: Lemma ntrans_point_trans : forall a b u y, mor a u -> ob (functor_cat a b) y -> ntrans (point_trans a b u) y = fmor y u.
proof: Proof. ir. uf point_trans. rww ntrans_create. rw source_point_functor. change (is_ob (functor_cat a b) y). lu. Qed.
imports: Arith nat_trans