Library UniMath.CategoryTheory.DisplayedCats.Constructions


Some important constructions on displayed categories
Partial contents:
  • Full subcategory as total category of a displayed category
  • Displayed category given by a structure on objects and a proposition on morphisms of the base category
  • Direct products of displayed categories (and their projections)
  • Sigmas of displayed categories
  • Displayed functor cat
  • Fiber cats

Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.All.
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.DisplayedCats.Auxiliary.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.FunctorCategory.
Local Open Scope cat.
Local Open Scope mor_disp_scope.

Section Auxiliary.

Lemma isweqcontrprop (X Y : UU) (f : X → Y) :
  iscontr X → isaprop Y → isweq f.
Proof.
  intros HX HY.
  apply isweqimplimpl.
  - intros. apply HX.
  - apply isapropifcontr. apply HX.
  - apply HY.
Defined.

Lemma transportf_pathsinv0_var :
∏ {X : UU} {P : X → UU} {x y : X} {p : x = y} {u : P x}
{v : P y}, transportf P p u = v → transportf P (!p) v = u.
Proof.
  intros. induction p. apply (!X0).
Defined.

End Auxiliary.

Full subcategories


Section full_subcat.

Definition disp_full_sub_ob_mor (C : precategory_ob_mor) (P : C → UU)
  : disp_cat_ob_mor C
  := (P,, (λ a b aa bb f, unit)).

Definition disp_full_sub_id_comp (C : precategory_data) (P : C → UU)
  : disp_cat_id_comp C (disp_full_sub_ob_mor C P).
Proof.
  split; intros; apply tt.
Defined.

Definition disp_full_sub_data (C : precategory_data) (P : C → UU)
  : disp_cat_data C
  := disp_full_sub_ob_mor C P,, disp_full_sub_id_comp C P.

Definition disp_full_sub_axioms (C : precategory) (P : C → UU)
  : disp_cat_axioms _ (disp_full_sub_data C P).
Proof.
  repeat split; intros; try (apply proofirrelevance; apply isapropunit).
  apply isasetaprop; apply isapropunit.
Qed.

Definition disp_full_sub (C : precategory) (P : C → UU)
  : disp_precat C := _ ,, disp_full_sub_axioms C P.

Lemma disp_full_sub_univalent (C : category) (P : C → UU) :
  (∏ x : C, isaprop (P x)) →
  is_univalent_disp (disp_full_sub C P).
Proof.
  intro HP.
  apply is_univalent_disp_from_fibers.
  intros x xx xx'. cbn in ×.
  apply isweqcontrprop. apply HP.
  apply isofhleveltotal2.
  - apply isapropunit.
  - intros ?. apply (@isaprop_is_iso_disp _ (disp_full_sub C P)).
Defined.

End full_subcat.

Displayed category from structure on objects and compatibility on morphisms


Section struct_hom.

Variable C : category.
Variable P : ob C → UU.
Variable H : ∏ (x y : C), P x → P y → C⟦x,y⟧ → UU.
Arguments H {_ _} _ _ _ .
Variable Hisprop : ∏ x y a b (f : C⟦x,y⟧), isaprop (H a b f).
Variable Hid : ∏ (x : C) (a : P x), H a a (identity _ ).
Variable Hcomp : ∏ (x y z : C) a b c (f : C⟦x,y⟧) (g : C⟦y,z⟧),
                 H a b f → H b c g → H a c (f · g).

Definition disp_struct_ob_mor : disp_cat_ob_mor C.
Proof.
  ∃ P.
  intros ? ? f a b; exact (H f a b ).
Defined.

Definition disp_struct_id_comp : disp_cat_id_comp _ disp_struct_ob_mor.
Proof.
  split; cbn; intros.
  - apply Hid.
  - eapply Hcomp. apply X. apply X0.
Qed.

Definition disp_struct_data : disp_cat_data C := _ ,, disp_struct_id_comp.

Definition disp_struct_axioms : disp_cat_axioms _ disp_struct_data.
Proof.
  repeat split; intros; try (apply proofirrelevance; apply Hisprop).
  apply isasetaprop; apply Hisprop.
Qed.

Definition disp_struct : disp_cat C := _ ,, disp_struct_axioms.

End struct_hom.

Products of displayed (pre)categories

We directly define direct products of displayed categories over a base.
An alternative would be to define the direct product as the sigma_disp_cat of the pullback to either factor.

Definition dirprod_disp_cat_ob_mor
           {C : precategory_ob_mor} (D1 D2 : disp_cat_ob_mor C)
  : disp_cat_ob_mor C.
Proof.
  ∃ (λ c, D1 c × D2 c).
  intros x y xx yy f.
  exact (pr1 xx -->[f] pr1 yy × pr2 xx -->[f] pr2 yy).
Defined.

Definition dirprod_disp_cat_id_comp
           {C : precategory_data}
           (D1 D2 : disp_cat_data C)
  : disp_cat_id_comp _ (dirprod_disp_cat_ob_mor D1 D2).
Proof.
  apply tpair.
  - intros x (x1, x2).
    exact (id_disp x1,, id_disp x2).
  - intros x y z f g xx yy zz ff gg.
    exact ((pr1 ff ;; pr1 gg),, (pr2 ff ;; pr2 gg)).
Defined.

Definition dirprod_disp_cat_data
           {C : precategory_data}
           (D1 D2 : disp_cat_data C)
  : disp_cat_data C
  := (_ ,, dirprod_disp_cat_id_comp D1 D2).

Section Dirprod.

Context {C : category} (D1 D2 : disp_cat C).

Definition dirprod_disp_cat_axioms
  : disp_cat_axioms _ (dirprod_disp_cat_data D1 D2).
Proof.
  repeat apply make_dirprod.
  - intros. apply dirprod_paths; use (id_left_disp @ !_).
    + use pr1_transportf.
    + apply pr2_transportf.
  - intros. apply dirprod_paths; use (id_right_disp @ !_).
    + use pr1_transportf.
    + apply pr2_transportf.
  - intros. apply dirprod_paths; use (assoc_disp @ !_).
    + use pr1_transportf.
    + apply pr2_transportf.
  - intros. apply isaset_dirprod; apply homsets_disp.
