Library UniMath.CategoryTheory.DisplayedCats.Limits
Limits
Require Import UniMath.Foundations.Sets.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.limits.graphs.colimits.
Require Import UniMath.CategoryTheory.limits.graphs.limits.
Local Open Scope cat.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Total.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
Local Open Scope type_scope.
Local Open Scope mor_disp_scope.
Section Creates_Limits.
Definition creates_limit
{C : category}
(D : disp_cat C)
{J : graph} (F : diagram J (total_category D))
{x : C} (L : cone (mapdiagram (pr1_category D) F) x)
(isL : isLimCone _ x L) : UU
:=
∑ (CC : iscontr
( ∑ (d : D x)
(δ : ∏ j : vertex J, d -->[coneOut L j] (pr2 (dob F j))),
forms_cone(c:=(x,,d)) F (λ j, (coneOut L j ,, δ j))))
, isLimCone _ _ (make_cone _ (pr2 (pr2 (iscontrpr1 CC)))).
Definition creates_limits {C : category} (D : disp_cat C) : UU
:=
∏ (J : graph) (F : diagram J (total_category D))
(x : C) (L : cone (mapdiagram (pr1_category D) F) x)
(isL : isLimCone _ x L),
creates_limit _ _ _ isL.
End Creates_Limits.
Section creates_preserves.
Context {C : category}
(D : disp_cat C)
(H : creates_limits D)
(J : graph)
(X : Lims_of_shape J C).
Notation π := (pr1_category D).
Definition total_limits : Lims_of_shape J (total_category D).
Show proof.
intro d.
set (πd := mapdiagram π d).
set (LL := X πd).
set (L := pr1 LL).
set (c := pr1 L).
set (isL := pr2 LL). cbn in isL.
set (XR := H _ d _ _ isL).
unfold creates_limit in XR.
cbn.
use (make_LimCone _ _ _ (pr2 XR)).
set (πd := mapdiagram π d).
set (LL := X πd).
set (L := pr1 LL).
set (c := pr1 L).
set (isL := pr2 LL). cbn in isL.
set (XR := H _ d _ _ isL).
unfold creates_limit in XR.
cbn.
use (make_LimCone _ _ _ (pr2 XR)).
Lemma pr1_preserves_limit (d : diagram J (total_category D))
(x : total_category D) (CC : cone d x) : preserves_limit π _ x CC.
Show proof.
intro H1.
set (XR := X (mapdiagram π d)).
use is_z_iso_isLim.
- apply X.
- match goal with |[ |- is_z_isomorphism ?foo ] => set (T:= foo) end.
destruct X as [[a L] isL]. cbn in isL.
clear XR.
set (tL := H _ _ _ _ isL).
unfold creates_limit in tL.
set (RR := pr1 tL).
set (RT1 := pr2 tL).
set (RX := isLim_is_z_iso _ (make_LimCone _ _ _ RT1) _ _ H1).
set (XR := @functor_on_is_z_isomorphism _ _ π _ _ _ RX).
match goal with |[ H : is_z_isomorphism ?f |- _ ] => set (T':= f) end.
assert (X0 : T' = T).
{
clear XR.
clear RX.
unfold T.
unfold T'.
apply (limArrowUnique (make_LimCone _ _ _ isL)) .
intro j.
set (RRt := make_LimCone _ _ _ RT1).
set (RRtt := limArrowCommutes RRt x CC j).
set (RH := maponpaths (#π)%Cat RRtt).
cbn in RH.
apply RH.
}
rewrite <- X0.
apply XR.
set (XR := X (mapdiagram π d)).
use is_z_iso_isLim.
- apply X.
- match goal with |[ |- is_z_isomorphism ?foo ] => set (T:= foo) end.
destruct X as [[a L] isL]. cbn in isL.
clear XR.
set (tL := H _ _ _ _ isL).
unfold creates_limit in tL.
set (RR := pr1 tL).
set (RT1 := pr2 tL).
set (RX := isLim_is_z_iso _ (make_LimCone _ _ _ RT1) _ _ H1).
set (XR := @functor_on_is_z_isomorphism _ _ π _ _ _ RX).
match goal with |[ H : is_z_isomorphism ?f |- _ ] => set (T':= f) end.
assert (X0 : T' = T).
{
clear XR.
clear RX.
unfold T.
unfold T'.
apply (limArrowUnique (make_LimCone _ _ _ isL)) .
intro j.
set (RRt := make_LimCone _ _ _ RT1).
set (RRtt := limArrowCommutes RRt x CC j).
set (RH := maponpaths (#π)%Cat RRtt).
cbn in RH.
apply RH.
}
rewrite <- X0.
apply XR.
End creates_preserves.