proposition: Lemma Id_com_law : forall axf : Com_ob, Com_law (Id (Ob_com_ob axf)).
proof: Proof. intro axf; unfold Com_law in |- *. apply Trans with (Mor_com_ob axf o Id (G (Ob_com_ob axf))). apply Idr. apply Comp_l; apply FId1. Qed.
imports: Functor