proposition: Lemma constant_nt_twoarrow_nt : forall a b u, a = twoarrow_cat -> mor b u -> constant_nt a b u = twoarrow_nt b (id b (source u)) (id b (source u)) (id b (target u)) (id b (target u)) u u.
proof: Proof. ir. rw H. ap eq_twoarrow_nt. app constant_nt_axioms. ap twoarrow_cat_axioms. uh H0; ee; am. rww osource_constant_nt. rww otarget_constant_nt. rw source_constant_nt. rw fmor_constant_functor. tv. ap mor_twoarrow_cat. rw source_constant_nt. rw fmor_constant_functor. tv. ap mor_twoarrow_cat. rw target_constant_nt. rw fmor_constant_functor. tv. ap mor_twoarrow_cat. rw target_constant_nt. rw fmor_constant_functor. tv. ap mor_twoarrow_cat. rww ntrans_constant_nt. ap ob_twoarrow_cat. rww ntrans_constant_nt. ap ob_twoarrow_cat. Qed.
imports: Arith cat_examples cardinal fc_limits