Qed.

Definition dirprod_disp_cat : disp_cat C
  := (_ ,, dirprod_disp_cat_axioms).

Characterization of the isomorphisms of the direct product of displayed categories

TODO: generalize over an aritrary base isomorphism
Definition iso_disp_prod1
      {x : C}
      (xx1 xx1' : D1 x)
      (xx2 xx2' : D2 x) :
  @iso_disp _ dirprod_disp_cat _ _ (identity_iso x) (xx1,, xx2) (xx1',, xx2') →
  (iso_disp (identity_iso x) xx1 xx1') × (iso_disp (identity_iso x) xx2 xx2').
Proof.
  unfold iso_disp. cbn.
  intros [[f1 f2] Hff].
  destruct Hff as [[g1 g2] Hfg].
  cbn in Hfg. destruct Hfg as [Hgf Hfg].
  use tpair.
  - ∃ f1, g1.
    split.
    + etrans. apply (maponpaths dirprod_pr1 Hgf).
      apply pr1_transportf.
    + etrans. apply (maponpaths dirprod_pr1 Hfg).
      apply pr1_transportf.
  - ∃ f2, g2.
    split.
    + etrans. apply (maponpaths dirprod_pr2 Hgf).
      apply pr2_transportf.
    + etrans. apply (maponpaths dirprod_pr2 Hfg).
      apply pr2_transportf.
Defined.

Definition iso_disp_prod2
      {x : C}
      (xx1 xx1' : D1 x)
      (xx2 xx2' : D2 x) :
  (iso_disp (identity_iso x) xx1 xx1') × (iso_disp (identity_iso x) xx2 xx2') →
  @iso_disp _ dirprod_disp_cat _ _ (identity_iso x) (xx1,, xx2) (xx1',, xx2').
Proof.
  unfold iso_disp. cbn.
  intros [[f1 Hf1] [f2 Hf2]].
  destruct Hf1 as [g1 [Hgf1 Hfg1]].
  destruct Hf2 as [g2 [Hgf2 Hfg2]].
  ∃ (f1,,f2), (g1,,g2).
  split.
  - apply dirprod_paths.
    + etrans. apply Hgf1.
      apply pathsinv0. apply pr1_transportf.
    + etrans. apply Hgf2.
      apply pathsinv0. apply pr2_transportf.
  - apply dirprod_paths.
    + etrans. apply Hfg1.
      apply pathsinv0. apply pr1_transportf.
    + etrans. apply Hfg2.
      apply pathsinv0. apply pr2_transportf.
Defined.

Lemma iso_disp_prod21
      {x : C}
      (xx1 xx1' : D1 x)
      (xx2 xx2' : D2 x)
      i
:
  iso_disp_prod2 xx1 xx1' xx2 xx2' (iso_disp_prod1 xx1 xx1' xx2 xx2' i) = i.
Proof.
  apply eq_iso_disp. cbn. reflexivity.
Qed.

Lemma iso_disp_prod12
      {x : C}
      (xx1 xx1' : D1 x)
      (xx2 xx2' : D2 x)
      (t : iso_disp (identity_iso x) xx1 xx1' × iso_disp (identity_iso x) xx2 xx2')
:
  iso_disp_prod1 xx1 xx1' xx2 xx2' (iso_disp_prod2 xx1 xx1' xx2 xx2' t) = t.
Proof.
  apply dirprod_paths.
  - apply eq_iso_disp. cbn. reflexivity.
  - apply eq_iso_disp. cbn. reflexivity.
Qed.

Lemma iso_disp_prod_weq
      (x : C)
      (xx1 xx1' : D1 x)
      (xx2 xx2' : D2 x) :
  @iso_disp _ dirprod_disp_cat _ _ (identity_iso x) (xx1,, xx2) (xx1',, xx2') ≃
  (iso_disp (identity_iso x) xx1 xx1') × (iso_disp (identity_iso x) xx2 xx2').
Proof.
  ∃ (iso_disp_prod1 xx1 xx1' xx2 xx2').
  use gradth.
  - apply iso_disp_prod2.
  - apply iso_disp_prod21.
  - apply iso_disp_prod12.
Defined.

Lemma iso_disp_aux_weq
      (U1 : is_univalent_in_fibers D1)
      (U2 : is_univalent_in_fibers D2)
      (x : C)
      (xx xx' : D1 x × D2 x)

:
  xx = xx'
    ≃ @iso_disp _ dirprod_disp_cat _ _ (identity_iso x) xx xx'.
Proof.
  eapply weqcomp. apply pathsdirprodweq.
  apply invweq. eapply weqcomp. apply iso_disp_prod_weq.
  apply invweq.
  apply weqdirprodf.
  - ∃ idtoiso_fiber_disp. apply U1.
  - ∃ idtoiso_fiber_disp. apply U2.
Defined.

Lemma dirprod_disp_cat_is_univalent :
  is_univalent_disp D1 →
  is_univalent_disp D2 →
  is_univalent_disp dirprod_disp_cat.
Proof.
  intros HD1 HD2.
  apply is_univalent_disp_from_fibers.
  intros x xx xx'.
  use isweqhomot.
  - apply iso_disp_aux_weq.
    + apply is_univalent_in_fibers_from_univalent_disp.
      apply HD1.
    + apply is_univalent_in_fibers_from_univalent_disp.
      apply HD2.
  - intros p. induction p. cbn.
    apply (@eq_iso_disp _ dirprod_disp_cat).
    reflexivity.
  - apply iso_disp_aux_weq.
Defined.

Definition dirprodpr1_disp_functor_data
  : disp_functor_data (functor_identity C) dirprod_disp_cat (D1).
Proof.
  use tpair.
  - intros x xx; exact (pr1 xx).
  - intros x y xx yy f ff; exact (pr1 ff).
Defined.

Definition dirprodpr1_disp_functor_axioms
  : disp_functor_axioms dirprodpr1_disp_functor_data.
Proof.
  split.
  - intros; apply idpath.
  - intros; apply idpath.
Qed.

Definition dirprodpr1_disp_functor
  : disp_functor (functor_identity C) dirprod_disp_cat (D1)
:= (dirprodpr1_disp_functor_data,, dirprodpr1_disp_functor_axioms).

Definition dirprodpr2_disp_functor_data
  : disp_functor_data (functor_identity C) dirprod_disp_cat (D2).
Proof.
  use tpair.
  - intros x xx; exact (pr2 xx).
  - intros x y xx yy f ff; exact (pr2 ff).
Defined.

Definition dirprodpr2_disp_functor_axioms
  : disp_functor_axioms dirprodpr2_disp_functor_data.
Proof.
  split.
  - intros; apply idpath.
  - intros; apply idpath.
Qed.

Definition dirprodpr2_disp_functor
  : disp_functor (functor_identity C) dirprod_disp_cat (D2)
:= (dirprodpr2_disp_functor_data,, dirprodpr2_disp_functor_axioms).

End Dirprod.

Declare Scope disp_cat_scope.
Notation "D1 × D2" := (dirprod_disp_cat D1 D2) : disp_cat_scope.
Delimit Scope disp_cat_scope with disp_cat.
Bind Scope disp_cat_scope with disp_cat.

Sigmas of displayed (pre)categories

Section Sigma.

Context {C : category}
        {D : disp_cat C}
        (E : disp_cat (total_category D)).

Definition sigma_disp_cat_ob_mor : disp_cat_ob_mor C.
Proof.
  ∃ (λ c, ∑ (d : D c), (E (c,,d))).
  intros x y xx yy f.
  exact (∑ (fD : pr1 xx -->[f] pr1 yy),
                (pr2 xx -->[f,,fD] pr2 yy)).
Defined.

Definition sigma_disp_cat_id_comp
  : disp_cat_id_comp _ sigma_disp_cat_ob_mor.
Proof.
  apply tpair.
  - intros x xx.
    ∃ (id_disp _). exact (id_disp (pr2 xx)).
  - intros x y z f g xx yy zz ff gg.
    ∃ (pr1 ff ;; pr1 gg). exact (pr2 ff ;; pr2 gg).
Defined.

Definition sigma_disp_cat_data : disp_cat_data C
  := (_ ,, sigma_disp_cat_id_comp).

Definition sigma_disp_cat_axioms
  : disp_cat_axioms _ sigma_disp_cat_data.
Proof.
  repeat apply tpair.
  - intros. use total2_reassoc_paths'.
    + apply id_left_disp.
    + etrans. exact (@id_left_disp _ _ _ _ _ _ _ (pr2 ff)).
      apply maponpaths_2, homset_property.
  - intros. use total2_reassoc_paths'.
    + apply id_right_disp.
    + etrans. exact (@id_right_disp _ _ _ _ _ _ _ (pr2 ff)).
      apply maponpaths_2, homset_property.
  - intros. use total2_reassoc_paths'.
    + apply assoc_disp.
    + etrans.
        exact (@assoc_disp _ _
                 _ _ _ _ _ _ _
                 _ _ _ _ (pr2 ff) (pr2 gg) (pr2 hh)).
      apply maponpaths_2, homset_property.
  - intros. apply isaset_total2; intros; apply homsets_disp.
Qed.

Definition sigma_disp_cat : disp_cat C
  := (_ ,, sigma_disp_cat_axioms).

Definition sigmapr1_disp_functor_data
  : disp_functor_data (functor_identity C) sigma_disp_cat D.
Proof.
  use tpair.
  - intros x xx; exact (pr1 xx).
  - intros x y xx yy f ff; exact (pr1 ff).
Defined.

Definition sigmapr1_disp_functor_axioms
  : disp_functor_axioms sigmapr1_disp_functor_data.
Proof.
  split.
  - intros; apply idpath.
  - intros; apply idpath.
Qed.

Definition sigmapr1_disp_functor
  : disp_functor (functor_identity C) sigma_disp_cat D
:= (sigmapr1_disp_functor_data,, sigmapr1_disp_functor_axioms).


Transport and isomorphism lemmas


Lemma pr1_transportf_sigma_disp {x y : C} {f f' : x --> y} (e : f = f')
    {xxx : sigma_disp_cat x} {yyy} (fff : xxx -->[f] yyy)
  : pr1 (transportf _ e fff) = transportf _ e (pr1 fff).
Proof.
  destruct e; apply idpath.
Qed.

Lemma pr2_transportf_sigma_disp {x y : C} {f f' : x --> y} (e : f = f')
    {xxx : sigma_disp_cat x} {yyy} (fff : xxx -->[f] yyy)
  : pr2 (transportf _ e fff)
  = transportf (λ ff, pr2 xxx -->[ff] _ ) (two_arg_paths_f e (! pr1_transportf_sigma_disp e fff))
      (pr2 fff).
Proof.
  destruct e. apply pathsinv0.
  etrans. apply maponpaths_2, maponpaths, maponpaths.
  apply (homsets_disp _ _ _ (idpath _)).
  apply idpath.
Qed.

Univalence


Local Open Scope hide_transport_scope.

Definition is_iso_sigma_disp_aux1
    {x y} {xxx : sigma_disp_cat x} {yyy : sigma_disp_cat y}
    {f : iso x y} (fff : xxx -->[f] yyy)
    (ii : is_iso_disp f (pr1 fff))
    (ffi := (_,, ii) : iso_disp f (pr1 xxx) (pr1 yyy))
    (iii : is_iso_disp (@total_iso _ _ (_,,_) (_,,_) f ffi) (pr2 fff))
  : yyy -->[inv_from_iso f] xxx.
Proof.
  ∃ (inv_mor_disp_from_iso ii).
  set (ggg := inv_mor_disp_from_iso iii).
  exact (transportf _ (inv_mor_total_iso _ _) ggg).
Defined.

Lemma is_iso_sigma_disp_aux2
    {x y} {xxx : sigma_disp_cat x} {yyy : sigma_disp_cat y}
    {f : iso x y} (fff : xxx -->[f] yyy)
    (ii : is_iso_disp f (pr1 fff))
    (ffi := (_,, ii) : iso_disp f (pr1 xxx) (pr1 yyy))
    (iii : is_iso_disp (@total_iso _ _ (_,,_) (_,,_) f ffi) (pr2 fff))
  : (is_iso_sigma_disp_aux1 fff ii iii) ;; fff
    = transportb _ (iso_after_iso_inv f) (id_disp yyy)
  ×
      fff ;; (is_iso_sigma_disp_aux1 fff ii iii)
    = transportb _ (iso_inv_after_iso f) (id_disp xxx).
Proof.
  split.
  - use total2_paths_f.
    + abstract ( etrans;
        [ apply iso_disp_after_inv_mor
        | apply pathsinv0, pr1_transportf_sigma_disp]).
    + etrans. 2: apply @pathsinv0, pr2_transportf_sigma_disp.
      etrans. apply maponpaths.
        use (mor_disp_transportf_postwhisker
          (@inv_mor_total_iso _ _ (_,,_) (_,,_) f ffi) _ (pr2 fff)).
      etrans. apply functtransportf.
      etrans. apply transport_f_f.
      etrans. eapply transportf_bind.
        apply (iso_disp_after_inv_mor iii).
      apply maponpaths_2, (@homset_property (total_category D)).
  - use total2_paths_f; cbn.
    + abstract ( etrans;
        [ apply inv_mor_after_iso_disp
        | apply pathsinv0, pr1_transportf_sigma_disp ]).
    + etrans. 2: apply @pathsinv0, pr2_transportf_sigma_disp.
      etrans. apply maponpaths.
      use (mor_disp_transportf_prewhisker
        (@inv_mor_total_iso _ _ (_,,_) (_,,_) f ffi) (pr2 fff) _).
      etrans. apply functtransportf.
      etrans. apply transport_f_f.
      etrans. eapply transportf_bind.
        apply (inv_mor_after_iso_disp iii).
      apply maponpaths_2, (@homset_property (total_category D)).
Qed.

Lemma is_iso_sigma_disp
    {x y} {xxx : sigma_disp_cat x} {yyy : sigma_disp_cat y}
    {f : iso x y} (fff : xxx -->[f] yyy)
    (ii : is_iso_disp f (pr1 fff))
    (ffi := (_,, ii) : iso_disp f (pr1 xxx) (pr1 yyy))
    (iii : is_iso_disp (@total_iso _ _ (_,,_) (_,,_) f ffi) (pr2 fff))
  : is_iso_disp f fff.
Proof.
  ∃ (is_iso_sigma_disp_aux1 fff ii iii).
  apply is_iso_sigma_disp_aux2.
Defined.

Definition sigma_disp_iso
    {x y} (xx : sigma_disp_cat x) (yy : sigma_disp_cat y)
    {f : iso x y} (ff : iso_disp f (pr1 xx) (pr1 yy))
    (fff : iso_disp (@total_iso _ _ (_,,_) (_,,_) f ff) (pr2 xx) (pr2 yy))
  : iso_disp f xx yy.
Proof.
  ∃ (pr1 ff,, pr1 fff). use is_iso_sigma_disp; cbn.
  - exact (pr2 ff).
  - exact (pr2 fff).
Defined.

Definition sigma_disp_iso_map
    {x y} (xx : sigma_disp_cat x) (yy : sigma_disp_cat y)
    (f : iso x y)
  : (∑ ff : iso_disp f (pr1 xx) (pr1 yy),
       iso_disp (@total_iso _ _ (_,,_) (_,,_) f ff) (pr2 xx) (pr2 yy))
  → iso_disp f xx yy
:= λ ff, sigma_disp_iso _ _ (pr1 ff) (pr2 ff).

Lemma sigma_disp_isweq_iso
    {x y} (xx : sigma_disp_cat x) (yy : sigma_disp_cat y)
    (f : iso x y)
  : isweq (sigma_disp_iso_map xx yy f).
Proof.
Abort.



End Sigma.

Displayed functor category

Displayed functors and natural transformations form a displayed category over the ordinary functor category between the bases.

Section Functor.

Variables C' C : category.
Variable D' : disp_cat C'.
Variable D : disp_cat C.

Let FunctorsC'C := functor_category C' C.

Lemma disp_nat_trans_transportf
  (F' F : functor C' C)
  (a' a : nat_trans F' F)
  (p : a' = a )
  (FF' : disp_functor F' D' D)
  (FF : disp_functor F D' D)
  (b : disp_nat_trans a' FF' FF)
  (c' : C')
  (xx' : D' c')
  :
  pr1 (transportf (λ x, disp_nat_trans x FF' FF) p b) c' xx' =
      transportf (mor_disp (FF' c' xx') (FF c' xx'))
           (nat_trans_eq_pointwise p _ ) (b c' xx').
Proof.
  induction p.
  assert (XR : nat_trans_eq_pointwise (idpath a') c' = idpath _ ).
  { apply homset_property. }
  rewrite XR.
  apply idpath.
Qed.

Lemma disp_nat_trans_id_left
  (F' F : functor C' C)
  (a : nat_trans F' F)
  (FF' : disp_functor F' D' D)
  (FF : disp_functor F D' D)
  (b : disp_nat_trans a FF' FF)
  :
   disp_nat_trans_comp (disp_nat_trans_id FF') b =
   transportb (λ f : nat_trans F' F, disp_nat_trans f FF' FF)
              (id_left (a : FunctorsC'C ⟦ _ , _ ⟧))
              b.
Proof.
  apply subtypePath.
  { intro. apply isaprop_disp_nat_trans_axioms. }
  apply funextsec; intro c'.
  apply funextsec; intro xx'.
  apply pathsinv0.
  etrans. apply disp_nat_trans_transportf.
  apply pathsinv0.
  etrans. apply id_left_disp.
  unfold transportb.
  apply maponpaths_2, homset_property.
Qed.

Lemma disp_nat_trans_id_right
  (F' F : functor C' C)
  (a : nat_trans F' F)
  (FF' : disp_functor F' D' D)
  (FF : disp_functor F D' D)
  (b : disp_nat_trans a FF' FF)
  :
   disp_nat_trans_comp b (disp_nat_trans_id FF) =
   transportb (λ f : nat_trans F' F, disp_nat_trans f FF' FF)
              (id_right (a : FunctorsC'C ⟦ _ , _ ⟧))
              b.
Proof.
  apply subtypePath.
  { intro. apply isaprop_disp_nat_trans_axioms. }
  apply funextsec; intro c'.
  apply funextsec; intro xx'.
  apply pathsinv0.
  etrans. apply disp_nat_trans_transportf.
  apply pathsinv0.
  etrans. apply id_right_disp.
  unfold transportb.
  apply maponpaths_2, homset_property.
Qed.

Lemma disp_nat_trans_assoc
  (x y z w : functor C' C)
  (f : nat_trans x y)
  (g : nat_trans y z)
  (h : nat_trans z w)
  (xx : disp_functor x D' D)
  (yy : disp_functor y D' D)
  (zz : disp_functor z D' D)
  (ww : disp_functor w D' D)
  (ff : disp_nat_trans f xx yy)
  (gg : disp_nat_trans g yy zz)
  (hh : disp_nat_trans h zz ww)
  :
   disp_nat_trans_comp ff (disp_nat_trans_comp gg hh) =
   transportb (λ f0 : nat_trans x w, disp_nat_trans f0 xx ww)
     (assoc (f : FunctorsC'C⟦_,_⟧) g h)
     (disp_nat_trans_comp (disp_nat_trans_comp ff gg) hh).
Proof.
  apply subtypePath.
  { intro. apply isaprop_disp_nat_trans_axioms. }
  apply funextsec; intro c'.
  apply funextsec; intro xx'.
  apply pathsinv0.
  etrans. apply disp_nat_trans_transportf.
  apply pathsinv0.
  etrans. apply assoc_disp.
  unfold transportb.
  apply maponpaths_2.
  apply homset_property.
Qed.

Lemma isaset_disp_nat_trans
  (x y : functor C' C)
  (f : nat_trans x y)
  (xx : disp_functor x D' D)
  (yy : disp_functor y D' D)
  :
   isaset (disp_nat_trans f xx yy).
Proof.
  intros. simpl in ×.
  apply (isofhleveltotal2 2).
  × do 2 (apply impred; intro).
    apply homsets_disp.
  × intro d.
    do 6 (apply impred; intro).
    apply hlevelntosn. apply homsets_disp.
Qed.

Definition disp_functor_cat :
  disp_cat (FunctorsC'C).
Proof.
  use tpair.
  - use tpair.
    + use tpair.
      × intro F.
        apply (disp_functor F D' D).
      × simpl. intros F' F FF' FF a.
        apply (disp_nat_trans a FF' FF).
    + use tpair.
      × intros x xx.
        apply disp_nat_trans_id.
      × intros ? ? ? ? ? ? ? ? X X0. apply (disp_nat_trans_comp X X0 ).
  - repeat split.
    + apply disp_nat_trans_id_left.
    + apply disp_nat_trans_id_right.
    + apply disp_nat_trans_assoc.
    + apply isaset_disp_nat_trans.
Defined.

TODO : characterize isos in the displayed functor cat
TODO: integrate has_homsets assumptions below!
Definition pointwise_iso_from_nat_iso {A X : precategory} {hsX : has_homsets X}
  {F G : functor_precategory A X hsX}
  (b : iso F G) (a : A) : iso (pr1 F a) (pr1 G a)
  :=
  functor_iso_pointwise_if_iso _ _ _ _ _ b (pr2 b)_ .

Definition pointwise_inv_is_inv_on {A X : precategory} {hsX : has_homsets X}
  {F G : functor_precategory A X hsX}
  (b : iso F G) (a : A) :

  inv_from_iso (pointwise_iso_from_nat_iso b a) =
                                       pr1 (inv_from_iso b) a.
Proof.
  apply id_right.
Defined.

TODO : write a few lemmas about isos in the disp functor precat, to make the following sane
However: it seems to be better to work on https://github.com/UniMath/UniMath/issues/362 first.

Definition is_pointwise_iso_if_is_disp_functor_cat_iso
  (x y : FunctorsC'C)
  (f : iso x y)
  (xx : disp_functor_cat x)
  (yy : disp_functor_cat y)
  (FF : xx -->[ f ] yy)
  (H : is_iso_disp f FF)
  :
  ∀ x' (xx' : D' x') , is_iso_disp (pointwise_iso_from_nat_iso f _ )
                          (pr1 FF _ xx' ).
Proof.
  intros x' xx'.
  use tpair.
  - set (X:= pr1 H). simpl in X.
    apply (transportb _ (pointwise_inv_is_inv_on f _ ) (X x' xx')).
  - simpl. repeat split.
    + etrans. apply mor_disp_transportf_postwhisker.
      apply pathsinv0.
      apply transportf_comp_lemma.
      assert (XR:= pr1 (pr2 H)).
      assert (XRT := (maponpaths pr1 XR)).
      assert (XRT' := toforallpaths _ _ _ (toforallpaths _ _ _ XRT x')).
      apply pathsinv0.
      etrans. apply XRT'.
      clear XRT' XRT XR.
      assert (XR := disp_nat_trans_transportf).
      specialize (XR _ _ _ _ (! iso_after_iso_inv f)).
      etrans. apply XR.
      apply maponpaths_2, homset_property.
    + etrans. apply mor_disp_transportf_prewhisker.
      apply pathsinv0.
      apply transportf_comp_lemma.
      assert (XR:= inv_mor_after_iso_disp H).
      assert (XRT := (maponpaths pr1 XR)).
      assert (XRT' := toforallpaths _ _ _ (toforallpaths _ _ _ XRT x')).
      apply pathsinv0.
      etrans. apply XRT'.
      clear XRT' XRT XR.
      assert (XR := disp_nat_trans_transportf).
      specialize (XR _ _ _ _ (! iso_inv_after_iso f)).
      etrans. apply XR.
      apply maponpaths_2, homset_property.
Defined.

Lemma is_disp_nat_trans_pointwise_inv
  (x y : FunctorsC'C)
  (f : iso x y)
  (xx : disp_functor_cat x)
  (yy : disp_functor_cat y)
  (FF : xx -->[ f] yy)
  (H : ∏ (x' : C') (xx' : D' x'),
      is_iso_disp (pointwise_iso_from_nat_iso f x') (pr1 FF x' xx'))
  (x' x0 : C')
  (f0 : x' --> x0)
  (xx' : D' x')
  (xx0 : D' x0)
  (ff : xx' -->[ f0] xx0)
  :
   # (yy : disp_functor _ _ _) ff ;; (let RT := pr1 (H x0 xx0) in
               transportf (mor_disp (pr1 yy x0 xx0) (pr1 xx x0 xx0))
                 (id_right (pr1 (inv_from_iso f) x0)) RT) =
   transportb (mor_disp (pr1 yy x' xx') (pr1 xx x0 xx0))
     (nat_trans_ax (inv_from_iso f) x' x0 f0)
     ((let RT := pr1 (H x' xx') in
       transportf (mor_disp (pr1 yy x' xx') (pr1 xx x' xx'))
         (id_right (pr1 (inv_from_iso f) x')) RT) ;;
      # (xx : disp_functor _ _ _) ff).
Proof.
 etrans. apply mor_disp_transportf_prewhisker.
    apply pathsinv0.
    etrans. apply maponpaths. apply mor_disp_transportf_postwhisker.
    etrans. apply transport_f_f.
    apply transportf_comp_lemma.
    set (Hx := H x' xx').
    assert (Hx1 := pr2 (pr2 Hx)).
    set (XR:= iso_disp_precomp (pointwise_iso_from_nat_iso f x' ) (_ ,,Hx)).
    specialize (XR _
       (
        ((# (y : functor _ _ ))%cat f0 · inv_from_iso (pointwise_iso_from_nat_iso f x0))

         )
       ).
    specialize (XR ((xx : disp_functor _ _ _ ) x0 xx0)).
    set (Xweq := make_weq _ XR).
    apply (invmaponpathsweq Xweq).
    unfold Xweq. clear Xweq.
    etrans. apply mor_disp_transportf_prewhisker.
    etrans. apply maponpaths. apply assoc_disp.
    etrans. apply transport_f_f.
    etrans. apply maponpaths. apply maponpaths_2. apply Hx1.
    etrans. apply maponpaths. apply mor_disp_transportf_postwhisker.
    etrans. apply transport_f_f.
    apply pathsinv0.
    etrans. apply assoc_disp.
    assert (XRO := @disp_nat_trans_ax _ _ _ _ _ _ _ _ _ FF).
    specialize (XRO _ _ _ xx' _ ff).
    assert (XR' := ! (transportf_pathsinv0 _ _ _ _ (!XRO))).
    clear XRO.
    clear XR. clear Hx1.
    etrans. apply maponpaths. apply maponpaths_2.
            apply XR'.
    etrans. apply maponpaths. apply mor_disp_transportf_postwhisker.
    etrans. apply transport_f_f.
    apply pathsinv0.
    etrans. apply maponpaths. apply id_left_disp.
    etrans. apply transport_f_f.
    apply pathsinv0.

    etrans. apply maponpaths.
            apply assoc_disp_var.
    etrans. apply transport_f_f.
    etrans. apply maponpaths. apply maponpaths.
            apply (inv_mor_after_iso_disp (H _ _ )).
    etrans. apply maponpaths. apply mor_disp_transportf_prewhisker.
    etrans. apply maponpaths. apply maponpaths.
            apply id_right_disp.
    etrans. apply transport_f_f.
    etrans. apply transport_f_f.
    apply maponpaths_2. apply homset_property.
Qed.

Definition inv_disp_from_pointwise_iso
  (x y : FunctorsC'C)
  (f : iso x y)
  (xx : disp_functor_cat x)
  (yy : disp_functor_cat y)
  (FF : xx -->[ f ] yy)
  (H : ∀ x' (xx' : D' x') , is_iso_disp (pointwise_iso_from_nat_iso f _ )
                          (pr1 FF _ xx' ))
  :
       yy -->[ inv_from_iso f] xx.
Proof.
  use tpair.
  + intros x' xx'.
    simpl in xx. simpl in yy.
    assert (XR : inv_from_iso (pointwise_iso_from_nat_iso f x') =
                                       pr1 (inv_from_iso f) x').
    { apply id_right. }
    set (RT := pr1 (H x' xx')).
    apply (transportf _ XR RT).
  + intros x' x0 f0 xx' xx0 ff.
    apply is_disp_nat_trans_pointwise_inv.
Defined.

Definition is_disp_functor_cat_iso_if_pointwise_iso
  (x y : FunctorsC'C)
  (f : iso x y)
  (xx : disp_functor_cat x)
  (yy : disp_functor_cat y)
  (FF : xx -->[ f ] yy)
  (H : ∀ x' (xx' : D' x') , is_iso_disp (pointwise_iso_from_nat_iso f _ )
                          (pr1 FF _ xx' ))
  : is_iso_disp f FF.
Proof.
  use tpair.
  - apply (inv_disp_from_pointwise_iso _ _ _ _ _ FF H).
  - split.
    + apply subtypePath.
      { intro. apply isaprop_disp_nat_trans_axioms. }
      apply funextsec; intro c'.
      apply funextsec; intro xx'.
      apply pathsinv0.
      etrans. apply disp_nat_trans_transportf.
      cbn.
      apply pathsinv0.
      etrans. apply mor_disp_transportf_postwhisker.
      etrans. apply maponpaths. apply (iso_disp_after_inv_mor (H c' xx')).
      etrans. apply transport_f_f.
      apply maponpaths_2, homset_property.
    + apply subtypePath.
      { intro. apply isaprop_disp_nat_trans_axioms. }
      apply funextsec; intro c'.
      apply funextsec; intro xx'.
      apply pathsinv0.
      etrans. apply disp_nat_trans_transportf.
      cbn.
      apply pathsinv0.
      etrans. apply mor_disp_transportf_prewhisker.
      etrans. apply maponpaths. apply (inv_mor_after_iso_disp (H c' xx')).
      etrans. apply transport_f_f.
      apply maponpaths_2, homset_property.
Defined.

Definition is_disp_functor_cat_iso_iff_pointwise_iso
  (x y : FunctorsC'C)
  (f : iso x y)
  (xx : disp_functor_cat x)
  (yy : disp_functor_cat y)
  (FF : xx -->[ f ] yy)
  :
  (∏ x' (xx' : D' x') , is_iso_disp (pointwise_iso_from_nat_iso f _ )
                          (pr1 FF _ xx' ))
    ↔
    is_iso_disp f FF.
Proof.
  split.
  - apply is_disp_functor_cat_iso_if_pointwise_iso.
  - apply is_pointwise_iso_if_is_disp_functor_cat_iso.
Defined.

End Functor.

Fiber categories

A displayed category gives a fiber category over each object of the base. These are most interesting in the case where the displayed category is an isofibration.
Section Fiber.

Context {C : category}
        (D : disp_cat C)
        (c : C).

Definition fiber_category_data : precategory_data.
Proof.
  use tpair.
  - use tpair.
    + apply (ob_disp D c).
    + intros xx xx'. apply (mor_disp xx xx' (identity c)).
  - use tpair.
    + intros. apply id_disp.
    + cbn. intros. apply (transportf _ (id_right _ ) (comp_disp X X0)).
Defined.

Lemma fiber_is_precategory : is_precategory fiber_category_data.
Proof.
  apply is_precategory_one_assoc_to_two.
  repeat split; intros; cbn.
  - etrans. apply maponpaths. apply id_left_disp.
    etrans. apply transport_f_f. apply transportf_comp_lemma_hset.
    apply (homset_property). apply idpath.
  - etrans. apply maponpaths. apply id_right_disp.
    etrans. apply transport_f_f. apply transportf_comp_lemma_hset.
    apply (homset_property). apply idpath.
  - etrans. apply maponpaths. apply mor_disp_transportf_prewhisker.
    etrans. apply transport_f_f.
    etrans. apply maponpaths. apply assoc_disp.
    etrans. apply transport_f_f.
    apply pathsinv0.
    etrans. apply maponpaths. apply mor_disp_transportf_postwhisker.
    etrans. apply transport_f_f.
    apply maponpaths_2. apply homset_property.
Qed.

Definition fiber_precategory : precategory := ( _ ,, fiber_is_precategory).

Lemma has_homsets_fiber_category : has_homsets fiber_precategory.
Proof.
  intros x y. apply homsets_disp.
Qed.

Definition fiber_category : category
  := ( fiber_precategory ,, has_homsets_fiber_category).

Definition iso_disp_from_iso_fiber (a b : fiber_category) :
  iso a b → iso_disp (identity_iso c) a b.
Proof.
 intro i.
 use tpair.
 + apply (pr1 i).
 + cbn.
   use tpair.
   × apply (inv_from_iso i).
   × abstract ( split;
       [ assert (XR := iso_after_iso_inv i);
        cbn in *;
        assert (XR' := transportf_pathsinv0_var XR);
        etrans; [ apply (!XR') |];
        unfold transportb;
        apply maponpaths_2; apply homset_property
       |assert (XR := iso_inv_after_iso i);
        cbn in *;
        assert (XR' := transportf_pathsinv0_var XR);
        etrans; [ apply (!XR') | ];
        unfold transportb;
        apply maponpaths_2; apply homset_property ] ).
Defined.

Definition iso_fiber_from_iso_disp (a b : fiber_category) :
  iso a b <- iso_disp (identity_iso c) a b.
Proof.
  intro i.
  use tpair.
  + apply (pr1 i).
  + cbn in ×.
    apply (@is_iso_from_is_z_iso fiber_category).
    use tpair.
    apply (inv_mor_disp_from_iso i).
    abstract (split; cbn;
              [
                assert (XR := inv_mor_after_iso_disp i);
                etrans; [ apply maponpaths , XR |];
                etrans; [ apply transport_f_f |];
                apply transportf_comp_lemma_hset;
                  try apply homset_property; apply idpath
              | assert (XR := iso_disp_after_inv_mor i);
                etrans; [ apply maponpaths , XR |] ;
                etrans; [ apply transport_f_f |];
                apply transportf_comp_lemma_hset;
                try apply homset_property; apply idpath
              ]).
Defined.

Lemma iso_disp_iso_fiber (a b : fiber_category) :
  iso a b ≃ iso_disp (identity_iso c) a b.
Proof.
  ∃ (iso_disp_from_iso_fiber a b).
  use (isweq_iso _ (iso_fiber_from_iso_disp _ _ )).
  - intro. apply eq_iso. apply idpath.
  - intro. apply eq_iso_disp. apply idpath.
Defined.

Univalence

Variable H : is_univalent_disp D.

Let idto1 (a b : fiber_category) : a = b ≃ iso_disp (identity_iso c) a b
  :=
  make_weq (@idtoiso_fiber_disp _ _ _ a b) (H _ _ (idpath _ ) a b).

Let idto2 (a b : fiber_category) : a = b → iso_disp (identity_iso c) a b
  :=
  funcomp (λ p : a = b, idtoiso p) (iso_disp_iso_fiber a b).

Lemma eq_idto1_idto2 (a b : fiber_category)
  : ∏ p : a = b, idto1 _ _ p = idto2 _ _ p.
Proof.
  intro p. induction p.
  apply eq_iso_disp.
  apply idpath.
Qed.

Lemma is_univalent_fiber_cat
  (a b : fiber_category)
  :
  isweq (λ p : a = b, idtoiso p).
Proof.
  use (twooutof3a _ (iso_disp_iso_fiber a b)).
  - use (isweqhomot (idto1 a b)).
    + intro p.
      apply eq_idto1_idto2.
    + apply weqproperty.
  - apply weqproperty.
Defined.

Lemma is_univalent_fiber : is_univalent fiber_category.
Proof.
  split.
  - apply is_univalent_fiber_cat.
  - apply has_homsets_fiber_category.
Defined.

End Fiber.

Arguments fiber_precategory {_} _ _ .
Arguments fiber_category {_} _ _ .

Notation "D [{ x }]" := (fiber_category D x)(at level 3,format "D [{ x }]").

Lemma is_univalent_disp_from_is_univalent_fiber {C : category} (D : disp_cat C)
  : (∏ (c : C), is_univalent D[{c}]) → is_univalent_disp D.
Proof.
  intro H.
  apply is_univalent_disp_from_fibers.
  intros c xx xx'.
  specialize (H c).
  set (w := make_weq _ (pr1 H xx xx')).
  set (w' := weqcomp w (iso_disp_iso_fiber D _ xx xx')).
  apply (weqhomot _ w').
  intro e. induction e.
  apply eq_iso_disp. apply idpath.
Defined.

Definition is_univalent_disp_iff_fibers_are_univalent {C : category} (D : disp_cat C)
  : is_univalent_disp D ↔ (∏ (c : C), is_univalent D[{c}]).
Proof.
  split; intro H.
  - intro. apply is_univalent_fiber. apply H.
  - apply is_univalent_disp_from_is_univalent_fiber.
    apply H.
Defined.

Fiber functors

Functors between displayed categories induce functors between their fibers.
Section Fiber_Functors.

Section fix_context.

Context {C C' : category} {D} {D'}
        {F : functor C C'} (FF : disp_functor F D D')
        (x : C).

Definition fiber_functor_data : functor_data D[{x}] D'[{F x}].
Proof.
  use tpair.
  - apply (λ xx', FF xx').
  - intros xx' xx ff.
    apply (transportf _ (functor_id _ _ ) (# FF ff)).
Defined.

Lemma is_functor_fiber_functor : is_functor fiber_functor_data.
Proof.
  split; unfold functor_idax, functor_compax; cbn.
  - intros.
    apply transportf_pathsinv0.
    apply pathsinv0. apply disp_functor_id.
  - intros.
    etrans. apply maponpaths. apply disp_functor_transportf.
    etrans. apply transport_f_f.
    etrans. apply maponpaths. apply disp_functor_comp.
    etrans. apply transport_f_f.
    apply pathsinv0.
    etrans. apply maponpaths. apply mor_disp_transportf_prewhisker.
    etrans. apply transport_f_f.
    etrans. apply maponpaths. apply mor_disp_transportf_postwhisker.
    etrans. apply transport_f_f.
    apply maponpaths_2, homset_property.
Qed.

Definition fiber_functor : functor D[{x}] D'[{F x}]
  := ( _ ,, is_functor_fiber_functor).

End fix_context.


Definition is_iso_fiber_from_is_iso_disp
  {C : category} {D : disp_cat C}
  {c : C} {d d' : D c} (ff : d -->[identity c] d')
  (Hff : is_iso_disp (identity_iso c) ff)
: @is_iso (fiber_category D c) _ _ ff.
Proof.
  apply is_iso_from_is_z_iso.
  ∃ (pr1 Hff).
  use tpair; cbn.
  + set (H := pr2 (pr2 Hff)).
    etrans. apply maponpaths, H.
    etrans. apply transport_f_b.
    use (@maponpaths_2 _ _ _ _ _ (paths_refl _)).
    apply homset_property.
  + set (H := pr1 (pr2 Hff)).
    etrans. apply maponpaths, H.
    etrans. apply transport_f_b.
    use (@maponpaths_2 _ _ _ _ _ (paths_refl _)).
    apply homset_property.
Qed.

Definition fiber_nat_trans {C C' : category}
  {F : functor C C'}
  {D D'} {FF FF' : disp_functor F D D'}
  (α : disp_nat_trans (nat_trans_id F) FF FF')
  (c : C)
: nat_trans (fiber_functor FF c) (fiber_functor FF' c).
Proof.
  use tpair; simpl.
  - intro d. exact (α c d).
  - unfold is_nat_trans; intros d d' ff; simpl.
    set (αff := pr2 α _ _ _ _ _ ff); simpl in αff.
    cbn.
    etrans. apply maponpaths, mor_disp_transportf_postwhisker.
    etrans. apply transport_f_f.
    etrans. apply maponpaths, αff.
    etrans. apply transport_f_b.
    apply @pathsinv0.
    etrans. apply maponpaths, mor_disp_transportf_prewhisker.
    etrans. apply transport_f_f.
    apply maponpaths_2, homset_property.
Defined.

Lemma fiber_functor_ff
    {C C' : category} {D} {D'}
    {F : functor C C'} (FF : disp_functor F D D')
    (H : disp_functor_ff FF)
    (c : C)
: fully_faithful (fiber_functor FF c).
Proof.
  intros xx yy; cbn.
  set (XR := H _ _ xx yy (identity _ )).
  apply twooutof3c.
  - apply XR.
  - apply isweqtransportf.
Defined.

End Fiber_Functors.