Library TypeTheory.Displayed_Cats.Fibrations
Definitions of various kinds of fibraitions, using displayed categories.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.CategoryTheory.Categories.
Require Import UniMath.CategoryTheory.limits.pullbacks.
Require Import UniMath.CategoryTheory.category_hset.
Require Import UniMath.CategoryTheory.Adjunctions.
Require Import UniMath.CategoryTheory.equivalences.
Require Import TypeTheory.Auxiliary.Auxiliary.
Require Import TypeTheory.Auxiliary.UnicodeNotations.
Require Import TypeTheory.Displayed_Cats.Auxiliary.
Require Import TypeTheory.Displayed_Cats.Core.
Require Import TypeTheory.Displayed_Cats.Constructions.
Set Automatic Introduction.
Local Open Scope type_scope.
Local Open Scope mor_disp_scope.
Fibratons, opfibrations, and isofibrations are all displayed categories with extra lifting conditions.
Classically, these lifting conditions are usually taken by default as mere existence conditions; when they are given by operations, one speaks of a cloven fibration, etc.
We make the cloven version the default, so is_fibration etc are the cloven notions, and call the mere-existence versions un-cloven.
(This conventional is provisional and and might change in future.)
The easiest to define are isofibrations, since they do not depend on a definition of (co-)cartesian-ness (because all displayed isomorphisms are cartesian).
Isofibrations
Given an iso φ : c' =~ c in C, and an object d in D c,
there’s some object d' in D c', and an iso φbar : d' =~ d over φ.
Definition iso_cleaving {C : category} (D : disp_cat C) : UU
:=
forall (c c' : C) (i : iso c' c) (d : D c),
∑ d' : D c', iso_disp i d' d.
Definition iso_fibration (C : category) : UU
:= ∑ D : disp_cat C, iso_cleaving D.
Definition is_uncloven_iso_cleaving {C : category} (D : disp_cat C) : UU
:=
forall (c c' : C) (i : iso c' c) (d : D c),
∃ d' : D c', iso_disp i d' d.
Definition weak_iso_fibration (C : category) : UU
:= ∑ D : disp_cat C, is_uncloven_iso_cleaving D.
As with fibrations, there is an evident dual version. However, in the iso case, it is self-dual: having forward (i.e. cocartesian) liftings along isos is equivalent to having backward (cartesian) liftings.
Definition is_op_isofibration {C : category} (D : disp_cat C) : UU
:=
forall (c c' : C) (i : iso c c') (d : D c),
∑ d' : D c', iso_disp i d d'.
Lemma is_isofibration_iff_is_op_isofibration
{C : category} (D : disp_cat C)
: iso_cleaving D <-> is_op_isofibration D.
Proof.
Abort.
End Isofibrations.
Section Fibrations.
Definition is_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 c'' (g : c'' --> c') (d'' : D c'') (hh : d'' -->[g;;f] d),
∃! (gg : d'' -->[g] d'), gg ;; ff = hh.
Definition is_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 c'' (g : c'' --> c') (d'' : D c'') (hh : d'' -->[g;;f] d),
∃! (gg : d'' -->[g] d'), gg ;; ff = hh.
See also cartesian_factorisation' below, for when the map one wishes to factor is not judgementally over g;;f, but over some equal map.
Definition 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_cartesian ff)
{c''} (g : c'' --> c') {d'' : D c''} (hh : d'' -->[g;;f] d)
: d'' -->[g] d'
:= pr1 (pr1 (H _ g _ hh)).
Definition 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_cartesian ff)
{c''} (g : c'' --> c') {d'' : D c''} (hh : d'' -->[g;;f] d)
: cartesian_factorisation H g hh ;; ff = hh
:= pr2 (pr1 (H _ g _ hh)).
{c c' : C} {f : c' --> c}
{d : D c} {d' : D c'} {ff : d' -->[f] d} (H : is_cartesian ff)
{c''} (g : c'' --> c') {d'' : D c''} (hh : d'' -->[g;;f] d)
: d'' -->[g] d'
:= pr1 (pr1 (H _ g _ hh)).
Definition 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_cartesian ff)
{c''} (g : c'' --> c') {d'' : D c''} (hh : d'' -->[g;;f] d)
: cartesian_factorisation H g hh ;; ff = hh
:= pr2 (pr1 (H _ g _ hh)).
This is essentially the third access function for is_cartesian, but given in a more usable form than pr2 (H …) would be.
Definition 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_cartesian ff)
{c''} {g : c'' --> c'} {d'' : D c''} (gg gg' : d'' -->[g] d')
: (gg ;; ff = gg' ;; ff) -> gg = gg'.
Proof.
revert gg gg'.
assert (goal' : forall gg : d'' -->[g] d',
gg = cartesian_factorisation H g (gg ;; ff)).
{
intros gg.
exact (maponpaths pr1
(pr2 (H _ g _ (gg ;; ff)) (gg,,idpath _))).
}
intros gg gg' Hggff.
eapply pathscomp0. apply goal'.
eapply pathscomp0. apply maponpaths, Hggff.
apply pathsinv0, goal'.
Qed.
Definition 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_cartesian ff)
{c''} (g : c'' --> c')
{h : c'' --> c} {d'' : D c''} (hh : d'' -->[h] d)
(e : (g ;; f = h)%mor)
: d'' -->[g] d'.
Proof.
simple refine (cartesian_factorisation H g _).
exact (transportb _ e hh).
Defined.
Definition 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_cartesian ff)
{c''} (g : c'' --> c')
{h : c'' --> c} {d'' : D c''} (hh : d'' -->[h] d)
(e : (g ;; f = h)%mor)
: (cartesian_factorisation' H g hh e) ;; ff
= transportb _ e hh.
Proof.
apply cartesian_factorisation_commutes.
Qed.
Definition cartesian_lift {C : category} {D : disp_cat C}
{c} (d : D c) {c' : C} (f : c' --> c)
: UU
:= ∑ (d' : D c') (ff : d' -->[f] d), is_cartesian ff.
Definition object_of_cartesian_lift {C : category} {D : disp_cat C}
{c} (d : D c) {c' : C} (f : c' --> c)
(fd : cartesian_lift d f)
: D c'
:= pr1 fd.
Coercion object_of_cartesian_lift : cartesian_lift >-> ob_disp.
Definition mor_disp_of_cartesian_lift {C : category} {D : disp_cat C}
{c} (d : D c) {c' : C} (f : c' --> c)
(fd : cartesian_lift d f)
: (fd : D c') -->[f] d
:= pr1 (pr2 fd).
Coercion mor_disp_of_cartesian_lift : cartesian_lift >-> mor_disp.
Definition cartesian_lift_is_cartesian {C : category} {D : disp_cat C}
{c} (d : D c) {c' : C} (f : c' --> c)
(fd : cartesian_lift d f)
: is_cartesian fd
:= pr2 (pr2 fd).
Coercion cartesian_lift_is_cartesian : cartesian_lift >-> is_cartesian.
Definition cleaving {C : category} (D : disp_cat C) : UU
:=
forall (c c' : C) (f : c' --> c) (d : D c), cartesian_lift d f.
{C : category} {D : disp_cat C}
{c c' : C} {f : c' --> c}
{d : D c} {d' : D c'} {ff : d' -->[f] d} (H : is_cartesian ff)
{c''} {g : c'' --> c'} {d'' : D c''} (gg gg' : d'' -->[g] d')
: (gg ;; ff = gg' ;; ff) -> gg = gg'.
Proof.
revert gg gg'.
assert (goal' : forall gg : d'' -->[g] d',
gg = cartesian_factorisation H g (gg ;; ff)).
{
intros gg.
exact (maponpaths pr1
(pr2 (H _ g _ (gg ;; ff)) (gg,,idpath _))).
}
intros gg gg' Hggff.
eapply pathscomp0. apply goal'.
eapply pathscomp0. apply maponpaths, Hggff.
apply pathsinv0, goal'.
Qed.
Definition 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_cartesian ff)
{c''} (g : c'' --> c')
{h : c'' --> c} {d'' : D c''} (hh : d'' -->[h] d)
(e : (g ;; f = h)%mor)
: d'' -->[g] d'.
Proof.
simple refine (cartesian_factorisation H g _).
exact (transportb _ e hh).
Defined.
Definition 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_cartesian ff)
{c''} (g : c'' --> c')
{h : c'' --> c} {d'' : D c''} (hh : d'' -->[h] d)
(e : (g ;; f = h)%mor)
: (cartesian_factorisation' H g hh e) ;; ff
= transportb _ e hh.
Proof.
apply cartesian_factorisation_commutes.
Qed.
Definition cartesian_lift {C : category} {D : disp_cat C}
{c} (d : D c) {c' : C} (f : c' --> c)
: UU
:= ∑ (d' : D c') (ff : d' -->[f] d), is_cartesian ff.
Definition object_of_cartesian_lift {C : category} {D : disp_cat C}
{c} (d : D c) {c' : C} (f : c' --> c)
(fd : cartesian_lift d f)
: D c'
:= pr1 fd.
Coercion object_of_cartesian_lift : cartesian_lift >-> ob_disp.
Definition mor_disp_of_cartesian_lift {C : category} {D : disp_cat C}
{c} (d : D c) {c' : C} (f : c' --> c)
(fd : cartesian_lift d f)
: (fd : D c') -->[f] d
:= pr1 (pr2 fd).
Coercion mor_disp_of_cartesian_lift : cartesian_lift >-> mor_disp.
Definition cartesian_lift_is_cartesian {C : category} {D : disp_cat C}
{c} (d : D c) {c' : C} (f : c' --> c)
(fd : cartesian_lift d f)
: is_cartesian fd
:= pr2 (pr2 fd).
Coercion cartesian_lift_is_cartesian : cartesian_lift >-> is_cartesian.
Definition cleaving {C : category} (D : disp_cat C) : UU
:=
forall (c c' : C) (f : c' --> c) (d : D c), cartesian_lift d f.
Definition is_cleaving {C : category} (D : disp_cat C) : UU
:=
forall (c c' : C) (f : c' --> c) (d : D c), ∥ cartesian_lift d f ∥.
Definition weak_fibration (C : category) : UU
:= ∑ D : disp_cat C, is_cleaving D.
Lemma is_iso_from_is_cartesian {C : category} {D : disp_cat C}
{c c' : C} (i : iso c' c) {d : D c} {d'} (ff : d' -->[i] d)
: is_cartesian ff -> is_iso_disp i ff.
Proof.
intros Hff.
simple refine (_,,_); try split.
- simple refine
(cartesian_factorisation' Hff (inv_from_iso i) (id_disp _) _).
apply iso_after_iso_inv.
- apply cartesian_factorisation_commutes'.
- apply (cartesian_factorisation_unique Hff).
etrans. apply assoc_disp_var.
rewrite cartesian_factorisation_commutes'.
etrans. eapply transportf_bind.
etrans. apply mor_disp_transportf_prewhisker.
eapply transportf_bind, id_right_disp.
apply pathsinv0.
etrans. apply mor_disp_transportf_postwhisker.
etrans. eapply transportf_bind, id_left_disp.
apply maponpaths_2, homset_property.
Qed.
Lemma is_isofibration_from_is_fibration {C : category} {D : disp_cat C}
: cleaving D -> iso_cleaving D.
Proof.
intros D_fib c c' f d.
assert (fd := D_fib _ _ f d).
exists (fd : D _).
exists (fd : _ -->[_] _).
apply is_iso_from_is_cartesian; exact fd.
Defined.
Definition cartesian_lifts_iso {C : category} {D : disp_cat C}
{c} {d : D c} {c' : C} {f : c' --> c} (fd fd' : cartesian_lift d f)
: iso_disp (identity_iso c') fd fd'.
Proof.
simple refine (_,,(_,,_)).
- exact (cartesian_factorisation' fd' (identity _) fd (id_left _)).
- exact (cartesian_factorisation' fd (identity _) fd' (id_left _)).
- cbn; split.
+ apply (cartesian_factorisation_unique fd').
etrans. apply assoc_disp_var.
rewrite cartesian_factorisation_commutes'.
etrans. eapply transportf_bind, mor_disp_transportf_prewhisker.
rewrite cartesian_factorisation_commutes'.
etrans. apply transport_f_f.
apply pathsinv0.
etrans. apply mor_disp_transportf_postwhisker.
rewrite id_left_disp.
etrans. apply transport_f_f.
apply maponpaths_2, homset_property.
+ apply (cartesian_factorisation_unique fd).
etrans. apply assoc_disp_var.
rewrite cartesian_factorisation_commutes'.
etrans. eapply transportf_bind, mor_disp_transportf_prewhisker.
rewrite cartesian_factorisation_commutes'.
etrans. apply transport_f_f.
apply pathsinv0.
etrans. apply mor_disp_transportf_postwhisker.
rewrite id_left_disp.
etrans. apply transport_f_f.
apply maponpaths_2, homset_property.
Defined.
Definition cartesian_lifts_iso_commutes {C : category} {D : disp_cat C}
{c} {d : D c} {c' : C} {f : c' --> c} (fd fd' : cartesian_lift d f)
: (cartesian_lifts_iso fd fd') ;; fd'
= transportb _ (id_left _) (fd : _ -->[_] _).
Proof.
cbn. apply cartesian_factorisation_commutes'.
Qed.
In a displayed category (i.e. univalent), cartesian lifts are literally unique, if they exist; that is, the type of cartesian lifts is always a proposition.
Definition isaprop_cartesian_lifts
{C : category} {D : disp_cat C} (D_cat : is_univalent_disp D)
{c} (d : D c) {c' : C} (f : c' --> c)
: isaprop (cartesian_lift d f).
Proof.
apply invproofirrelevance; intros fd fd'.
use total2_paths_f.
{ apply (isotoid_disp D_cat (idpath _)); cbn.
apply cartesian_lifts_iso. }
apply subtypeEquality.
{ intros ff. repeat (apply impred; intro).
apply isapropiscontr. }
etrans.
refine (@functtransportf_2 (D c') _ _ (fun x => pr1) _ _ _ _).
cbn. etrans. apply transportf_precompose_disp.
rewrite idtoiso_isotoid_disp.
refine (pathscomp0 (maponpaths _ _) (transportfbinv _ _ _)).
apply (precomp_with_iso_disp_is_inj (cartesian_lifts_iso fd fd')).
etrans. apply assoc_disp.
etrans. eapply transportf_bind, cancel_postcomposition_disp.
refine (inv_mor_after_iso_disp _).
etrans. eapply transportf_bind, id_left_disp.
apply pathsinv0.
etrans. apply mor_disp_transportf_prewhisker.
etrans. eapply transportf_bind, cartesian_lifts_iso_commutes.
apply maponpaths_2, homset_property.
Defined.
Definition univalent_fibration_is_cloven
{C : category} {D : disp_cat C} (D_cat : is_univalent_disp D)
: is_cleaving D -> cleaving D.
Proof.
intros D_fib c c' f d.
apply (squash_to_prop (D_fib c c' f d)).
apply isaprop_cartesian_lifts; assumption.
auto.
Defined.
End Fibrations.
{C : category} {D : disp_cat C} (D_cat : is_univalent_disp D)
{c} (d : D c) {c' : C} (f : c' --> c)
: isaprop (cartesian_lift d f).
Proof.
apply invproofirrelevance; intros fd fd'.
use total2_paths_f.
{ apply (isotoid_disp D_cat (idpath _)); cbn.
apply cartesian_lifts_iso. }
apply subtypeEquality.
{ intros ff. repeat (apply impred; intro).
apply isapropiscontr. }
etrans.
refine (@functtransportf_2 (D c') _ _ (fun x => pr1) _ _ _ _).
cbn. etrans. apply transportf_precompose_disp.
rewrite idtoiso_isotoid_disp.
refine (pathscomp0 (maponpaths _ _) (transportfbinv _ _ _)).
apply (precomp_with_iso_disp_is_inj (cartesian_lifts_iso fd fd')).
etrans. apply assoc_disp.
etrans. eapply transportf_bind, cancel_postcomposition_disp.
refine (inv_mor_after_iso_disp _).
etrans. eapply transportf_bind, id_left_disp.
apply pathsinv0.
etrans. apply mor_disp_transportf_prewhisker.
etrans. eapply transportf_bind, cartesian_lifts_iso_commutes.
apply maponpaths_2, homset_property.
Defined.
Definition univalent_fibration_is_cloven
{C : category} {D : disp_cat C} (D_cat : is_univalent_disp D)
: is_cleaving D -> cleaving D.
Proof.
intros D_fib c c' f d.
apply (squash_to_prop (D_fib c c' f d)).
apply isaprop_cartesian_lifts; assumption.
auto.
Defined.
End Fibrations.
a proof principle for use with discrete fibrations TODO: upstream
Lemma eq_exists_unique (A : UU) (B : A → UU) (H : iscontr (∑ a : A, B a))
: ∏ a, B a → a = pr1 (iscontrpr1 H).
Proof.
intros a b.
assert (g : ((a,,b) : total2 B)
=
( (pr1 (iscontrpr1 H),, pr2 (iscontrpr1 H)) : total2 B)).
{ etrans. apply (pr2 H). apply tppr. }
apply (maponpaths pr1 g).
Defined.
Section Discrete_Fibrations.
Definition is_discrete_fibration {C : category} (D : disp_cat C) : UU
:=
(forall (c c' : C) (f : c' --> c) (d : D c),
∃! d' : D c', d' -->[f] d)
×
(forall c, isaset (D c)).
Definition discrete_fibration C : UU
:= ∑ D : disp_cat C, is_discrete_fibration D.
Coercion disp_cat_from_discrete_fibration C (D : discrete_fibration C)
: disp_cat C := pr1 D.
Definition unique_lift {C} {D : discrete_fibration C} {c c'}
(f : c' --> c) (d : D c)
: ∃! d' : D c', d' -->[f] d
:= pr1 (pr2 D) c c' f d.
Definition isaset_fiber_discrete_fibration {C} (D : discrete_fibration C)
(c : C) : isaset (D c) := pr2 (pr2 D) c.
: ∏ a, B a → a = pr1 (iscontrpr1 H).
Proof.
intros a b.
assert (g : ((a,,b) : total2 B)
=
( (pr1 (iscontrpr1 H),, pr2 (iscontrpr1 H)) : total2 B)).
{ etrans. apply (pr2 H). apply tppr. }
apply (maponpaths pr1 g).
Defined.
Section Discrete_Fibrations.
Definition is_discrete_fibration {C : category} (D : disp_cat C) : UU
:=
(forall (c c' : C) (f : c' --> c) (d : D c),
∃! d' : D c', d' -->[f] d)
×
(forall c, isaset (D c)).
Definition discrete_fibration C : UU
:= ∑ D : disp_cat C, is_discrete_fibration D.
Coercion disp_cat_from_discrete_fibration C (D : discrete_fibration C)
: disp_cat C := pr1 D.
Definition unique_lift {C} {D : discrete_fibration C} {c c'}
(f : c' --> c) (d : D c)
: ∃! d' : D c', d' -->[f] d
:= pr1 (pr2 D) c c' f d.
Definition isaset_fiber_discrete_fibration {C} (D : discrete_fibration C)
(c : C) : isaset (D c) := pr2 (pr2 D) c.
TODO: move upstream
Lemma pair_inj {A : UU} {B : A -> UU} (is : isaset A) {a : A}
{b b' : B a} : (a,,b) = (a,,b') -> b = b'.
Proof.
intro H.
use (invmaponpathsincl _ _ _ _ H).
apply isofhlevelffib. intro. apply is.
Defined.
Lemma disp_mor_unique_disc_fib C (D : discrete_fibration C)
: ∏ (c c' : C) (f : c --> c') (d : D c) (d' : D c')
(ff ff' : d -->[f] d'), ff = ff'.
Proof.
intros.
assert (XR := unique_lift f d').
assert (foo : ((d,,ff) : ∑ d0, d0 -->[f] d') = (d,,ff')).
{ apply proofirrelevance.
apply isapropifcontr. apply XR.
}
apply (pair_inj (isaset_fiber_discrete_fibration _ _ ) foo).
Defined.
Lemma isaprop_disc_fib_hom C (D : discrete_fibration C)
: ∏ (c c' : C) (f : c --> c') (d : D c) (d' : D c'),
isaprop (d -->[f] d').
Proof.
intros.
apply invproofirrelevance.
intros x x'. apply disp_mor_unique_disc_fib.
Qed.
Definition fibration_from_discrete_fibration C (D : discrete_fibration C)
: cleaving D.
Proof.
intros c c' f d.
mkpair.
- exact (pr1 (iscontrpr1 (unique_lift f d))).
- mkpair.
+ exact (pr2 (iscontrpr1 (unique_lift f d))).
+ intros c'' g db hh.
set (ff := pr2 (iscontrpr1 (unique_lift f d)) ). cbn in ff.
set (d' := pr1 (iscontrpr1 (unique_lift f d))) in *.
set (ggff := pr2 (iscontrpr1 (unique_lift (g;;f) d)) ). cbn in ggff.
set (d'' := pr1 (iscontrpr1 (unique_lift (g;;f) d))) in *.
set (gg := pr2 (iscontrpr1 (unique_lift g d'))). cbn in gg.
set (d3 := pr1 (iscontrpr1 (unique_lift g d'))) in *.
assert (XR : ((d'',, ggff) : ∑ r, r -->[g;;f] d) = (db,,hh)).
{ apply proofirrelevance. apply isapropifcontr. apply (pr2 D). }
assert (XR1 : ((d'',, ggff) : ∑ r, r -->[g;;f] d) = (d3 ,,gg;;ff)).
{ apply proofirrelevance. apply isapropifcontr. apply (pr2 D). }
assert (XT := maponpaths pr1 XR). cbn in XT.
assert (XT1 := maponpaths pr1 XR1). cbn in XT1.
generalize XR.
generalize XR1; clear XR1.
destruct XT.
generalize gg; clear gg.
destruct XT1.
intros gg XR1 XR0.
apply iscontraprop1.
* apply invproofirrelevance.
intros x x'. apply subtypeEquality.
{ intro. apply homsets_disp. }
apply disp_mor_unique_disc_fib.
* exists gg.
cbn.
assert (XX := pair_inj (isaset_fiber_discrete_fibration _ _ ) XR1).
assert (YY := pair_inj (isaset_fiber_discrete_fibration _ _ ) XR0).
etrans. apply (!XX). apply YY.
Defined.
Section Equivalence_disc_fibs_presheaves.
Variable C : category.
Definition precat_of_discrete_fibs_ob_mor : precategory_ob_mor.
Proof.
exists (discrete_fibration C).
intros a b. exact (disp_functor (functor_identity _ ) a b).
Defined.
Definition precat_of_discrete_fibs_data : precategory_data.
Proof.
exists precat_of_discrete_fibs_ob_mor.
split.
- intro.
exact (@disp_functor_identity _ _ ).
- intros ? ? ? f g. exact (disp_functor_composite f g ).
Defined.
Lemma eq_discrete_fib_mor (F G : precat_of_discrete_fibs_ob_mor)
(a b : F --> G)
(H : ∏ x y, pr1 (pr1 a) x y = pr1 (pr1 b) x y)
: a = b.
Proof.
apply subtypeEquality.
{ intro. apply isaprop_disp_functor_axioms. }
use total2_paths_f.
- apply funextsec. intro x.
apply funextsec. intro y.
apply H.
- repeat (apply funextsec; intro).
apply disp_mor_unique_disc_fib.
Qed.
Definition precat_axioms_of_discrete_fibs : is_precategory precat_of_discrete_fibs_data.
Proof.
repeat split; intros;
apply eq_discrete_fib_mor; intros; apply idpath.
Qed.
Definition precat_of_discrete_fibs : precategory
:= (_ ,, precat_axioms_of_discrete_fibs).
Lemma has_homsets_precat_of_discrete_fibs : has_homsets precat_of_discrete_fibs.
Proof.
intros f f'.
apply (isofhleveltotal2 2).
- apply (isofhleveltotal2 2).
+ do 2 (apply impred; intro).
apply isaset_fiber_discrete_fibration.
+ intro. do 6 (apply impred; intro).
apply homsets_disp.
- intro. apply isasetaprop. apply isaprop_disp_functor_axioms.
Qed.
Definition Precat_of_discrete_fibs : category
:= ( precat_of_discrete_fibs ,, has_homsets_precat_of_discrete_fibs).
{b b' : B a} : (a,,b) = (a,,b') -> b = b'.
Proof.
intro H.
use (invmaponpathsincl _ _ _ _ H).
apply isofhlevelffib. intro. apply is.
Defined.
Lemma disp_mor_unique_disc_fib C (D : discrete_fibration C)
: ∏ (c c' : C) (f : c --> c') (d : D c) (d' : D c')
(ff ff' : d -->[f] d'), ff = ff'.
Proof.
intros.
assert (XR := unique_lift f d').
assert (foo : ((d,,ff) : ∑ d0, d0 -->[f] d') = (d,,ff')).
{ apply proofirrelevance.
apply isapropifcontr. apply XR.
}
apply (pair_inj (isaset_fiber_discrete_fibration _ _ ) foo).
Defined.
Lemma isaprop_disc_fib_hom C (D : discrete_fibration C)
: ∏ (c c' : C) (f : c --> c') (d : D c) (d' : D c'),
isaprop (d -->[f] d').
Proof.
intros.
apply invproofirrelevance.
intros x x'. apply disp_mor_unique_disc_fib.
Qed.
Definition fibration_from_discrete_fibration C (D : discrete_fibration C)
: cleaving D.
Proof.
intros c c' f d.
mkpair.
- exact (pr1 (iscontrpr1 (unique_lift f d))).
- mkpair.
+ exact (pr2 (iscontrpr1 (unique_lift f d))).
+ intros c'' g db hh.
set (ff := pr2 (iscontrpr1 (unique_lift f d)) ). cbn in ff.
set (d' := pr1 (iscontrpr1 (unique_lift f d))) in *.
set (ggff := pr2 (iscontrpr1 (unique_lift (g;;f) d)) ). cbn in ggff.
set (d'' := pr1 (iscontrpr1 (unique_lift (g;;f) d))) in *.
set (gg := pr2 (iscontrpr1 (unique_lift g d'))). cbn in gg.
set (d3 := pr1 (iscontrpr1 (unique_lift g d'))) in *.
assert (XR : ((d'',, ggff) : ∑ r, r -->[g;;f] d) = (db,,hh)).
{ apply proofirrelevance. apply isapropifcontr. apply (pr2 D). }
assert (XR1 : ((d'',, ggff) : ∑ r, r -->[g;;f] d) = (d3 ,,gg;;ff)).
{ apply proofirrelevance. apply isapropifcontr. apply (pr2 D). }
assert (XT := maponpaths pr1 XR). cbn in XT.
assert (XT1 := maponpaths pr1 XR1). cbn in XT1.
generalize XR.
generalize XR1; clear XR1.
destruct XT.
generalize gg; clear gg.
destruct XT1.
intros gg XR1 XR0.
apply iscontraprop1.
* apply invproofirrelevance.
intros x x'. apply subtypeEquality.
{ intro. apply homsets_disp. }
apply disp_mor_unique_disc_fib.
* exists gg.
cbn.
assert (XX := pair_inj (isaset_fiber_discrete_fibration _ _ ) XR1).
assert (YY := pair_inj (isaset_fiber_discrete_fibration _ _ ) XR0).
etrans. apply (!XX). apply YY.
Defined.
Section Equivalence_disc_fibs_presheaves.
Variable C : category.
Definition precat_of_discrete_fibs_ob_mor : precategory_ob_mor.
Proof.
exists (discrete_fibration C).
intros a b. exact (disp_functor (functor_identity _ ) a b).
Defined.
Definition precat_of_discrete_fibs_data : precategory_data.
Proof.
exists precat_of_discrete_fibs_ob_mor.
split.
- intro.
exact (@disp_functor_identity _ _ ).
- intros ? ? ? f g. exact (disp_functor_composite f g ).
Defined.
Lemma eq_discrete_fib_mor (F G : precat_of_discrete_fibs_ob_mor)
(a b : F --> G)
(H : ∏ x y, pr1 (pr1 a) x y = pr1 (pr1 b) x y)
: a = b.
Proof.
apply subtypeEquality.
{ intro. apply isaprop_disp_functor_axioms. }
use total2_paths_f.
- apply funextsec. intro x.
apply funextsec. intro y.
apply H.
- repeat (apply funextsec; intro).
apply disp_mor_unique_disc_fib.
Qed.
Definition precat_axioms_of_discrete_fibs : is_precategory precat_of_discrete_fibs_data.
Proof.
repeat split; intros;
apply eq_discrete_fib_mor; intros; apply idpath.
Qed.
Definition precat_of_discrete_fibs : precategory
:= (_ ,, precat_axioms_of_discrete_fibs).
Lemma has_homsets_precat_of_discrete_fibs : has_homsets precat_of_discrete_fibs.
Proof.
intros f f'.
apply (isofhleveltotal2 2).
- apply (isofhleveltotal2 2).
+ do 2 (apply impred; intro).
apply isaset_fiber_discrete_fibration.
+ intro. do 6 (apply impred; intro).
apply homsets_disp.
- intro. apply isasetaprop. apply isaprop_disp_functor_axioms.
Qed.
Definition Precat_of_discrete_fibs : category
:= ( precat_of_discrete_fibs ,, has_homsets_precat_of_discrete_fibs).
Definition preshv_data_from_disc_fib_ob (D : discrete_fibration C)
: functor_data C^op HSET_univalent_category.
Proof.
mkpair.
+ intro c. exists (D c). apply isaset_fiber_discrete_fibration.
+ intros c' c f x. cbn in *.
exact (pr1 (iscontrpr1 (unique_lift f x))).
Defined.
Definition preshv_ax_from_disc_fib_ob (D : discrete_fibration C)
: is_functor (preshv_data_from_disc_fib_ob D).
Proof.
split.
+ intro c; cbn.
apply funextsec; intro x. simpl.
apply pathsinv0. apply eq_exists_unique.
apply id_disp.
+ intros c c' c'' f g. cbn in *.
apply funextsec; intro x.
apply pathsinv0.
apply eq_exists_unique.
eapply comp_disp.
* apply (pr2 (iscontrpr1 (unique_lift g _))).
* apply (pr2 (iscontrpr1 (unique_lift f _ ))).
Qed.
Definition preshv_from_disc_fib_ob (D : discrete_fibration C)
: preShv C := (_ ,, preshv_ax_from_disc_fib_ob D).
Definition foo : functor_data Precat_of_discrete_fibs (preShv C).
Proof.
exists preshv_from_disc_fib_ob.
intros D D' a.
mkpair.
- intro c. simpl.
exact (pr1 a c).
- abstract (
intros x y f; cbn in *;
apply funextsec; intro d;
apply eq_exists_unique;
apply #a;
apply (pr2 (iscontrpr1 (unique_lift f _ )))
).
Defined.
Definition bar : is_functor foo.
Proof.
split.
- intro D. apply nat_trans_eq. { apply has_homsets_HSET. }
intro c . apply idpath.
- intros D E F a b. apply nat_trans_eq. { apply has_homsets_HSET. }
intro c. apply idpath.
Qed.
Definition functor_Disc_Fibs_to_preShvs : functor _ _
:= ( _ ,, bar).
Definition disp_cat_from_preshv (D : preShv C) : disp_cat C.
Proof.
mkpair.
- mkpair.
+ exists (fun c => pr1hSet (pr1 D c)).
intros x y c d f. exact (functor_on_morphisms (pr1 D) f d = c).
+ split.
* intros; cbn in *; apply (toforallpaths _ _ _ (functor_id D x ) _ ).
* intros ? ? ? ? ? ? ? ? X X0; cbn in *;
etrans; [apply (toforallpaths _ _ _ (functor_comp D g f ) _ ) |];
cbn; etrans; [ apply maponpaths; apply X0 |];
apply X.
- abstract (
repeat mkpair; cbn; intros; try apply setproperty;
apply isasetaprop; apply setproperty
).
Defined.
Definition disc_fib_from_preshv (D : preShv C) : discrete_fibration C.
Proof.
mkpair.
- apply (disp_cat_from_preshv D).
- cbn.
split.
+ intros c c' f d. simpl.
use unique_exists.
* apply (functor_on_morphisms (pr1 D) f d).
* apply idpath.
* intro. apply setproperty.
* intros. apply pathsinv0. assumption.
+ intro. simpl. apply setproperty.
Defined.
Definition functor_data_preShv_Disc_fibs
: functor_data (preShv C) Precat_of_discrete_fibs.
Proof.
mkpair.
- apply disc_fib_from_preshv.
- intros F G a.
mkpair.
+ mkpair.
* intros c. apply (pr1 a c).
* intros x y X Y f H;
assert (XR := nat_trans_ax a);
apply pathsinv0; etrans; [|apply (toforallpaths _ _ _ (XR _ _ f))];
cbn; apply maponpaths, (!H).
+ abstract (repeat mkpair; intros; apply setproperty).
Defined.
Definition is_functor_functor_data_preShv_Disc_fibs
: is_functor functor_data_preShv_Disc_fibs .
Proof.
split; unfold functor_idax, functor_compax; intros;
apply eq_discrete_fib_mor; intros; apply idpath.
Qed.
Definition functor_preShvs_to_Disc_Fibs : functor _ _
:= ( _ ,, is_functor_functor_data_preShv_Disc_fibs ).
Definition η_disc_fib : nat_trans (functor_identity _ )
(functor_preShvs_to_Disc_Fibs ∙ functor_Disc_Fibs_to_preShvs).
Proof.
mkpair.
- intro F.
cbn. mkpair.
+ cbn. intro c; apply idfun.
+ intros c c' f. cbn in *. apply idpath.
- abstract (
intros F G a;
apply nat_trans_eq; [ apply has_homsets_HSET |];
intro c ; apply idpath
).
Defined.
Definition ε_disc_fib
: nat_trans (functor_Disc_Fibs_to_preShvs ∙ functor_preShvs_to_Disc_Fibs)
(functor_identity _ ).
Proof.
mkpair.
- intro D.
mkpair.
+ mkpair.
* cbn. intro c; apply idfun.
* intros c c' x y f H. cbn.
set (XR := pr2 (iscontrpr1 (unique_lift f y))). cbn in XR.
apply (transportf (fun t => t -->[f] y) H XR).
+ abstract (split; cbn; unfold idfun; intros; apply disp_mor_unique_disc_fib).
- abstract (intros c c' f; apply eq_discrete_fib_mor; intros; apply idpath).
Defined.
Definition ε_inv_disc_fib
: nat_trans (functor_identity _ )
(functor_Disc_Fibs_to_preShvs ∙ functor_preShvs_to_Disc_Fibs).
Proof.
mkpair.
- intro D.
cbn.
mkpair.
+ mkpair.
* cbn. intro c; apply idfun.
* abstract (
intros c c' x y f H; cbn;
unfold idfun;
apply pathsinv0; apply path_to_ctr; apply H
).
+ abstract (
split;
[ intros x y; apply isaset_fiber_discrete_fibration |];
intros; apply isaset_fiber_discrete_fibration
).
- abstract (intros c c' f; apply eq_discrete_fib_mor; intros; apply idpath).
Defined.
Definition adjunction_data_disc_fib
: adjunction_data (preShv C) Precat_of_discrete_fibs.
Proof.
exists functor_preShvs_to_Disc_Fibs.
exists functor_Disc_Fibs_to_preShvs.
exists η_disc_fib.
exact ε_disc_fib.
Defined.
Lemma forms_equivalence_disc_fib
: forms_equivalence adjunction_data_disc_fib.
Proof.
split.
- intro F.
apply functor_iso_if_pointwise_iso.
intro c. cbn.
set (XR := hset_equiv_is_iso _ _ (idweq (pr1 F c : hSet) )).
apply XR.
- intro F.
apply is_iso_from_is_z_iso.
use (_ ,, (_,,_ )).
+ apply ε_inv_disc_fib.
+ apply eq_discrete_fib_mor.
intros. apply idpath.
+ apply eq_discrete_fib_mor.
intros. apply idpath.
Qed.
Definition adj_equivalence_disc_fib : adj_equivalence_of_precats _ :=
adjointificiation (_ ,, forms_equivalence_disc_fib).
End Equivalence_disc_fibs_presheaves.
End Discrete_Fibrations.
Section Opfibrations.
End Opfibrations.
Section isofibration_from_disp_over_univalent.
Context (C : category)
(Ccat : is_univalent C)
(D : disp_cat C).
Definition iso_cleaving_category : iso_cleaving D.
Proof.
intros c c' i d.
mkpair.
- exact (transportb D (isotoid _ Ccat i) d).
- generalize i. clear i.
apply forall_isotid.
{ apply Ccat. }
intro e. induction e.
cbn.
rewrite isotoid_identity_iso.
cbn.
apply identity_iso_disp.
Defined.
End isofibration_from_disp_over_univalent.