proposition: Lemma Cldiese_map : forall (c : C) (tau1 tau2 : CoCone F c), tau1 =_NT tau2 -> Colim_diese l tau1 =_S Colim_diese l tau2.
proof: Proof. intros c tau1 tau2 p. apply (Prf_colimit2 l (tau:=tau2) (g:=Colim_diese l tau1)). unfold CoLimit_eq in |- *; intro i. apply Trans with (tau1 i). apply (Prf_colimit1 l tau1). apply (p i). Qed.
imports: Limit