proposition: Lemma Adj_FunFreeMon_FunForget : FunFreeMon =_F Adjoint LeftAdj_FunForget.
proof: Proof. unfold Equal_Functor in |- *; intros A B f. apply Build_Equal_hom; simpl in |- *. unfold Equal_MonMor in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *; intro l. elim l; simpl in |- *. trivial. intros c t H; split. apply Refl. trivial. Qed.
imports: FunFreeMon FunForget_UA Th_Adjoint