Library UniMath.CategoryTheory.DisplayedCats.MoreFibrations.Prefibrations
Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.PartA.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.categories.HSET.Core.
Require Import UniMath.CategoryTheory.categories.HSET.MonoEpiIso.
Require Import UniMath.CategoryTheory.categories.HSET.Univalence.
Require Import UniMath.CategoryTheory.limits.pullbacks.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.Equivalences.Core.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.CategoryTheory.Presheaf.
Local Open Scope cat.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
Require Import UniMath.Foundations.All.
Local Open Scope type_scope.
Local Open Scope mor_disp_scope.
Require Import UniMath.MoreFoundations.PartA.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.categories.HSET.Core.
Require Import UniMath.CategoryTheory.categories.HSET.MonoEpiIso.
Require Import UniMath.CategoryTheory.categories.HSET.Univalence.
Require Import UniMath.CategoryTheory.limits.pullbacks.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.Equivalences.Core.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.CategoryTheory.Presheaf.
Local Open Scope cat.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
Require Import UniMath.Foundations.All.
Local Open Scope type_scope.
Local Open Scope mor_disp_scope.
The following two equivalent definitions are convenient in different situations.
Definition is_precartesian {C : category} {D : disp_cat C}
{c c' : C} {f : c' --> c}
{d : D c} {d' : D c'} (ff : d' -->[f] d)
: UU
:= forall (d'' : D c') (hh : d'' -->[f] d),
∃! (gg : d'' -->[identity c'] d'), gg ;; ff = transportb _ (id_left _) hh.
Definition is_pre'cartesian {C : category} {D : disp_cat C}
{c c' : C} {f : c' --> c}
{d : D c} {d' : D c'} (ff : d' -->[f] d)
: UU
:= forall (d'' : D c') (hh : d'' -->[identity c' · f] d),
∃! (gg : d'' -->[identity c'] d'), gg ;; ff = hh.
Definition pre'_implies_pre
{C : category} {D : disp_cat C}
{c c' : C} {f : c' --> c}
{d : D c} {d' : D c'} (ff : d' -->[f] d)
: is_pre'cartesian ff -> is_precartesian ff.
Show proof.
Definition pre_implies_pre'
{C : category} {D : disp_cat C}
{c c' : C} {f : c' --> c}
{d : D c} {d' : D c'} (ff : d' -->[f] d)
: is_precartesian ff -> is_pre'cartesian ff.
Show proof.
{c c' : C} {f : c' --> c}
{d : D c} {d' : D c'} (ff : d' -->[f] d)
: UU
:= forall (d'' : D c') (hh : d'' -->[f] d),
∃! (gg : d'' -->[identity c'] d'), gg ;; ff = transportb _ (id_left _) hh.
Definition is_pre'cartesian {C : category} {D : disp_cat C}
{c c' : C} {f : c' --> c}
{d : D c} {d' : D c'} (ff : d' -->[f] d)
: UU
:= forall (d'' : D c') (hh : d'' -->[identity c' · f] d),
∃! (gg : d'' -->[identity c'] d'), gg ;; ff = hh.
Definition pre'_implies_pre
{C : category} {D : disp_cat C}
{c c' : C} {f : c' --> c}
{d : D c} {d' : D c'} (ff : d' -->[f] d)
: is_pre'cartesian ff -> is_precartesian ff.
Show proof.
intros H d'' hh.
apply H.
Coercion pre'_implies_pre : is_pre'cartesian >-> is_precartesian.apply H.
Definition pre_implies_pre'
{C : category} {D : disp_cat C}
{c c' : C} {f : c' --> c}
{d : D c} {d' : D c'} (ff : d' -->[f] d)
: is_precartesian ff -> is_pre'cartesian ff.
Show proof.
See also precartesian_factorisation' below, for when the map one wishes to factor is not judgementally over f, but over some equal map. TODO!
Definition precartesian_factorisation {C : category} {D : disp_cat C}
{c c' : C} {f : c' --> c}
{d : D c} {d' : D c'} {ff : d' -->[f] d} (H : is_precartesian ff)
{d'': D c'} (hh : d'' -->[f] d)
: d'' -->[identity c'] d'
:= pr1 (pr1 (H _ hh)).
Definition pre'cartesian_factorisation {C : category} {D : disp_cat C}
{c c' : C} {f : c' --> c}
{d : D c} {d' : D c'} {ff : d' -->[f] d} (H : is_pre'cartesian ff)
{d'': D c'} (hh : d'' -->[identity c' · f] d)
: d'' -->[identity c'] d'
:= pr1 (pr1 (H _ hh)).
Definition precartesian_factorisation_commutes
{C : category} {D : disp_cat C} {c c' : C} {f : c' --> c}
{d : D c} {d' : D c'} {ff : d' -->[f] d} (H : is_precartesian ff)
{d'': D c'} (hh : d'' -->[f] d)
: precartesian_factorisation H hh ;; ff = transportb _ (id_left _) hh
:= pr2 (pr1 (H _ hh)).
Definition pre'cartesian_factorisation_commutes
{C : category} {D : disp_cat C} {c c' : C} {f : c' --> c}
{d : D c} {d' : D c'} {ff : d' -->[f] d} (H : is_pre'cartesian ff)
{d'': D c'} (hh : d'' -->[identity c' · f] d)
: pre'cartesian_factorisation H hh ;; ff = hh
:= pr2 (pr1 (H _ hh)).
Definition precartesian_factorisation_of_composite
{C : category} {D : disp_cat C}
{c c' : C} {f : c' --> c}
{d : D c} {d' : D c'} {ff : d' -->[f] d} (H : is_precartesian ff)
{d'' : D c'} (gg : d'' -->[identity c'] d')
: gg = precartesian_factorisation H (transportf _ (id_left _) (gg ;; ff)).
Show proof.
Definition pre'cartesian_factorisation_of_composite
{C : category} {D : disp_cat C}
{c c' : C} {f : c' --> c}
{d : D c} {d' : D c'} {ff : d' -->[f] d} (H : is_pre'cartesian ff)
{d'' : D c'} (gg : d'' -->[identity c'] d')
: gg = pre'cartesian_factorisation H (gg ;; ff).
Show proof.
Definition pre'cartesian_factorisation_unique
{C : category} {D : disp_cat C} {c c' : C} {f : c' --> c}
{d : D c} {d' : D c'} {ff : d' -->[f] d} (H : is_pre'cartesian ff)
{d'': D c'} (gg gg' : d'' -->[identity c'] d')
: (gg ;; ff = gg' ;; ff) -> gg = gg'.
Show proof.
intro Hggff.
eapply pathscomp0.
- apply (pre'cartesian_factorisation_of_composite H).
- eapply pathscomp0.
+ apply maponpaths.
exact Hggff.
+ apply pathsinv0.
apply pre'cartesian_factorisation_of_composite.
eapply pathscomp0.
- apply (pre'cartesian_factorisation_of_composite H).
- eapply pathscomp0.
+ apply maponpaths.
exact Hggff.
+ apply pathsinv0.
apply pre'cartesian_factorisation_of_composite.
Definition precartesian_factorisation_unique
{C : category} {D : disp_cat C} {c c' : C} {f : c' --> c}
{d : D c} {d' : D c'} {ff : d' -->[f] d} (H : is_precartesian ff)
{d'': D c'} (gg gg' : d'' -->[identity c'] d')
: (gg ;; ff = gg' ;; ff) -> gg = gg'.
Show proof.
intro Hggff.
eapply pathscomp0.
- apply (precartesian_factorisation_of_composite H).
- eapply pathscomp0.
+ apply maponpaths.
apply maponpaths.
exact Hggff.
+ apply pathsinv0.
apply precartesian_factorisation_of_composite.
eapply pathscomp0.
- apply (precartesian_factorisation_of_composite H).
- eapply pathscomp0.
+ apply maponpaths.
apply maponpaths.
exact Hggff.
+ apply pathsinv0.
apply precartesian_factorisation_of_composite.
Definition isaprop_is_precartesian
{C : category} {D : disp_cat C}
{c c' : C} {f : c' --> c}
{d : D c} {d' : D c'} (ff : d' -->[f] d)
: isaprop (is_precartesian ff).
Show proof.
Definition isaprop_is_pre'cartesian
{C : category} {D : disp_cat C}
{c c' : C} {f : c' --> c}
{d : D c} {d' : D c'} (ff : d' -->[f] d)
: isaprop (is_pre'cartesian ff).
Show proof.
End Precartesian_morphisms.
Section Precartesian_lifts.
Definition precartesian_lift
{C : category} {D : disp_cat C}
{c c' : C} (d : D c) (f : c' --> c)
: UU
:= ∑ (d' : D c') (ff : d' -->[f] d), is_precartesian ff.
Definition pre'cartesian_lift
{C : category} {D : disp_cat C}
{c c' : C} (d : D c) (f : c' --> c)
: UU
:= ∑ (d' : D c') (ff : d' -->[f] d), is_pre'cartesian ff.
Definition object_of_precartesian_lift
{C : category} {D : disp_cat C}
{c c' : C} {d : D c} {f : c' --> c}
(fd : precartesian_lift d f)
: D c'
:= pr1 fd.
Coercion object_of_precartesian_lift : precartesian_lift >-> ob_disp.
Definition object_of_pre'cartesian_lift
{C : category} {D : disp_cat C}
{c c' : C} {d : D c} {f : c' --> c}
(fd : pre'cartesian_lift d f)
: D c'
:= pr1 fd.
Coercion object_of_pre'cartesian_lift : pre'cartesian_lift >-> ob_disp.
Definition mor_disp_of_precartesian_lift
{C : category} {D : disp_cat C}
{c c' : C} {d : D c} {f : c' --> c}
(fd : precartesian_lift d f)
: (fd : D c') -->[f] d
:= pr1 (pr2 fd).
Coercion mor_disp_of_precartesian_lift : precartesian_lift >-> mor_disp.
Definition mor_disp_of_pre'cartesian_lift
{C : category} {D : disp_cat C}
{c c' : C} {d : D c} {f : c' --> c}
(fd : pre'cartesian_lift d f)
: (fd : D c') -->[f] d
:= pr1 (pr2 fd).
Coercion mor_disp_of_pre'cartesian_lift : pre'cartesian_lift >-> mor_disp.
Definition precartesian_lift_is_precartesian
{C : category} {D : disp_cat C}
{c c' : C} {d : D c} {f : c' --> c}
(fd : precartesian_lift d f)
: is_precartesian fd
:= pr2 (pr2 fd).
Coercion precartesian_lift_is_precartesian : precartesian_lift >-> is_precartesian.
Definition pre'cartesian_lift_is_pre'cartesian
{C : category} {D : disp_cat C}
{c c' : C} {d : D c} {f : c' --> c}
(fd : pre'cartesian_lift d f)
: is_pre'cartesian fd
:= pr2 (pr2 fd).
Coercion pre'cartesian_lift_is_pre'cartesian : pre'cartesian_lift >-> is_pre'cartesian.
Definition pre'_implies_precartesian_lift
{C : category} {D : disp_cat C}
{c c' : C} {d : D c} {f : c' --> c}
(fd : pre'cartesian_lift d f)
: precartesian_lift d f.
Show proof.
Coercion pre'_implies_precartesian_lift : pre'cartesian_lift >-> precartesian_lift.
Definition pre_implies_pre'cartesian_lift
{C : category} {D : disp_cat C}
{c c' : C} {d : D c} {f : c' --> c}
(fd : precartesian_lift d f)
: pre'cartesian_lift d f.
Show proof.
End Precartesian_lifts.
Section Precleavages.
Definition precleaving
{C : category} (D : disp_cat C) : UU
:= forall (c c' : C) (f : c' --> c) (d : D c), precartesian_lift d f.
Definition pre'cleaving
{C : category} (D : disp_cat C) : UU
:= forall (c c' : C) (f : c' --> c) (d : D c), pre'cartesian_lift d f.
Definition pre_implies_pre'cleaving
{C : category} (D : disp_cat C)
: precleaving D -> pre'cleaving D.
Show proof.
Coercion pre_implies_pre'cleaving : precleaving >-> pre'cleaving.
Definition pre'_implies_precleaving
{C : category} (D : disp_cat C)
: pre'cleaving D -> precleaving D.
Show proof.
End Precleavages.
Section Prefibrations.
Definition prefibration
(C : category) : UU
:= ∑ (D : disp_cat C), precleaving D.
Definition pre'fibration
(C : category) : UU
:= ∑ (D : disp_cat C), pre'cleaving D.
Definition pre'_implies_prefibration
(C : category)
: pre'fibration C -> prefibration C.
Show proof.
Coercion pre'_implies_prefibration : pre'fibration >-> prefibration.
Definition pre_implies_pre'fibration
(C : category)
: prefibration C -> pre'fibration C.
Show proof.
End Prefibrations.