Require Export FunFreeMon.
Require Export FunForget_UA.
Require Export Th_Adjoint.

Set Implicit Arguments.
Unset Strict Implicit.

Definition LeftAdj_FunForget := LeftAdjUA UA_FM.

Lemma Adj_FunFreeMon_FunForget : FunFreeMon =_F Adjoint LeftAdj_FunForget.
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.