Set Implicit Arguments.
Unset Strict Implicit.

Variables (C D : Category) (F : Functor D C).

Hypothesis UA_of : c : C, CoUA c F.

Definition CoadjointUA_ob (c : C) := CoUA_ob (UA_of c).

Variable c c' : C.

Definition CoadjointUA_mor (f : c --> c') :=
CoUA_diese (UA_of c') (CoUA_mor (UA_of c) o f).

Proof.
unfold Map_law, CoadjointUA_mor in |- *; intros f g H.
apply
(Codiese_map (UA_of c') (x:=CoUA_mor (UA_of c) o f)
(y:=CoUA_mor (UA_of c) o g)).
apply Comp_l; assumption.
Qed.

Proof.
unfold Fid_law in |- *; simpl in |- ×.
intro c.
apply CoUA_unic1.
apply Trans with (Id (F (CoUA_ob (UA_of c))) o CoUA_mor (UA_of c)).
apply Comp_r; apply FId.
apply Trans with (CoUA_mor (UA_of c)).
apply Idl.
apply Idr.
Qed.

Proof.
unfold Fcomp_law in |- *; simpl in |- ×.
unfold CoadjointUA_mor, CoadjointUA_ob in |- *; intros c1 c2 c3 f g.
apply CoUA_unic1.
apply
Trans
with
((FMor F (CoUA_diese (UA_of c2) (CoUA_mor (UA_of c1) o f))
o FMor F (CoUA_diese (UA_of c3) (CoUA_mor (UA_of c2) o g)))
o CoUA_mor (UA_of c3)).
apply Comp_r; apply FComp.
apply
Trans
with
(FMor F (CoUA_diese (UA_of c2) (CoUA_mor (UA_of c1) o f))
o FMor F (CoUA_diese (UA_of c3) (CoUA_mor (UA_of c2) o g))
o CoUA_mor (UA_of c3)).
apply Ass1.
apply
Trans
with
(FMor F (CoUA_diese (UA_of c2) (CoUA_mor (UA_of c1) o f))
o CoUA_mor (UA_of c2) o g).
apply Comp_l; apply CoUA_diag.

apply
Trans
with
((FMor F (CoUA_diese (UA_of c2) (CoUA_mor (UA_of c1) o f))
o CoUA_mor (UA_of c2)) o g).
apply Ass.

apply Trans with ((CoUA_mor (UA_of c1) o f) o g).
apply Comp_r; apply CoUA_diag.
apply Ass1.
Qed.

Section psi_ua_tau_def.

Variable dxc : POb (Dual D) C.

Definition PsiUA_arrow (f : F (Ob_l dxc) --> Ob_r dxc) :=
CoUA_diese (UA_of (Ob_r dxc)) f.

Lemma PsiUA_arrow_map_law : Map_law PsiUA_arrow.
Proof.
unfold Map_law, PsiUA_arrow in |- ×.
intros f g H.
apply (Codiese_map (UA_of (Ob_r dxc)) (x:=f) (y:=g)).
assumption.
Qed.

Canonical Structure PsiUA_tau := Build_Map PsiUA_arrow_map_law.

End psi_ua_tau_def.

Lemma PsiUA_tau_nt_law :
NT_law (F:=FunSET2_r F) (G:=FunSET2_l CoadjointUA) PsiUA_tau.
Proof.
unfold NT_law, PsiUA_tau, PsiUA_arrow in |- *; simpl in |- ×.
unfold Ext in |- *; simpl in |- ×.
intros d1xc1 d2xc2 fxg h.
unfold FunSET2_r_mor1, FunSET2_l_mor1, FunSET2_l_ob in |- *; simpl in |- *;
apply CoUA_unic1.
apply
Trans
with
((FMor F (HOM_l fxg o CoUA_diese (UA_of (Ob_r d1xc1)) h)
o FMor F (FMor CoadjointUA (Hom_r fxg)))
o CoUA_mor (UA_of (Ob_r d2xc2))).
apply Comp_r; apply FComp.
apply
Trans
with
(((FMor F (HOM_l fxg) o FMor F (CoUA_diese (UA_of (Ob_r d1xc1)) h))
o FMor F (FMor CoadjointUA (Hom_r fxg)))
o CoUA_mor (UA_of (Ob_r d2xc2))).
apply Comp_r; apply Comp_r; apply FComp.
apply
Trans
with
((FMor F (HOM_l fxg) o FMor F (CoUA_diese (UA_of (Ob_r d1xc1)) h))
o FMor F (FMor CoadjointUA (Hom_r fxg))
o CoUA_mor (UA_of (Ob_r d2xc2))).
apply Ass1.
apply
Trans
with
(FMor F (HOM_l fxg)
o FMor F (CoUA_diese (UA_of (Ob_r d1xc1)) h)
o FMor F (FMor CoadjointUA (Hom_r fxg))
o CoUA_mor (UA_of (Ob_r d2xc2))).
apply Ass1.
apply Trans with (FMor F (HOM_l fxg) o h o Hom_r fxg).
apply Comp_l.
apply
Trans
with
(FMor F (CoUA_diese (UA_of (Ob_r d1xc1)) h)
o CoUA_mor (UA_of (Ob_r d1xc1)) o Hom_r fxg).
apply Comp_l.
unfold FMor at 2 in |- *; simpl in |- *;
apply CoUA_diag.
apply
Trans
with
((FMor F (CoUA_diese (UA_of (Ob_r d1xc1)) h)
o CoUA_mor (UA_of (Ob_r d1xc1))) o Hom_r fxg).
apply Ass.
apply Comp_r; apply CoUA_diag.
apply Ass.
Qed.

Canonical Structure PsiUA := Build_NT PsiUA_tau_nt_law.

Section psi_ua_1_tau_def.

Variable dxc : POb (Dual D) C.

Definition PsiUA_1_arrow (f : OB_l dxc --> CoadjointUA (Ob_r dxc)) :=
FMor F f o CoUA_mor (UA_of (Ob_r dxc)).

Lemma PsiUA_1_arrow_map_law : Map_law PsiUA_1_arrow.
Proof.
unfold Map_law, PsiUA_1_arrow in |- ×.
intros f g H.
apply Comp_r; apply FPres; assumption.
Qed.

Canonical Structure PsiUA_1_tau := Build_Map PsiUA_1_arrow_map_law.

End psi_ua_1_tau_def.

Lemma PsiUA_1_tau_nt_law :
NT_law (F:=FunSET2_l CoadjointUA) (G:=FunSET2_r F) PsiUA_1_tau.
Proof.
unfold NT_law, PsiUA_1_tau, PsiUA_1_arrow in |- *; simpl in |- ×.
unfold Ext in |- *; simpl in |- ×.
intros d1xc1 d2xc2 fxg h.
unfold FunSET2_r_mor1, FunSET2_l_mor1 in |- ×.
unfold FOb at 1 in |- *; simpl in |- *; unfold FunSET2_r_ob in |- ×.
apply
Trans
with
(((FMor F (HOM_l fxg) o FMor F h)
o FMor F (FMor CoadjointUA (Hom_r fxg)))
o CoUA_mor (UA_of (Ob_r d2xc2))).
apply Comp_r.
apply
Trans
with (FMor F (HOM_l fxg o h) o FMor F (FMor CoadjointUA (Hom_r fxg))).
apply FComp.
apply Comp_r; apply FComp.
apply
Trans
with
((FMor F (HOM_l fxg) o FMor F h)
o FMor F (FMor CoadjointUA (Hom_r fxg))
o CoUA_mor (UA_of (Ob_r d2xc2))).
apply Ass1.
apply
Trans
with
(FMor F (HOM_l fxg)
o FMor F h
o FMor F (FMor CoadjointUA (Hom_r fxg))
o CoUA_mor (UA_of (Ob_r d2xc2))).
apply Ass1.
apply
Trans
with
(FMor F (HOM_l fxg)
o (FMor F h o CoUA_mor (UA_of (Ob_r d1xc1))) o Hom_r fxg).
apply Comp_l.
apply Trans with (FMor F h o CoUA_mor (UA_of (Ob_r d1xc1)) o Hom_r fxg).
apply Comp_l.
unfold FMor at 2 in |- *; simpl in |- *;
apply CoUA_diag.
apply Ass.
apply Ass.
Qed.

Canonical Structure PsiUA_1 := Build_NT PsiUA_1_tau_nt_law.

Section psi_ua_iso.

Variable dxc : POb (Dual D) C.

Lemma PsiUA_1_o_PsiUA : AreIsos (PsiUA dxc) (PsiUA_1 dxc).
Proof.
unfold AreIsos, RIso_law in |- *; simpl in |- *; split.
unfold Ext in |- *; simpl in |- ×.
unfold PsiUA_arrow, Id_fun, PsiUA_1_arrow in |- ×.
intro f.
unfold FunSET2_l_ob in |- *; simpl in |- *; unfold CoadjointUA_ob in |- ×.
apply CoUA_unic1; apply Refl.
unfold Ext in |- *; simpl in |- ×.
unfold PsiUA_arrow, Id_fun, PsiUA_1_arrow in |- ×.
intro f.
unfold FunSET2_r_ob in |- *; apply (CoUA_diag (UA_of (Ob_r dxc))).
Qed.

End psi_ua_iso.