# Library UniMath.CategoryTheory.limits.graphs.limits

*************************************************
Contents:
• Definition of limits
• Proof that limits form a property in a (saturated/univalent) category (isaprop_Lims)
• Pointwise construction of limits in functor precategories LimsFunctorCategory
• Alternative definition of limits via colimits
Written by: Benedikt Ahrens and Anders Mörtberg, 2015-2016

# Definition of limits

Section lim_def.

Context {C : precategory} (hsC : has_homsets C).

Definition cone {g : graph} (d : diagram g C) (c : C) : UU :=
(f : (v : vertex g), Cc,dob d v),
(u v : vertex g) (e : edge u v), f u · dmor d e = f v.

Definition make_cone {g : graph} {d : diagram g C} {c : C}
(f : v, Cc, dob d v) (Hf : u v (e : edge u v), f u · dmor d e = f v) :
cone d c
:= tpair _ f Hf.

The injections to c in the cocone
Definition coneOut {g : graph} {d : diagram g C} {c : C} (cc : cone d c) :
v, Cc, dob d v := pr1 cc.

Lemma coneOutCommutes {g : graph} {d : diagram g C} {c : C} (cc : cone d c) :
u v (e : edge u v), coneOut cc u · dmor d e = coneOut cc v.
Proof.
apply (pr2 cc).
Qed.

Definition isLimCone {g : graph} (d : diagram g C) (c0 : C)
(cc0 : cone d c0) : UU := (c : C) (cc : cone d c),
iscontr ( x : Cc,c0, v, x · coneOut cc0 v = coneOut cc v).

Definition LimCone {g : graph} (d : diagram g C) : UU :=
(A : ( l, cone d l)), isLimCone d (pr1 A) (pr2 A).

Definition make_LimCone {g : graph} (d : diagram g C)
(c : C) (cc : cone d c) (isCC : isLimCone d c cc) : LimCone d
:= tpair _ (tpair _ c cc) isCC.

lim is the tip of the LimCone
Definition lim {g : graph} {d : diagram g C} (CC : LimCone d) : C
:= pr1 (pr1 CC).

Definition limCone {g : graph} {d : diagram g C} (CC : LimCone d) :
cone d (lim CC) := pr2 (pr1 CC).

Definition limOut {g : graph} {d : diagram g C} (CC : LimCone d) :
(v : vertex g), Clim CC, dob d v := coneOut (limCone CC).

Lemma limOutCommutes {g : graph} {d : diagram g C}
(CC : LimCone d) : (u v : vertex g) (e : edge u v),
limOut CC u · dmor d e = limOut CC v.
Proof.
exact (coneOutCommutes (limCone CC)).
Qed.

Lemma limUnivProp {g : graph} {d : diagram g C}
(CC : LimCone d) : (c : C) (cc : cone d c),
iscontr ( x : Cc, lim CC, (v : vertex g), x · limOut CC v = coneOut cc v).
Proof.
apply (pr2 CC).
Qed.

Lemma isaprop_isLimCone {g : graph} {d : diagram g C} (c0 : C)
(cc0 : cone d c0) : isaprop (isLimCone d c0 cc0).
Proof.
repeat (apply impred; intro).
apply isapropiscontr.
Qed.

Definition isLimCone_LimCone {g : graph} {d : diagram g C}
(CC : LimCone d)
: isLimCone d (lim CC) (tpair _ (limOut CC) (limOutCommutes CC))
:= pr2 CC.

Definition limArrow {g : graph} {d : diagram g C} (CC : LimCone d)
(c : C) (cc : cone d c) : Cc, lim CC :=
pr1 (pr1 (isLimCone_LimCone CC c cc)).

Lemma limArrowCommutes {g : graph} {d : diagram g C} (CC : LimCone d)
(c : C) (cc : cone d c) (u : vertex g) :
limArrow CC c cc · limOut CC u = coneOut cc u.
Proof.
exact ((pr2 (pr1 (isLimCone_LimCone CC _ cc))) u).
Qed.

Lemma limArrowUnique {g : graph} {d : diagram g C} (CC : LimCone d)
(c : C) (cc : cone d c) (k : Cc, lim CC)
(Hk : (u : vertex g), k · limOut CC u = coneOut cc u) :
k = limArrow CC c cc.
Proof.
now apply path_to_ctr, Hk.
Qed.

Lemma Cone_precompose {g : graph} {d : diagram g C}
{c : C} (cc : cone d c) (x : C) (f : Cx,c) :
u v (e : edge u v), (f · coneOut cc u) · dmor d e = f · coneOut cc v.
Proof.
now intros u v e; rewrite <- assoc, coneOutCommutes.
Qed.

