proposition: Lemma Diag_comp_law : Fcomp_law Diag_map.
proof: Proof. unfold Fcomp_law, Diag_map, Diag_mor in |- *; simpl in |- *. unfold Equal_Pmor in |- *; simpl in |- *. intros a b c f g; split; apply Refl. Qed.
imports: PROD Functor