Require Export Adj_UA.
Require Export Pres_Limits.

Set Implicit Arguments.
Unset Strict Implicit.


Section ladj_pres.

Variables (C D : Category) (G : Functor C D) (la : LeftAdj G)
  (J : Category) (H : Functor J C) (l : Limit H).


 Section lp_diese.

 Variables (d : D) (tau : Cone d (H o_F G)).

 Definition Lp_sigma_tau (i : J) := ApAphi_inv la (tau i:d --> G (H i)).


 Lemma Lp_sigma_tau_cone_law : Cone_law Lp_sigma_tau.
 Proof.
 unfold Cone_law, Lp_sigma_tau in |- ×.
 intros i j g.
apply Trans with (ApAphi_inv la (tau i o FMor G (FMor H g))).
 apply Aphi_invPres.
 apply (Eq_cone tau g).
 apply (Adj_eq5 la (FMor H g) (tau i)).
 Qed.

 Definition Lp_sigma := Build_Cone Lp_sigma_tau_cone_law.


 Definition Lp_diese : d --> G (Lim l) := ApAphi la (Lim_diese l Lp_sigma).

 End lp_diese.

Lemma Lp_coUAlaw1 : Limit_law1 (Limiting_cone l o_C G) Lp_diese.
Proof.
unfold Limit_law1, Limit_eq in |- *; simpl in |- *; intros d tau i.
unfold Comp_cone_tau, Lp_diese in |- ×.
apply
       Trans
        with (ApAphi la (Lim_diese l (Lp_sigma tau) o Limiting_cone l i)).
apply Sym.
apply (Adj_eq3 la (Limiting_cone l i) (Lim_diese l (Lp_sigma tau))).
apply Trans with (ApAphi la (ApAphi_inv (c:=H i) la (tau i))).
unfold Comp_FOb in |- *; apply AphiPres.
apply (Prf_limit1 l (Lp_sigma tau) i).
apply (Idl_inv (NTa_areIso la (Build_POb1 d (H i))) (tau i)).
Qed.

Lemma Lp_coUAlaw2 : Limit_law2 (Limiting_cone l o_C G) Lp_diese.
Proof.
unfold Limit_law2, Limit_eq in |- *; simpl in |- *; intros d tau t.
unfold Comp_cone_tau, Lp_diese in |- ×.
intro H'.
apply Trans with (ApAphi la (ApAphi_inv la t)).
apply Sym.
apply (Idl_inv (NTa_areIso la (Build_POb1 d (Lim l))) t).
apply AphiPres; apply (Prf_limit2 l).
unfold Limit_eq in |- *; intro i.
apply Trans with (ApAphi_inv la (t o FMor G (Limiting_cone l i))).
apply Sym.
apply (Adj_eq5 la (Limiting_cone l i) t).
simpl in |- *; unfold Lp_sigma_tau in |- *; apply Aphi_invPres; apply (H' i).
Qed.

Lemma Ladj_Pres1 : Preserves_1limit G l.
Proof.
apply (Build_IsLimit Lp_coUAlaw1 Lp_coUAlaw2).
Defined.

End ladj_pres.


Lemma Ladj_continuous :
 ∀ (C D : Category) (G : Functor C D), LeftAdj G → Continuous G.
Proof.
unfold Continuous, Preserves_limits in |- *; intros C D G la J H l.
apply (Ladj_Pres1 la l).
Defined.