Lemma limArrowEta {g : graph} {d : diagram g C} (CC : LimCone d)
(c : C) (f : Cc, lim CC) :
f = limArrow CC c (tpair _ (λ u, f · limOut CC u)
(Cone_precompose (limCone CC) c f)).
Proof.
now apply limArrowUnique.
Qed.

Definition limOfArrows {g : graph} {d1 d2 : diagram g C}
(CC1 : LimCone d1) (CC2 : LimCone d2)
(f : (u : vertex g), Cdob d1 u,dob d2 u)
(fNat : u v (e : edge u v), f u · dmor d2 e = dmor d1 e · f v) :
Clim CC1 , lim CC2.
Proof.
apply limArrow; use make_cone.
- now intro u; apply (limOut CC1 u · f u).
- abstract (intros u v e; simpl;
now rewrite <- assoc, fNat, assoc, limOutCommutes).
Defined.

Lemma limOfArrowsOut {g : graph} (d1 d2 : diagram g C)
(CC1 : LimCone d1) (CC2 : LimCone d2)
(f : (u : vertex g), Cdob d1 u,dob d2 u)
(fNat : u v (e : edge u v), f u · dmor d2 e = dmor d1 e · f v) :
u, limOfArrows CC1 CC2 f fNat · limOut CC2 u =
limOut CC1 u · f u.
Proof.
now unfold limOfArrows; intro u; rewrite limArrowCommutes.
Qed.

Lemma postCompWithLimOfArrows_subproof {g : graph} {d1 d2 : diagram g C}
(CC1 : LimCone d1) (CC2 : LimCone d2)
(f : (u : vertex g), Cdob d1 u,dob d2 u)
(fNat : u v (e : edge u v), f u · dmor d2 e = dmor d1 e · f v)
(x : C) (cc : cone d1 x) u v (e : edge u v) :
(coneOut cc u · f u) · dmor d2 e = coneOut cc v · f v.
Proof.
now rewrite <- (coneOutCommutes cc u v e), <- assoc, fNat, assoc.
Defined.

Lemma postCompWithLimOfArrows {g : graph} (d1 d2 : diagram g C)
(CC1 : LimCone d1) (CC2 : LimCone d2)
(f : (u : vertex g), Cdob d1 u,dob d2 u)
(fNat : u v (e : edge u v), f u · dmor d2 e = dmor d1 e · f v)
(x : C) (cc : cone d1 x) :
limArrow CC1 x cc · limOfArrows CC1 CC2 f fNat =
limArrow CC2 x (make_cone (λ u, coneOut cc u · f u)
(postCompWithLimOfArrows_subproof CC1 CC2 f fNat x cc)).
Proof.
apply limArrowUnique; intro u.
now rewrite <- assoc, limOfArrowsOut, assoc, limArrowCommutes.
Qed.

Lemma postCompWithLimArrow {g : graph} (D : diagram g C)
(CC : LimCone D) (c : C) (cc : cone D c) (d : C) (k : Cd,c) :
k · limArrow CC c cc =
limArrow CC d (make_cone (λ u, k · coneOut cc u)
(Cone_precompose cc d k)).
Proof.
apply limArrowUnique.
now intro u; rewrite <- assoc, limArrowCommutes.
Qed.

Lemma lim_endo_is_identity {g : graph} (D : diagram g C)
(CC : LimCone D) (k : lim CC --> lim CC)
(H : u, k · limOut CC u = limOut CC u) :
identity _ = k.
Proof.
use (uniqueExists (limUnivProp CC _ _)).
- now apply (limCone CC).
- intros v; simpl.
unfold compose. simpl.
now apply id_left.
- simpl; now apply H.
Qed.

Lemma isLim_is_iso {g : graph} (D : diagram g C) (CC : LimCone D) (d : C) (cd : cone D d) :
isLimCone D d cd is_iso (limArrow CC d cd).
Proof.
intro H.
apply is_iso_from_is_z_iso.
set (CD := make_LimCone D d cd H).
apply (tpair _ (limArrow (make_LimCone D d cd H) (lim CC) (limCone CC))).
split.
apply pathsinv0.
change d with (lim CD).
apply lim_endo_is_identity. simpl; intro u;
rewrite <- assoc.
eapply pathscomp0; [eapply maponpaths; apply limArrowCommutes|].
apply (limArrowCommutes CC).
apply pathsinv0, (lim_endo_is_identity _ CC); simpl; intro u;
rewrite <- assoc.
eapply pathscomp0; [eapply maponpaths; apply (limArrowCommutes CC)|].
apply (limArrowCommutes CD).
Defined.

