Library UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.Adjunctions.Reflections.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
Require Import UniMath.CategoryTheory.DisplayedCats.Functors.
Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.Limits.Pullbacks.
Local Open Scope cat.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.Adjunctions.Reflections.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
Require Import UniMath.CategoryTheory.DisplayedCats.Functors.
Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.Limits.Pullbacks.
Local Open Scope cat.
Definition left_beck_chevalley_nat_trans
{C₁ C₂ C₃ C₄ : category}
{F : C₁ ⟶ C₂}
{G : C₁ ⟶ C₃}
{H : C₃ ⟶ C₄}
{K : C₂ ⟶ C₄}
(HF : is_right_adjoint F)
(FL := left_adjoint HF)
(η₁ := unit_from_right_adjoint HF)
(HH : is_right_adjoint H)
(HL := left_adjoint HH)
(ε₂ := counit_from_right_adjoint HH)
(τ : nat_z_iso (F ∙ K) (G ∙ H))
: K ∙ HL ⟹ FL ∙ G
:= nat_trans_comp
_ _ _
(post_whisker η₁ (K ∙ HL))
(nat_trans_comp
_ _ _
(pre_whisker
FL
(post_whisker
τ
HL))
(pre_whisker (FL ∙ G) ε₂)).
Proposition left_beck_chevalley_nat_trans_ob
{C₁ C₂ C₃ C₄ : category}
{F : C₁ ⟶ C₂}
{G : C₁ ⟶ C₃}
{H : C₃ ⟶ C₄}
{K : C₂ ⟶ C₄}
(HF : is_right_adjoint F)
(FL := left_adjoint HF)
(η₁ := unit_from_right_adjoint HF)
(HH : is_right_adjoint H)
(HL := left_adjoint HH)
(ε₂ := counit_from_right_adjoint HH)
(τ : nat_z_iso (F ∙ K) (G ∙ H))
(x : C₂)
: left_beck_chevalley_nat_trans HF HH τ x
=
#HL (#K (η₁ x))
· #HL (τ (FL x))
· ε₂ (G (FL x)).
Proof.
apply assoc.
Qed.
{C₁ C₂ C₃ C₄ : category}
{F : C₁ ⟶ C₂}
{G : C₁ ⟶ C₃}
{H : C₃ ⟶ C₄}
{K : C₂ ⟶ C₄}
(HF : is_right_adjoint F)
(FL := left_adjoint HF)
(η₁ := unit_from_right_adjoint HF)
(HH : is_right_adjoint H)
(HL := left_adjoint HH)
(ε₂ := counit_from_right_adjoint HH)
(τ : nat_z_iso (F ∙ K) (G ∙ H))
: K ∙ HL ⟹ FL ∙ G
:= nat_trans_comp
_ _ _
(post_whisker η₁ (K ∙ HL))
(nat_trans_comp
_ _ _
(pre_whisker
FL
(post_whisker
τ
HL))
(pre_whisker (FL ∙ G) ε₂)).
Proposition left_beck_chevalley_nat_trans_ob
{C₁ C₂ C₃ C₄ : category}
{F : C₁ ⟶ C₂}
{G : C₁ ⟶ C₃}
{H : C₃ ⟶ C₄}
{K : C₂ ⟶ C₄}
(HF : is_right_adjoint F)
(FL := left_adjoint HF)
(η₁ := unit_from_right_adjoint HF)
(HH : is_right_adjoint H)
(HL := left_adjoint HH)
(ε₂ := counit_from_right_adjoint HH)
(τ : nat_z_iso (F ∙ K) (G ∙ H))
(x : C₂)
: left_beck_chevalley_nat_trans HF HH τ x
=
#HL (#K (η₁ x))
· #HL (τ (FL x))
· ε₂ (G (FL x)).
Proof.
apply assoc.
Qed.
Section DependentSum.
Context {C : category}
{D : disp_cat C}
(HD : cleaving D).
Definition dependent_sum
{x y : C}
(f : x --> y)
: UU
:= is_right_adjoint
(fiber_functor_from_cleaving D HD f).
Definition comm_nat_z_iso
{w x y z : C}
(f : x --> w)
(g : y --> w)
(h : z --> y)
(k : z --> x)
(p : k · f = h · g)
(F := fiber_functor_from_cleaving D HD f : D[{w}] ⟶ D[{x}])
(G := fiber_functor_from_cleaving D HD g : D[{w}] ⟶ D[{y}])
(H := fiber_functor_from_cleaving D HD h : D[{y}] ⟶ D[{z}])
(K := fiber_functor_from_cleaving D HD k : D[{x}] ⟶ D[{z}])
: nat_z_iso (F ∙ K) (G ∙ H)
:= nat_z_iso_comp
(fiber_functor_from_cleaving_comp_nat_z_iso _ _ _)
(nat_z_iso_comp
(fiber_functor_on_eq_nat_z_iso HD p)
(nat_z_iso_inv
(fiber_functor_from_cleaving_comp_nat_z_iso _ _ _))).
Proposition comm_nat_z_iso_ob
{w x y z : C}
(f : x --> w)
(g : y --> w)
(h : z --> y)
(k : z --> x)
(p : k · f = h · g)
(F := fiber_functor_from_cleaving D HD f : D[{w}] ⟶ D[{x}])
(G := fiber_functor_from_cleaving D HD g : D[{w}] ⟶ D[{y}])
(H := fiber_functor_from_cleaving D HD h : D[{y}] ⟶ D[{z}])
(K := fiber_functor_from_cleaving D HD k : D[{x}] ⟶ D[{z}])
(φ : D[{w}])
: comm_nat_z_iso f g h k p φ
=
fiber_functor_from_cleaving_comp _ _ _ φ
· fiber_functor_on_eq HD p φ
· fiber_functor_from_cleaving_comp_inv _ _ _ φ.
Proof.
apply assoc.
Qed.
Definition left_beck_chevalley
{w x y z : C}
(f : x --> w)
(g : y --> w)
(h : z --> y)
(k : z --> x)
(p : k · f = h · g)
(L₁ : dependent_sum f)
(L₂ : dependent_sum h)
: UU
:= ∏ (a : D[{x}]),
is_z_isomorphism
(left_beck_chevalley_nat_trans L₁ L₂ (comm_nat_z_iso f g h k p) a).
Proposition isaprop_left_beck_chevalley
{w x y z : C}
(f : x --> w)
(g : y --> w)
(h : z --> y)
(k : z --> x)
(p : k · f = h · g)
(L₁ : dependent_sum f)
(L₂ : dependent_sum h)
: isaprop (left_beck_chevalley f g h k p L₁ L₂).
Proof.
use impred ; intro.
apply isaprop_is_z_isomorphism.
Qed.
Definition has_dependent_sums
: UU
:= ∑ (L : ∏ (x y : C) (f : x --> y), dependent_sum f),
∏ (w x y z : C)
(f : x --> w)
(g : y --> w)
(h : z --> y)
(k : z --> x)
(p : k · f = h · g)
(H : isPullback p),
left_beck_chevalley f g h k p (L _ _ f) (L _ _ h).
End DependentSum.
Section DependentSumPoset.
Context {C : category}
{D : disp_cat C}
(HD : cleaving D)
(HD' : locally_propositional D)
(ex : ∏ (Γ₁ Γ₂ : C) (s : Γ₁ --> Γ₂), D[{Γ₁}] → D[{Γ₂}])
(ex_i : ∏ (Γ₁ Γ₂ : C)
(s : Γ₁ --> Γ₂)
(φ : D[{Γ₁}]),
φ -->[ identity _ ] pr1 (HD _ _ s (ex _ _ s φ)))
(ex_e : ∏ (Γ₁ Γ₂ : C)
(s : Γ₁ --> Γ₂)
(ψ : D[{Γ₁}])
(χ : D[{Γ₂}])
(p : ψ -->[ identity _ ] pr1 (HD Γ₂ Γ₁ s χ)),
ex Γ₁ Γ₂ s ψ -->[ identity _ ] χ)
(ex_sub : ∏ (Γ₁ Γ₂ Γ₃ Γ₄ : C)
(s₁ : Γ₂ --> Γ₁)
(s₂ : Γ₃ --> Γ₁)
(s₃ : Γ₄ --> Γ₃)
(s₄ : Γ₄ --> Γ₂)
(p : s₄ · s₁ = s₃ · s₂)
(Hp : isPullback p)
(φ : D[{Γ₂}]),
pr1 (HD Γ₁ Γ₃ s₂ (ex Γ₂ Γ₁ s₁ φ))
-->[ identity _ ]
ex Γ₄ Γ₃ s₃ (pr1 (HD Γ₂ Γ₄ s₄ φ))).
Definition make_dependent_sum_of_mor_poset
{Γ₁ Γ₂ : C}
(s : Γ₁ --> Γ₂)
: dependent_sum HD s.
Proof.
apply reflections_to_is_right_adjoint.
intro x.
use make_reflection'.
- exact (ex _ _ s x).
- exact (ex_i _ _ s x).
- intros p.
use make_reflection_arrow.
+ apply ex_e.
exact (p : _ --> _).
+ abstract apply HD'.
+ intros.
abstract apply HD'.
Defined.
Definition make_has_dependent_sums_poset
: has_dependent_sums HD.
Proof.
simple refine (_ ,, _).
- exact (λ _ _ s, make_dependent_sum_of_mor_poset s).
- abstract
(intros Γ₁ Γ₂ Γ₃ Γ₄ s₁ s₂ s₃ s₄ p Hp φ ;
simple refine (_ ,, _ ,, _) ; [ | apply HD' | apply HD' ] ;
exact (ex_sub _ _ _ _ _ _ _ _ _ Hp φ)).
Defined.
End DependentSumPoset.
Context {C : category}
{D : disp_cat C}
(HD : cleaving D).
Definition dependent_sum
{x y : C}
(f : x --> y)
: UU
:= is_right_adjoint
(fiber_functor_from_cleaving D HD f).
Definition comm_nat_z_iso
{w x y z : C}
(f : x --> w)
(g : y --> w)
(h : z --> y)
(k : z --> x)
(p : k · f = h · g)
(F := fiber_functor_from_cleaving D HD f : D[{w}] ⟶ D[{x}])
(G := fiber_functor_from_cleaving D HD g : D[{w}] ⟶ D[{y}])
(H := fiber_functor_from_cleaving D HD h : D[{y}] ⟶ D[{z}])
(K := fiber_functor_from_cleaving D HD k : D[{x}] ⟶ D[{z}])
: nat_z_iso (F ∙ K) (G ∙ H)
:= nat_z_iso_comp
(fiber_functor_from_cleaving_comp_nat_z_iso _ _ _)
(nat_z_iso_comp
(fiber_functor_on_eq_nat_z_iso HD p)
(nat_z_iso_inv
(fiber_functor_from_cleaving_comp_nat_z_iso _ _ _))).
Proposition comm_nat_z_iso_ob
{w x y z : C}
(f : x --> w)
(g : y --> w)
(h : z --> y)
(k : z --> x)
(p : k · f = h · g)
(F := fiber_functor_from_cleaving D HD f : D[{w}] ⟶ D[{x}])
(G := fiber_functor_from_cleaving D HD g : D[{w}] ⟶ D[{y}])
(H := fiber_functor_from_cleaving D HD h : D[{y}] ⟶ D[{z}])
(K := fiber_functor_from_cleaving D HD k : D[{x}] ⟶ D[{z}])
(φ : D[{w}])
: comm_nat_z_iso f g h k p φ
=
fiber_functor_from_cleaving_comp _ _ _ φ
· fiber_functor_on_eq HD p φ
· fiber_functor_from_cleaving_comp_inv _ _ _ φ.
Proof.
apply assoc.
Qed.
Definition left_beck_chevalley
{w x y z : C}
(f : x --> w)
(g : y --> w)
(h : z --> y)
(k : z --> x)
(p : k · f = h · g)
(L₁ : dependent_sum f)
(L₂ : dependent_sum h)
: UU
:= ∏ (a : D[{x}]),
is_z_isomorphism
(left_beck_chevalley_nat_trans L₁ L₂ (comm_nat_z_iso f g h k p) a).
Proposition isaprop_left_beck_chevalley
{w x y z : C}
(f : x --> w)
(g : y --> w)
(h : z --> y)
(k : z --> x)
(p : k · f = h · g)
(L₁ : dependent_sum f)
(L₂ : dependent_sum h)
: isaprop (left_beck_chevalley f g h k p L₁ L₂).
Proof.
use impred ; intro.
apply isaprop_is_z_isomorphism.
Qed.
Definition has_dependent_sums
: UU
:= ∑ (L : ∏ (x y : C) (f : x --> y), dependent_sum f),
∏ (w x y z : C)
(f : x --> w)
(g : y --> w)
(h : z --> y)
(k : z --> x)
(p : k · f = h · g)
(H : isPullback p),
left_beck_chevalley f g h k p (L _ _ f) (L _ _ h).
End DependentSum.
Section DependentSumPoset.
Context {C : category}
{D : disp_cat C}
(HD : cleaving D)
(HD' : locally_propositional D)
(ex : ∏ (Γ₁ Γ₂ : C) (s : Γ₁ --> Γ₂), D[{Γ₁}] → D[{Γ₂}])
(ex_i : ∏ (Γ₁ Γ₂ : C)
(s : Γ₁ --> Γ₂)
(φ : D[{Γ₁}]),
φ -->[ identity _ ] pr1 (HD _ _ s (ex _ _ s φ)))
(ex_e : ∏ (Γ₁ Γ₂ : C)
(s : Γ₁ --> Γ₂)
(ψ : D[{Γ₁}])
(χ : D[{Γ₂}])
(p : ψ -->[ identity _ ] pr1 (HD Γ₂ Γ₁ s χ)),
ex Γ₁ Γ₂ s ψ -->[ identity _ ] χ)
(ex_sub : ∏ (Γ₁ Γ₂ Γ₃ Γ₄ : C)
(s₁ : Γ₂ --> Γ₁)
(s₂ : Γ₃ --> Γ₁)
(s₃ : Γ₄ --> Γ₃)
(s₄ : Γ₄ --> Γ₂)
(p : s₄ · s₁ = s₃ · s₂)
(Hp : isPullback p)
(φ : D[{Γ₂}]),
pr1 (HD Γ₁ Γ₃ s₂ (ex Γ₂ Γ₁ s₁ φ))
-->[ identity _ ]
ex Γ₄ Γ₃ s₃ (pr1 (HD Γ₂ Γ₄ s₄ φ))).
Definition make_dependent_sum_of_mor_poset
{Γ₁ Γ₂ : C}
(s : Γ₁ --> Γ₂)
: dependent_sum HD s.
Proof.
apply reflections_to_is_right_adjoint.
intro x.
use make_reflection'.
- exact (ex _ _ s x).
- exact (ex_i _ _ s x).
- intros p.
use make_reflection_arrow.
+ apply ex_e.
exact (p : _ --> _).
+ abstract apply HD'.
+ intros.
abstract apply HD'.
Defined.
Definition make_has_dependent_sums_poset
: has_dependent_sums HD.
Proof.
simple refine (_ ,, _).
- exact (λ _ _ s, make_dependent_sum_of_mor_poset s).
- abstract
(intros Γ₁ Γ₂ Γ₃ Γ₄ s₁ s₂ s₃ s₄ p Hp φ ;
simple refine (_ ,, _ ,, _) ; [ | apply HD' | apply HD' ] ;
exact (ex_sub _ _ _ _ _ _ _ _ _ Hp φ)).
Defined.
End DependentSumPoset.
Section DependentSum.
Context {C : category}
{D : disp_cat C}
{HD : cleaving D}
(S : has_dependent_sums HD)
{x y : C}
(f : x --> y).
Definition dep_sum
(xx : D[{x}])
: D[{y}]
:= left_adjoint (pr1 S x y f) xx.
Definition dep_sum_mor
{xx₁ xx₂ : D[{x}]}
(ff : xx₁ --> xx₂)
: dep_sum xx₁ --> dep_sum xx₂
:= #(left_adjoint (pr1 S x y f)) ff.
Definition dep_sum_unit
(xx : D[{x}])
: xx -->[ identity x ] fiber_functor_from_cleaving D HD f (dep_sum xx)
:= unit_from_right_adjoint (pr1 S x y f) xx.
Definition dep_sum_counit
(yy : D[{y}])
: dep_sum (fiber_functor_from_cleaving D HD f yy) -->[ identity y ] yy
:= counit_from_right_adjoint (pr1 S x y f) yy.
End DependentSum.
Context {C : category}
{D : disp_cat C}
{HD : cleaving D}
(S : has_dependent_sums HD)
{x y : C}
(f : x --> y).
Definition dep_sum
(xx : D[{x}])
: D[{y}]
:= left_adjoint (pr1 S x y f) xx.
Definition dep_sum_mor
{xx₁ xx₂ : D[{x}]}
(ff : xx₁ --> xx₂)
: dep_sum xx₁ --> dep_sum xx₂
:= #(left_adjoint (pr1 S x y f)) ff.
Definition dep_sum_unit
(xx : D[{x}])
: xx -->[ identity x ] fiber_functor_from_cleaving D HD f (dep_sum xx)
:= unit_from_right_adjoint (pr1 S x y f) xx.
Definition dep_sum_counit
(yy : D[{y}])
: dep_sum (fiber_functor_from_cleaving D HD f yy) -->[ identity y ] yy
:= counit_from_right_adjoint (pr1 S x y f) yy.
End DependentSum.
Definition preserves_dependent_sums
{C₁ C₂ : category}
{D₁ : disp_cat C₁}
{HD₁ : cleaving D₁}
{D₂ : disp_cat C₂}
{HD₂ : cleaving D₂}
{F : C₁ ⟶ C₂}
(FF : cartesian_disp_functor F D₁ D₂)
(L₁ : has_dependent_sums HD₁)
(L₂ : has_dependent_sums HD₂)
: UU
:= ∏ (x y : C₁)
(f : x --> y)
(a : D₁[{x}]),
is_z_isomorphism
(left_beck_chevalley_nat_trans
(pr1 L₁ x y f)
(pr1 L₂ (F x) (F y) (#F f))
(nat_z_iso_inv
(fiber_functor_natural_nat_z_iso HD₁ HD₂ FF f))
a).
Proposition isaprop_preserves_dependent_sums
{C₁ C₂ : category}
{D₁ : disp_cat C₁}
{HD₁ : cleaving D₁}
{D₂ : disp_cat C₂}
{HD₂ : cleaving D₂}
{F : C₁ ⟶ C₂}
(FF : cartesian_disp_functor F D₁ D₂)
(L₁ : has_dependent_sums HD₁)
(L₂ : has_dependent_sums HD₂)
: isaprop (preserves_dependent_sums FF L₁ L₂).
Proof.
do 4 (use impred ; intro).
apply isaprop_is_z_isomorphism.
Qed.
{C₁ C₂ : category}
{D₁ : disp_cat C₁}
{HD₁ : cleaving D₁}
{D₂ : disp_cat C₂}
{HD₂ : cleaving D₂}
{F : C₁ ⟶ C₂}
(FF : cartesian_disp_functor F D₁ D₂)
(L₁ : has_dependent_sums HD₁)
(L₂ : has_dependent_sums HD₂)
: UU
:= ∏ (x y : C₁)
(f : x --> y)
(a : D₁[{x}]),
is_z_isomorphism
(left_beck_chevalley_nat_trans
(pr1 L₁ x y f)
(pr1 L₂ (F x) (F y) (#F f))
(nat_z_iso_inv
(fiber_functor_natural_nat_z_iso HD₁ HD₂ FF f))
a).
Proposition isaprop_preserves_dependent_sums
{C₁ C₂ : category}
{D₁ : disp_cat C₁}
{HD₁ : cleaving D₁}
{D₂ : disp_cat C₂}
{HD₂ : cleaving D₂}
{F : C₁ ⟶ C₂}
(FF : cartesian_disp_functor F D₁ D₂)
(L₁ : has_dependent_sums HD₁)
(L₂ : has_dependent_sums HD₂)
: isaprop (preserves_dependent_sums FF L₁ L₂).
Proof.
do 4 (use impred ; intro).
apply isaprop_is_z_isomorphism.
Qed.