proposition: Lemma Teta_arrow_map_law : Map_law Teta_arrow.
proof: Proof. unfold Map_law, Teta_arrow in |- *. intros f g H. unfold FOb at 1 in |- *; simpl in |- *; unfold Id_CAT_ob in |- *. apply Comp_l. unfold Comp_FOb in |- *; apply FPres; assumption. Qed.
imports: IdCAT Adj_UA