Lemma inv_isLim_is_iso {g : graph} (D : diagram g C) (CC : LimCone D) (d : C)
(cd : cone D d) (H : isLimCone D d cd) :
inv_from_iso (make_iso _ (isLim_is_iso D CC d cd H)) =
limArrow (make_LimCone D d cd H) _ (limCone CC).
Proof.
cbn. unfold precomp_with.
apply id_right.
Qed.

Lemma is_iso_isLim {g : graph} (D : diagram g C) (CC : LimCone D) (d : C) (cd : cone D d) :
is_iso (limArrow CC d cd) isLimCone D d cd.
Proof.
intro H.
set (iinv := z_iso_inv_from_is_z_iso _ (is_z_iso_from_is_iso _ H)).
intros x cx.
use tpair.
- use tpair.
+ exact (limArrow CC x cx·iinv).
+ simpl; intro u.
assert (XR:=limArrowCommutes CC x cx u).
eapply pathscomp0; [| apply XR].
eapply pathscomp0; [ apply (!assoc _ _ _ ) |].
apply maponpaths.
apply z_iso_inv_on_right.
apply pathsinv0, limArrowCommutes.
- intros p; destruct p as [f Hf].
apply subtypePath.
+ intro a; apply impred; intro u; apply hsC.
+ simpl; apply z_iso_inv_on_left; simpl.
apply pathsinv0, limArrowUnique; intro u.
cbn in ×.
eapply pathscomp0; [| apply Hf].
eapply pathscomp0. apply (!assoc _ _ _ ).
apply maponpaths.
apply limArrowCommutes.
Defined.

Definition iso_from_lim_to_lim {g : graph} {d : diagram g C}
(CC CC' : LimCone d) : iso (lim CC) (lim CC').
Proof.
use make_iso.
- apply limArrow, limCone.
- use is_iso_qinv.
+ apply limArrow, limCone.
+ abstract (now split; apply pathsinv0, lim_endo_is_identity; intro u;
rewrite <- assoc, limArrowCommutes; eapply pathscomp0; try apply limArrowCommutes).
Defined.

End lim_def.

Section Lims.

Definition Lims (C : precategory) : UU := (g : graph) (d : diagram g C), LimCone d.
Definition hasLims (C : precategory) : UU :=
(g : graph) (d : diagram g C), ishinh (LimCone d).

Limits of a specific shape
Definition Lims_of_shape (g : graph) (C : precategory) : UU :=
(d : diagram g C), LimCone d.

Section Universal_Unique.

Variable (C : univalent_category).

Let H : is_univalent C := pr2 C.

