Set Implicit Arguments.
Unset Strict Implicit.

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

Hypothesis UA_of : d : D, UA d G.

Definition AdjointUA_ob (d : D) := UA_ob (UA_of d).

Variable d d' : D.

Definition AdjointUA_mor (f : d --> d') :=
UA_diese (UA_of d) (f o UA_mor (UA_of d')).

Proof.
unfold Map_law, AdjointUA_mor in |- *; intros f g H.
apply
(Diese_map (UA_of d) (x:=f o UA_mor (UA_of d')) (y:=g o UA_mor (UA_of d'))).
apply Comp_r; assumption.
Qed.

Proof.
unfold Fid_law in |- *; simpl in |- ×.
intro d.
apply UA_unic1.
apply Trans with (UA_mor (UA_of d) o Id (G (UA_ob (UA_of d)))).
apply Comp_l; apply FId.
apply Trans with (UA_mor (UA_of d)).
apply Idr1.
apply Idl1.
Qed.

Proof.
unfold Fcomp_law in |- *; simpl in |- ×.
unfold AdjointUA_mor, AdjointUA_ob in |- *; intros d1 d2 d3 f g.
apply UA_unic1.
apply
Trans
with
(UA_mor (UA_of d1)
o FMor G (UA_diese (UA_of d1) (f o UA_mor (UA_of d2)))
o FMor G (UA_diese (UA_of d2) (g o UA_mor (UA_of d3)))).
apply Comp_l; apply FComp.
apply
Trans
with
((UA_mor (UA_of d1)
o FMor G (UA_diese (UA_of d1) (f o UA_mor (UA_of d2))))
o FMor G (UA_diese (UA_of d2) (g o UA_mor (UA_of d3)))).
apply Ass.
apply
Trans
with
((f o UA_mor (UA_of d2))
o FMor G (UA_diese (UA_of d2) (g o UA_mor (UA_of d3)))).
apply Comp_r; apply UA_diag.
apply
Trans
with
(f
o UA_mor (UA_of d2)
o FMor G (UA_diese (UA_of d2) (g o UA_mor (UA_of d3)))).
apply Ass1.
apply Trans with (f o g o UA_mor (UA_of d3)).
apply Comp_l; apply UA_diag.
apply Ass.
Qed.

Section phi_ua_tau_def.

Variable dxc : POb (Dual D) C.

Definition PhiUA_arrow (f : UA_ob (UA_of (OB_l dxc)) --> Ob_r dxc) :=
UA_mor (UA_of (OB_l dxc)) o FMor G f.

Lemma PhiUA_arrow_map_law : Map_law PhiUA_arrow.
Proof.
unfold Map_law, PhiUA_arrow in |- ×.
intros f g H.
apply Comp_l; apply FPres; assumption.
Qed.

Canonical Structure PhiUA_tau := Build_Map PhiUA_arrow_map_law.

End phi_ua_tau_def.

Lemma PhiUA_tau_nt_law :
NT_law (F:=FunSET2_r AdjointUA) (G:=FunSET2_l G) PhiUA_tau.
Proof.
unfold NT_law, PhiUA_tau, PhiUA_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_l_ob in |- ×.
apply
Trans
with
(UA_mor (UA_of (OB_l d2xc2))
o FMor G (FMor AdjointUA (HOM_l fxg) o h) o FMor G (Hom_r fxg)).
apply Comp_l; apply FComp.
apply
Trans
with
((UA_mor (UA_of (OB_l d2xc2))
o FMor G (FMor AdjointUA (HOM_l fxg) o h)) o
FMor G (Hom_r fxg)).
apply Ass.
apply Comp_r.
apply
Trans
with
(UA_mor (UA_of (OB_l d2xc2))
o FMor G (FMor AdjointUA (HOM_l fxg)) o FMor G h).
apply Comp_l; apply FComp.
apply
Trans
with
((UA_mor (UA_of (OB_l d2xc2)) o FMor G (FMor AdjointUA (HOM_l fxg)))
o FMor G h).
apply Ass.
apply Trans with ((HOM_l fxg o UA_mor (UA_of (OB_l d1xc1))) o FMor G h).
apply Comp_r; unfold FMor at 2 in |- *; simpl in |- *;
apply UA_diag.
apply Ass1.
Qed.

Canonical Structure PhiUA := Build_NT PhiUA_tau_nt_law.

Section phi_ua_1_tau_def.

Variable dxc : POb (Dual D) C.

Definition PhiUA_1_arrow (f : OB_l dxc --> G (Ob_r dxc)) :=
UA_diese (UA_of (OB_l dxc)) f.

Lemma PhiUA_1_arrow_map_law : Map_law PhiUA_1_arrow.
Proof.
unfold Map_law, PhiUA_1_arrow in |- ×.
intros f g H.
apply (Diese_map (UA_of (OB_l dxc)) (x:=f) (y:=g)).
assumption.
Qed.

Canonical Structure PhiUA_1_tau := Build_Map PhiUA_1_arrow_map_law.

End phi_ua_1_tau_def.

Lemma PhiUA_1_tau_nt_law :
NT_law (F:=FunSET2_l G) (G:=FunSET2_r AdjointUA) PhiUA_1_tau.
Proof.
unfold NT_law in |- *; simpl in |- ×.
unfold Ext in |- *; simpl in |- ×.
intros d1xc1 d2xc2 fxg h.
unfold PhiUA_1_arrow, FunSET2_r_mor1 in |- ×.
unfold FMor at 1 in |- *; simpl in |- ×.
unfold AdjointUA_mor, FunSET2_r_ob in |- *; simpl in |- *;
apply UA_unic1.
apply
Trans
with
(UA_mor (UA_of (OB_l d2xc2))
o FMor G
(UA_diese (UA_of (OB_l d2xc2))
(HOM_l fxg o UA_mor (UA_of (OB_l d1xc1)))
o UA_diese (UA_of (OB_l d1xc1)) h) o FMor G (Hom_r fxg)).
apply Comp_l; apply FComp.
apply
Trans
with
((UA_mor (UA_of (OB_l d2xc2))
o FMor G
(UA_diese (UA_of (OB_l d2xc2))
(HOM_l fxg o UA_mor (UA_of (OB_l d1xc1)))
o UA_diese (UA_of (OB_l d1xc1)) h)) o FMor G (Hom_r fxg)).
apply Ass.
apply
Trans
with
((UA_mor (UA_of (OB_l d2xc2))
o FMor G
(UA_diese (UA_of (OB_l d2xc2))
(HOM_l fxg o UA_mor (UA_of (OB_l d1xc1))))
o FMor G (UA_diese (UA_of (OB_l d1xc1)) h)) o
FMor G (Hom_r fxg)).
apply Comp_r; apply Comp_l; apply FComp.
apply
Trans
with
(((UA_mor (UA_of (OB_l d2xc2))
o FMor G
(UA_diese (UA_of (OB_l d2xc2))
(HOM_l fxg o UA_mor (UA_of (OB_l d1xc1)))))
o FMor G (UA_diese (UA_of (OB_l d1xc1)) h)) o
FMor G (Hom_r fxg)).
apply Comp_r; apply Ass.
apply
Trans
with
(((HOM_l fxg o UA_mor (UA_of (OB_l d1xc1)))
o FMor G (UA_diese (UA_of (OB_l d1xc1)) h)) o
FMor G (Hom_r fxg)).
apply Comp_r; apply Comp_r; apply UA_diag.
unfold FunSET2_l_mor1 in |- *; apply Comp_r.
apply
Trans
with
(HOM_l fxg
o UA_mor (UA_of (OB_l d1xc1)) o FMor G (UA_diese (UA_of (OB_l d1xc1)) h)).
apply Ass1.
apply Comp_l; apply UA_diag.
Qed.

Canonical Structure PhiUA_1 := Build_NT PhiUA_1_tau_nt_law.

Section phi_ua_iso.

Variable dxc : POb (Dual D) C.

Lemma PhiUA_1_o_PhiUA : AreIsos (PhiUA dxc) (PhiUA_1 dxc).
Proof.
unfold AreIsos in |- *; unfold RIso_law in |- *; simpl in |- *; split.
unfold Ext in |- *; simpl in |- ×.
unfold PhiUA_arrow, Id_fun, PhiUA_1_arrow in |- ×.
intro f.
unfold FunSET2_l_ob in |- *; apply UA_diag.
unfold Ext in |- *; simpl in |- ×.
unfold PhiUA_arrow, Id_fun, PhiUA_1_arrow in |- ×.
intro f.
unfold FunSET2_r_ob in |- *; simpl in |- *; unfold AdjointUA_ob in |- ×.
apply UA_unic1.
apply Refl.
Qed.

End phi_ua_iso.