proposition: Lemma cocommutativity : forall c u, mor (cocone_source c) u -> is_cocone c -> comp (cocone_target c) (coedge c (target u)) (fmor (cosocle c) u) = coedge c (source u).
proof: Proof. ir. assert (K:is_cocone c). am. uh H0; ee. uf coedge. assert (cocone_target c = otarget (coedge_nt c)). rww otarget_coedge_nt. assert (cosocle c = source (coedge_nt c)). rww source_coedge_nt. assert (lem1: forall y, ntrans (coedge_nt c) y = coedge c y). ir. tv. rw H4; rw H5. rw carre. rw target_coedge_nt. rw fmor_constant_functor. rw left_id. tv. wr H4; am. wr H4. change (mor (cocone_target c) (coedge c (source u))). app mor_coedge. rww ob_source. rw ntrans_coedge_nt. rw target_coedge. tv. rww ob_source. am. rww otarget_coedge_nt. am. am. am. rww osource_coedge_nt. Qed.
imports: Arith limits