Lemma isaprop_Lims : isaprop (Lims C).
Proof.
apply impred; intro g; apply impred; intro cc.
apply invproofirrelevance; intros Hccx Hccy.
apply subtypePath.
- intro; apply isaprop_isLimCone.
- apply (total2_paths_f (isotoid _ H (iso_from_lim_to_lim Hccx Hccy))).
set (B c := v, Cc,dob cc v).
set (C' (c : C) f := u v (e : edge u v), @compose _ c _ _ (f u) (dmor cc e) = f v).
rewrite (@transportf_total2 _ B C').
apply subtypePath.
+ intro; repeat (apply impred; intro); apply univalent_category_has_homsets.
+ abstract (now simpl; eapply pathscomp0; [apply transportf_isotoid_dep'|];
apply funextsec; intro v; rewrite inv_isotoid, idtoiso_isotoid;
cbn; unfold precomp_with; rewrite id_right; apply limArrowCommutes).
Qed.

End Universal_Unique.
End Lims.

# Limits in functor categories

Section LimFunctor.

Context {A C : precategory} (hsC : has_homsets C) {g : graph} (D : diagram g [A, C, hsC]).

Variable (HCg : (a : A), LimCone (diagram_pointwise hsC D a)).

Definition LimFunctor_ob (a : A) : C := lim (HCg a).

Definition LimFunctor_mor (a a' : A) (f : Aa, a') :
CLimFunctor_ob a,LimFunctor_ob a'.
Proof.
use limOfArrows.
- now intro u; apply (# (pr1 (dob D u)) f).
- abstract (now intros u v e; simpl; apply (nat_trans_ax (# D e))).
Defined.

Definition LimFunctor_data : functor_data A C := tpair _ _ LimFunctor_mor.

Lemma is_functor_LimFunctor_data : is_functor LimFunctor_data.
Proof.
split.
- intro a; simpl.
apply pathsinv0, lim_endo_is_identity; intro u.
unfold LimFunctor_mor; rewrite limOfArrowsOut.
assert (H : # (pr1 (dob D u)) (identity a) = identity (pr1 (dob D u) a)).
apply (functor_id (dob D u) a).
now rewrite H, id_right.
- intros a b c fab fbc; simpl; unfold LimFunctor_mor.
apply pathsinv0.
eapply pathscomp0; [now apply postCompWithLimOfArrows|].
apply pathsinv0, limArrowUnique; intro u.
rewrite limOfArrowsOut, (functor_comp (dob D u)); simpl.
now rewrite <- assoc.
Qed.

Definition LimFunctor : functor A C := tpair _ _ is_functor_LimFunctor_data.

Definition lim_nat_trans_in_data v : [A, C, hsC] LimFunctor, dob D v .
Proof.
use tpair.
- intro a; exact (limOut (HCg a) v).
- abstract (intros a a' f; apply (limOfArrowsOut _ _ (HCg a) (HCg a'))).
Defined.

Definition cone_pointwise (F : [A,C,hsC]) (cc : cone D F) a :
cone (diagram_pointwise _ D a) (pr1 F a).
Proof.
use make_cone.
- now intro v; apply (pr1 (coneOut cc v) a).
- abstract (intros u v e;
now apply (nat_trans_eq_pointwise (coneOutCommutes cc u v e))).
Defined.

Lemma LimFunctor_unique (F : [A, C, hsC]) (cc : cone D F) :
iscontr ( x : [A, C, hsC] F, LimFunctor ,
v, x · lim_nat_trans_in_data v = coneOut cc v).
Proof.
use tpair.
- use tpair.
+ apply (tpair _ (λ a, limArrow (HCg a) _ (cone_pointwise F cc a))).
abstract (intros a a' f; simpl; apply pathsinv0; eapply pathscomp0;
[ apply (postCompWithLimOfArrows _ _ (HCg a))
| apply pathsinv0; eapply pathscomp0;
[ apply postCompWithLimArrow
| apply limArrowUnique; intro u; eapply pathscomp0;
[ now apply limArrowCommutes | now use nat_trans_ax]]]).
+ abstract (intro u; apply (nat_trans_eq hsC); simpl; intro a;
now apply (limArrowCommutes (HCg a))).
- abstract (intro t; destruct t as [t1 t2];
apply subtypePath; simpl;
[ intro; apply impred; intro u; apply functor_category_has_homsets
| apply (nat_trans_eq hsC); simpl; intro a;
apply limArrowUnique; intro u;
now apply (nat_trans_eq_pointwise (t2 u))]).
Defined.

Lemma LimFunctorCone : LimCone D.
Proof.
use make_LimCone.
- exact LimFunctor.
- use make_cone.
+ now apply lim_nat_trans_in_data.
+ abstract (now intros u v e; apply (nat_trans_eq hsC);
intro a; apply (limOutCommutes (HCg a))).
- now intros F cc; simpl; apply (LimFunctor_unique _ cc).
Defined.

Definition isLimFunctor_is_pointwise_Lim
(X : [A,C,hsC]) (R : cone D X) (H : isLimCone D X R)
: a, isLimCone (diagram_pointwise hsC D a) _ (cone_pointwise X R a).
Proof.
intro a.
apply (is_iso_isLim hsC _ (HCg a)).
set (XR := isLim_is_iso D LimFunctorCone X R H).
apply (is_functor_iso_pointwise_if_iso _ _ _ _ _ _ XR).
Defined.

End LimFunctor.

Lemma LimsFunctorCategory (A C : precategory) (hsC : has_homsets C)
(HC : Lims C) : Lims [A,C,hsC].
Proof.
now intros g d; apply LimFunctorCone.
Defined.

Lemma LimsFunctorCategory_of_shape (g : graph) (A C : precategory) (hsC : has_homsets C)
(HC : Lims_of_shape g C) : Lims_of_shape g [A,C,hsC].
Proof.
now intros d; apply LimFunctorCone.
Defined.

Section map.

Context {C D : precategory} (F : functor C D).

Definition mapcone {g : graph} (d : diagram g C) {x : C}
(dx : cone d x) : cone (mapdiagram F d) (F x).
Proof.
use make_cone.
- simpl; intro n.
exact (#F (coneOut dx n)).
- abstract (intros u v e; simpl; rewrite <- functor_comp;
apply maponpaths, (coneOutCommutes dx _ _ e)).
Defined.

Definition preserves_limit {g : graph} (d : diagram g C) (L : C)
(cc : cone d L) : UU :=
isLimCone d L cc isLimCone (mapdiagram F d) (F L) (mapcone d cc).

Lemma right_adjoint_preserves_limit (HF : is_right_adjoint F) (hsC : has_homsets C) (hsD : has_homsets D)
{g : graph} (d : diagram g C) (L : C) (ccL : cone d L) : preserves_limit d L ccL.
Proof.
intros HccL M ccM.
set (H := pr2 HF : are_adjoints G F).
apply (@iscontrweqb _ ( y : C G M, L ,
i, y · coneOut ccL i = φ_adj_inv H (coneOut ccM i))).
- eapply (weqcomp (Y := y : C G M, L ,
i, φ_adj H y · # F (coneOut ccL i) = coneOut ccM i)).
+ apply invweq, (weqbandf (adjunction_hom_weq H M L)); simpl; intro f.
abstract (now apply weqiff; try (apply impred; intro; apply hsD)).
+ eapply (weqcomp (Y := y : C G M, L ,
i, φ_adj H (y · coneOut ccL i) = coneOut ccM i)).
× apply weqfibtototal; simpl; intro f.
abstract (apply weqiff; try (apply impred; intro; apply hsD); split; intros HH i;
[ now rewrite φ_adj_natural_postcomp; apply HH
| now rewrite <- φ_adj_natural_postcomp; apply HH ]).
× apply weqfibtototal; simpl; intro f.
abstract (apply weqiff; [ | apply impred; intro; apply hsD | apply impred; intro; apply hsC ];
split; intros HH i;
- transparent assert (X : (cone d (G M))).
{ use make_cone.
+ intro v; apply (φ_adj_inv H (coneOut ccM v)).
+ intros m n e; simpl.
rewrite <- (coneOutCommutes ccM m n e); simpl.
}
apply (HccL (G M) X).
Defined.

End map.

Section Reflects.
Context {C D : precategory} (F : functor C D).

Definition reflects_limits_of_shape (g : graph) : UU :=
(d : diagram g C) (L : ob C) cc,
isLimCone (mapdiagram F d) (F L) (mapcone F d cc)
isLimCone d L cc.

Definition reflects_all_limits : UU :=
(g : graph), reflects_limits_of_shape g.

Fully faithful functors reflect limits of any given shape.
Lemma fully_faithful_reflects_all_limits (fff : fully_faithful F) :
reflects_all_limits.
Proof.
intros g d L cc isLimConeImL.
unfold isLimCone in ×.
intros L' cc'.
unfold fully_faithful in fff.
apply (@iscontrweqf
( x : D F L', F L ,
v : vertex g,
x · coneOut (mapcone F d cc) v = coneOut (mapcone F d cc') v)).
- apply (@weqcomp _ ( x : C L', L , v : vertex g, # F x · coneOut (mapcone F d cc) v = coneOut (mapcone F d cc') v)).
+ apply invweq.
apply (weqfp (weq_from_fully_faithful fff _ _)
(λ f, v, f · coneOut (mapcone F d cc) v = coneOut (mapcone F d cc') v)).
+ apply weqfibtototal; intro f.
apply weqonsecfibers; intro v.
unfold mapcone; cbn.
apply invweq.
apply fully_faithful_commutative_triangle_weq.
assumption.
- apply isLimConeImL.
Qed.
End Reflects.

# Definition of limits via colimits

Put in a module for namespace reasons

Require UniMath.CategoryTheory.opp_precat.

Module co.

Import UniMath.CategoryTheory.opp_precat.

Section lim_def.

Context {C : precategory} (hsC : has_homsets C).

Definition opp_diagram g C := diagram g C^op.

Definition cone {g : graph} (d : diagram g C^op) (c : C) : UU :=
@cocone C^op g d c.

Definition make_cone {g : graph} {d : diagram g C^op} {c : C}
(f : v, Cc, dob d v) (Hf : u v (e : edge u v) , f v · dmor d e = f u) :
cone d c
:= tpair _ f Hf.

Definition coneOut {g : graph} {d : diagram g C^op} {c : C} (cc : cone d c) :
v, Cc, dob d v := coconeIn cc.

Lemma coneOutCommutes {g : graph} {d : diagram g C^op} {c : C} (cc : cone d c) :
u v (e : edge u v), coneOut cc v · dmor d e = coneOut cc u.
Proof.
apply (coconeInCommutes cc).
Qed.

Definition isLimCone {g : graph} (d : diagram g C^op) (c0 : C)
(cc0 : cone d c0) : UU :=
isColimCocone _ _ cc0.

Definition LimCone {g : graph} (d : diagram g C^op) : UU :=
ColimCocone d.

Definition make_LimCone {g : graph} (d : diagram g C^op)
(c : C) (cc : cone d c) (isCC : isLimCone d c cc) : LimCone d.
Proof.
use make_ColimCocone.
- apply c.
- apply cc.
- apply isCC.
Defined.

Definition Lims : UU := (g : graph) (d : diagram g C^op), LimCone d.
Definition hasLims : UU :=
(g : graph) (d : diagram g C^op), ishinh (LimCone d).

Definition lim {g : graph} {d : diagram g C^op} (CC : LimCone d) : C
:= colim CC.

Definition limCone {g : graph} {d : diagram g C^op} (CC : LimCone d) :
cone d (lim CC) := colimCocone CC.

Definition limOut {g : graph} {d : diagram g C^op} (CC : LimCone d) :
(v : vertex g), Clim CC, dob d v := coneOut (limCone CC).

Lemma limOutCommutes {g : graph} {d : diagram g C^op}
(CC : LimCone d) : (u v : vertex g) (e : edge u v),
limOut CC v · dmor d e = limOut CC u.
Proof.
exact (coneOutCommutes (limCone CC)).
Qed.

Lemma limUnivProp {g : graph} {d : diagram g C^op}
(CC : LimCone d) : (c : C) (cc : cone d c),
iscontr ( x : Cc, lim CC, (v : vertex g), x · limOut CC v = coneOut cc v).
Proof.
apply (colimUnivProp CC).
Qed.

Definition isLimCone_LimCone {g : graph} {d : diagram g C^op}
(CC : LimCone d)
: isLimCone d (lim CC) (tpair _ (limOut CC) (limOutCommutes CC))
:= isColimCocone_ColimCocone CC.

Definition limArrow {g : graph} {d : diagram g C^op} (CC : LimCone d)
(c : C) (cc : cone d c) : Cc, lim CC.
Proof.
exact (colimArrow CC _ cc).
Defined.

Lemma limArrowCommutes {g : graph} {d : diagram g C^op} (CC : LimCone d)
(c : C) (cc : cone d c) (u : vertex g) :
limArrow CC c cc · limOut CC u = coneOut cc u.
Proof.
exact (colimArrowCommutes CC _ cc _ ).
Qed.

Lemma limArrowUnique {g : graph} {d : diagram g C^op} (CC : LimCone d)
(c : C) (cc : cone d c) (k : Cc, lim CC)
(Hk : (u : vertex g), k · limOut CC u = coneOut cc u) :
k = limArrow CC c cc.
Proof.
apply (colimArrowUnique CC c cc k Hk).
Qed.

Lemma Cone_precompose {g : graph} {d : diagram g C^op}
{c : C} (cc : cone d c) (x : C) (f : Cx,c) :
u v (e : edge u v), (f · coneOut cc v) · dmor d e = f · coneOut cc u.
Proof.
apply (Cocone_postcompose cc x f).
Qed.

Lemma limArrowEta {g : graph} {d : diagram g C^op} (CC : LimCone d)
(c : C) (f : Cc, lim CC) :
f = limArrow CC c (tpair _ (λ u, f · limOut CC u)
(Cone_precompose (limCone CC) c f)).
Proof.
now apply limArrowUnique.
Qed.

Definition limOfArrows {g : graph} {d1 d2 : diagram g C^op}
(CC1 : LimCone d1) (CC2 : LimCone d2)
(f : (u : vertex g), Cdob d1 u,dob d2 u)
(fNat : u v (e : edge u v), f v · (dmor d2 e : Cdob d2 v, dob d2 u)
=
(dmor d1 e : Cdob d1 v, dob d1 u f u) :
Clim CC1 , lim CC2.
Proof.
use (colimOfArrows CC2 CC1).
- apply f.
- apply fNat.
Defined.

Lemma limOfArrowsOut {g : graph} (d1 d2 : diagram g C^op)
(CC1 : LimCone d1) (CC2 : LimCone d2)
(f : (u : vertex g), Cdob d1 u,dob d2 u)
(fNat : u v (e : edge u v), f v · dmor d2 e = (dmor d1 e : C _ , _ ) · f u) :
u, limOfArrows CC1 CC2 f fNat · limOut CC2 u =
limOut CC1 u · f u.
Proof.
apply (colimOfArrowsIn _ _ CC2 CC1 f fNat).
Qed.

Lemma postCompWithLimOfArrows_subproof {g : graph} {d1 d2 : diagram g C^op}
(CC1 : LimCone d1) (CC2 : LimCone d2)
(f : (u : vertex g), Cdob d1 u,dob d2 u)
(fNat : u v (e : edge u v), f v · dmor d2 e = (dmor d1 e : C _ , _ ) · f u)
(x : C) (cc : cone d1 x) u v (e : edge u v) :
(coneOut cc v · f v) · dmor d2 e = coneOut cc u · f u.
Proof.
apply (preCompWithColimOfArrows_subproof CC2 CC1 f fNat x cc _ _ e).
Defined.

Lemma postcompWithColimOfArrows {g : graph} (d1 d2 : diagram g C^op)
(CC1 : LimCone d1) (CC2 : LimCone d2)
(f : (u : vertex g), Cdob d1 u,dob d2 u)
(fNat : u v (e : edge u v), f v · dmor d2 e = (dmor d1 e : C _ , _ ) · f u)
(x : C) (cc : cone d1 x) :
limArrow CC1 x cc · limOfArrows CC1 CC2 f fNat =
limArrow CC2 x (make_cone (λ u, coneOut cc u · f u)
(postCompWithLimOfArrows_subproof CC1 CC2 f fNat x cc)).
Proof.
apply limArrowUnique.
intro.
rewrite <- assoc.
rewrite limOfArrowsOut.
rewrite assoc.
rewrite limArrowCommutes.
apply idpath.
Qed.

Lemma precompWithLimArrow {g : graph} (D : diagram g C^op)
(CC : LimCone D) (c : C) (cc : cone D c) (d : C) (k : Cd,c) :
k · limArrow CC c cc =
limArrow CC d (make_cone (λ u, k · coneOut cc u)
(Cone_precompose cc d k)).
Proof.
apply limArrowUnique.
now intro u; rewrite <- assoc, limArrowCommutes.
Qed.

Lemma lim_endo_is_identity {g : graph} (D : diagram g C^op)
(CC : LimCone D) (k : lim CC --> lim CC)
(H : u, k · limOut CC u = limOut CC u) :
identity _ = k.
Proof.
use (uniqueExists (limUnivProp CC _ _)).
- now apply (limCone CC).
- intros v; simpl.
unfold compose. simpl.
now apply id_left.
- simpl; now apply H.
Qed.

Lemma isLim_is_iso {g : graph} (D : diagram g C^op) (CC : LimCone D) (d : C) (cd : cone D d) :
isLimCone D d cd is_iso (limArrow CC d cd).
Proof.
intro H.
apply is_iso_from_is_z_iso.
set (CD := make_LimCone D d cd H).
apply (tpair _ (limArrow (make_LimCone D d cd H) (lim CC) (limCone CC))).
split.
apply pathsinv0.
change d with (lim CD).
apply lim_endo_is_identity. simpl; intro u;
rewrite <- assoc.
eapply pathscomp0; [eapply maponpaths; apply limArrowCommutes|].
apply (limArrowCommutes CC).
apply pathsinv0, (lim_endo_is_identity _ CC); simpl; intro u;
rewrite <- assoc.
eapply pathscomp0; [eapply maponpaths; apply (limArrowCommutes CC)|].
apply (limArrowCommutes CD).
Defined.

Lemma inv_isLim_is_iso {g : graph} (D : diagram g C^op) (CC : LimCone D) (d : C)
(cd : cone D d) (H : isLimCone D d cd) :
inv_from_iso (make_iso _ (isLim_is_iso D CC d cd H)) =
limArrow (make_LimCone D d cd H) _ (limCone CC).
Proof.
cbn. unfold precomp_with.
apply id_right.
Qed.

Lemma is_iso_isLim {g : graph} (D : diagram g C^op) (CC : LimCone D) (d : C) (cd : cone D d) :
is_iso (limArrow CC d cd) isLimCone D d cd.
Proof.
intro H.
set (iinv := z_iso_inv_from_is_z_iso _ (is_z_iso_from_is_iso _ H)).
intros x cx.
use tpair.
- use tpair.
+ exact (limArrow CC x cx·iinv).
+ simpl; intro u.
assert (XR:=limArrowCommutes CC x cx u).
eapply pathscomp0; [| apply XR].
eapply pathscomp0; [ apply (!assoc _ _ _ ) |].
apply maponpaths.
apply z_iso_inv_on_right.
apply pathsinv0, limArrowCommutes.
- intros p; destruct p as [f Hf].
apply subtypePath.
+ intro a; apply impred; intro u; apply hsC.
+ simpl; apply z_iso_inv_on_left; simpl.
apply pathsinv0, limArrowUnique; intro u.
cbn in ×.
eapply pathscomp0; [| apply Hf].
eapply pathscomp0. apply (!assoc _ _ _ ).
apply maponpaths.
apply limArrowCommutes.
Defined.

End lim_def.

Arguments Lims : clear implicits.

Section LimFunctor.

Definition get_diagram (A C : precategory) (hsC : has_homsets C)
(g : graph) (D : diagram g [A, C, hsC]^op) :
diagram g [A^op, C^op, has_homsets_opp hsC].
Proof.
apply (tpair _ (λ u, from_opp_to_opp_opp _ _ _ (pr1 D u))).
intros u v e; simpl.
use tpair; simpl.
+ apply (pr2 D _ _ e).
+ abstract (intros a b f; apply pathsinv0, (pr2 (pr2 D u v e) b a f)).
Defined.

Definition get_cocone (A C : precategory) (hsC : has_homsets C)
(g : graph) (D : diagram g [A, C, hsC]^op) (F : functor A C) (ccF : cocone D F) :
cocone (get_diagram A C hsC g D) (functor_opp F).
Proof.
destruct ccF as [t p]. use make_cocone.
- intro u; apply (tpair _ (pr1 (t u))).
abstract (intros a b f; apply pathsinv0, (pr2 (t u) b a f)).
- abstract (intros u v e; apply (nat_trans_eq (has_homsets_opp hsC));
now intro a; simpl; rewrite <- (p u v e)).
Defined.

Lemma LimFunctorCone (A C : precategory) (hsC : has_homsets C)
(g : graph)
(D : diagram g [A, C, hsC]^op)
(HC : a : A^op,
LimCone
(diagram_pointwise (has_homsets_opp hsC) (get_diagram A C hsC g D) a))
: LimCone D.
Proof.
set (HColim := ColimFunctorCocone (has_homsets_opp hsC) (get_diagram _ _ _ _ D) HC).
destruct HColim as [pr1x pr2x].
destruct pr1x as [pr1pr1x pr2pr1x].
destruct pr2pr1x as [pr1pr2pr1x pr2pr2pr1x].
simpl in ×.
use (make_ColimCocone _ (from_opp_opp_to_opp _ _ _ pr1pr1x)).
- use make_cocone.
+ simpl; intros.
use tpair.
× intro a; apply (pr1pr2pr1x v a).
× abstract (intros a b f; apply pathsinv0, (nat_trans_ax (pr1pr2pr1x v) )).
+ abstract (intros u v e; apply (nat_trans_eq hsC); simpl; intro a;
now rewrite <- (pr2pr2pr1x u v e)).
- intros F ccF.
set (H := pr2x (from_opp_to_opp_opp _ _ _ F) (get_cocone _ _ _ _ _ _ ccF)).
destruct H as [H1 H2].
destruct H1 as [α ].
simpl in ×.
use tpair.
+ use tpair.
× α.
abstract (intros a b f; simpl; now apply pathsinv0, (nat_trans_ax α b a f)).
× abstract (intro u; apply (nat_trans_eq hsC); intro a;
destruct ccF as [t p]; apply (toforallpaths _ _ _ (maponpaths pr1 ( u)) a)).
+ intro H; destruct H as [f Hf]; apply subtypePath.
× abstract (intro β; repeat (apply impred; intro);
now apply (has_homsets_opp (functor_category_has_homsets A C hsC))).
× match goal with |[ H2 : _ : ?TT , _ = _ ,,_ |- _ ] ⇒
transparent assert (T : TT) end.
{ use (tpair _ (tpair _ (pr1 f) _)); simpl.
- abstract (intros x y fxy; apply pathsinv0, (pr2 f y x fxy)).
- abstract (intro u; apply (nat_trans_eq (has_homsets_opp hsC)); intro x;
destruct ccF as [t p]; apply (toforallpaths _ _ _ (maponpaths pr1 (Hf u)) x)).
}
set (T' := maponpaths pr1 (H2 T)); simpl in T'.
apply (nat_trans_eq hsC); intro a; simpl.
now rewrite <- T'.
Defined.

End LimFunctor.

End co.