proposition: Lemma another_same : another_map = our_map.
proof: Proof. assert (lem0: Nat_Trans.axioms another_map). cp mor_another. rwi mor_functor_cat H. lu. am. am. ap Nat_Trans.axioms_extensionality. am. cp mor_our_map. rwi mor_functor_cat H. lu. am. am. rw source_another. rw source_our_map. tv. rw target_another. rww target_our_map. ir. rwi osource_another H. rw ntrans_our_map. ap pointwise_same. am. am. Qed.
imports: Arith colimits functor_cat