Library UniMath.CategoryTheory.Presheaves.DisplayedCatOfDependentPresheaf

The displayed category of dependent presheaves and natural transformations

In this file, we show that dependent presheaves and natural transformations form a displayed category over the category of presheaves. We also establish various facts about this displayed category, and in particular, we show that it is univalent.

The relevance of this displayed category comes from the presheaf model of dependent type theory, because it gives us the category of types in this model. We also construct a cleaving for this displayed category, and we construct a comprehension functor.

Contents 1. The displayed category of dependent presheaves 2. Isomorphisms in this displaed category 3. This displayed category is univalent 4. The cleaving 5. The comprehension functor 6. The comprehension functor is Cartesian 7. The comprehension functor is fully faithful 8. Useful calculational lemmas

4. The cleaving

  Definition cleaving_disp_cat_dep_psh
    : cleaving disp_cat_dep_psh.
  Proof.
    intros Γ₁ Γ₂ s A.
    simple refine (_ ,, _).
    - exact (dep_psh_subst s A).
    - simple refine (_ ,, _).
      + exact (dep_psh_subst_nat_trans s A).
      + intros Γ' s' B τ.
        use make_iscontr.
        * simple refine (_ ,, _).
          ** exact (dep_psh_factor_nat_trans τ).
          ** abstract
              (use dep_psh_nat_trans_eq ;
               intros x xx a ; cbn ;
               apply idpath).
        * abstract
            (intros τ' ;
             use subtypePath ; [ intro ; apply homsets_disp | ] ;
             use dep_psh_nat_trans_eq ;
             intros x xx a ; cbn ;
             exact (eqtohomot (maponpaths (λ z , pr1 z (x ,, xx)) (pr2 τ')) a)).
  Defined.

5. The comprehension functor

  Definition dep_psh_comprehension_data
    : disp_functor_data
        (functor_identity _)
        disp_cat_dep_psh
        (disp_codomain (PreShv C)).
  Proof.
    simple refine (_ ,, _).
    - exact (λ Γ A , total_psh A ,, total_psh_pr A).
    - refine (λ Γ₁ Γ₂ A B s τ , total_psh_nat_trans s τ ,, _).
      abstract
        (use nat_trans_eq ; [ apply homset_property | ] ;
         intro x ; cbn ;
         apply idpath).
  Defined.

  Proposition dep_psh_comprehension_laws
    : disp_functor_axioms dep_psh_comprehension_data.
  Proof.
    split.
    - intros Γ A.
      use subtypePath.
      {
        intro.
        apply homset_property.
      }
      use nat_trans_eq.
      {
        apply homset_property.
      }
      intro x ; cbn.
      apply idpath.
    - intros Γ₁ Γ₂ Γ₃ A₁ A₂ A₃ s₁ s₂ τ₁ τ₂.
      use subtypePath.
      {
        intro.
        apply homset_property.
      }
      use nat_trans_eq.
      {
        apply homset_property.
      }
      intro x ; cbn.
      apply idpath.
  Qed.

  Definition dep_psh_comprehension
    : disp_functor
        (functor_identity _)
        disp_cat_dep_psh
        (disp_codomain (PreShv C)).
  Proof.
    simple refine (_ ,, _).
    - exact dep_psh_comprehension_data.
    - exact dep_psh_comprehension_laws.
  Defined.

6. The comprehension functor is Cartesian

  Section ComprehensionCartesian.
    Context {Γ₁ Γ₂ Γ₃ : C ^op ⟶ HSET}
            {s₁ : Γ₁ ⟹ Γ₂}
            {s₂ : Γ₂ ⟹ Γ₃}
            (A : dep_psh Γ₃)
            (τ : Γ₁ ⟹ total_psh A)
            (p : nat_trans_comp _ _ _ τ (total_psh_pr A) = nat_trans_comp _ _ _ s₁ s₂).

    Definition dep_psh_comprehension_pb_mor_data
      : nat_trans_data Γ₁ (total_psh (dep_psh_subst s₂ A)).
    Proof.
      intros x xx.
      refine (s₁ x xx ,, _).
      refine (#d A (identity _) _ (pr2 (τ x xx ))).
      abstract
        (refine (_ @ eqtohomot (nat_trans_eq_pointwise p x) xx) ;
         apply (eqtohomot (functor_id Γ₃ _))).
    Defined.

    Proposition dep_psh_comprehension_pb_mor_laws
      : is_nat_trans _ _ dep_psh_comprehension_pb_mor_data.
    Proof.
      intros x y f.
      use funextsec.
      intros xx.
      use dep_psh_total_space_path.
      - exact (eqtohomot (nat_trans_ax s₁ _ _ f) xx).
      - cbn.
        rewrite !dep_psh_mor_comp'.
        etrans.
        {
          apply maponpaths.
          exact (dep_psh_total_space_pr2_path' _ (eqtohomot (nat_trans_ax τ _ _ f) xx)).
        }
        cbn.
        rewrite !dep_psh_mor_comp'.
        apply dep_psh_mor_path_eq.
        rewrite !id_left, id_right.
        apply idpath.
    Qed.

    Definition dep_psh_comprehension_pb_mor
      : Γ₁ ⟹ total_psh (dep_psh_subst s₂ A).
    Proof.
      use make_nat_trans.
      - exact dep_psh_comprehension_pb_mor_data.
      - exact dep_psh_comprehension_pb_mor_laws.
    Defined.

    Proposition dep_psh_comprehension_pb_mor_eq
      : nat_trans_comp
          _ _ _
          dep_psh_comprehension_pb_mor
          (total_psh_nat_trans s₂ (dep_psh_subst_nat_trans s₂ A))
        =
        τ.
    Proof.
      use nat_trans_eq ; [ apply homset_property | ].
      intro x.
      use funextsec.
      intro xx.
      use dep_psh_total_space_path ; cbn.
      - exact (!(eqtohomot (nat_trans_eq_pointwise p x) xx)).
      - rewrite dep_psh_mor_comp'.
        apply dep_psh_mor_id'.
        rewrite id_left.
        apply idpath.
    Qed.

    Proposition dep_psh_comprehension_pb_mor_unique
                (τ' : Γ₁ ⟹ total_psh_data (dep_psh_subst s₂ A))
                (q : nat_trans_comp
                       _ _ _
                       τ'
                       (total_psh_nat_trans s₂ (dep_psh_subst_nat_trans s₂ A))
                     =
                     τ)
                (r : nat_trans_comp
                       _ _ _
                       τ'
                       (total_psh_pr (dep_psh_subst s₂ A))
                     =
                     s₁)
      : τ' = dep_psh_comprehension_pb_mor.
    Proof.
      use nat_trans_eq ; [ apply homset_property | ].
      intro x.
      use funextsec.
      intro xx.
      use dep_psh_total_space_path.
      - exact (eqtohomot (nat_trans_eq_pointwise r x) xx).
      - pose (dep_psh_total_space_pr2_path' _ (eqtohomot (nat_trans_eq_pointwise q x) xx))
          as r'.
        cbn ; cbn in r'.
        etrans.
        {
          apply maponpaths.
          exact r'.
        }
        rewrite dep_psh_mor_comp'.
        apply dep_psh_mor_path_eq.
        apply id_left.
    Qed.
  End ComprehensionCartesian.

  Proposition is_cartesian_dep_psh_comprehension
    : is_cartesian_disp_functor dep_psh_comprehension.
  Proof.
    use is_cartesian_disp_functor_chosen_lifts.
    {
      exact cleaving_disp_cat_dep_psh.
    }
    intros Γ₂ Γ₃ s₂ A.
    use isPullback_cartesian_in_cod_disp.
    intros Γ₁ τ s₁ p.
    use make_iscontr.
    - simple refine (_ ,, _).
      + exact (dep_psh_comprehension_pb_mor A τ p).
      + split.
        * exact (dep_psh_comprehension_pb_mor_eq A τ p).
        * abstract
            (use nat_trans_eq ; [ apply homset_property | ] ;
             intro x ;
             use funextsec ;
             intro xx ;
             cbn ;
             apply idpath).
    - abstract
        (intro τ' ;
         use subtypePath ; [ intro ; apply isapropdirprod ; apply homset_property | ] ;
         exact (dep_psh_comprehension_pb_mor_unique A τ p (pr1 τ') (pr12 τ') (pr22 τ'))).
  Defined.

7. The comprehension functor is fully faithful

  Definition dep_psh_nat_trans_from_total
             {Γ₁ Γ₂ : C ^op ⟶ HSET}
             {A : dep_psh Γ₁}
             {B : dep_psh Γ₂}
             {s : Γ₁ ⟹ Γ₂}
             (τ : total_psh A ⟹ total_psh B)
             (p : nat_trans_comp _ _ _ τ (total_psh_pr B)
                  =
                  nat_trans_comp _ _ _ (total_psh_pr A) s)
    : dep_psh_nat_trans A B s.
  Proof.
    use make_dep_psh_nat_trans.
    - refine (λ x xx a , #d B (identity _) _ (pr2 (τ x (xx ,, a )))).
      abstract
        (refine (eqtohomot (functor_id Γ₂ _) _ @ _) ; cbn ;
         exact (eqtohomot (nat_trans_eq_pointwise p x) (xx ,, a))).
    - abstract
        (intros x y xx yy f q r a ; cbn ;
         pose proof (dep_psh_total_space_pr2_path'
                       _
                       (eqtohomot (nat_trans_ax τ _ _ f) (xx ,, a))) as r' ;
         cbn in r' ;
         induction q ;
         simple refine (dep_psh_mor_path_eq _ _ _ (idpath _) _
                        @ maponpaths (#d B (identity _) _) r'
                        @ _) ;
         [ cbn ;
           refine (_ @ r) ;
           refine (eqtohomot (functor_id Γ₂ _) _ @ _) ;
           refine (maponpaths pr1 (eqtohomot (nat_trans_ax τ _ _ f) (xx ,, a)) @ _) ;
           cbn ;
           apply maponpaths ;
           exact (eqtohomot (nat_trans_eq_pointwise p x) (xx ,, a))
         | rewrite !dep_psh_mor_comp' ;
           apply dep_psh_mor_path_eq ;
           rewrite !id_left, id_right ;
           apply idpath ]).
  Defined.

  Proposition disp_functor_ff_dep_psh_comprehension
    : disp_functor_ff dep_psh_comprehension.
  Proof.
    intros Γ₁ Γ₂ A B s.
    use isweq_iso.
    - intros τ.
      exact (dep_psh_nat_trans_from_total (pr1 τ) (pr2 τ)).
    - abstract
        (intro τ ;
         use dep_psh_nat_trans_eq ;
         intros x xx a ; cbn ;
         apply dep_psh_mor_id).
    - abstract
        (intros [ τ p ] ; cbn in p ;
         use subtypePath ; [ intro ; apply homset_property | ] ;
         use nat_trans_eq ; [ apply homset_property | ] ;
         intros x ;
         use funextsec ;
         intros xx ;
         pose (eqtohomot (nat_trans_eq_pointwise p x) xx) as q ;
         use dep_psh_total_space_path ; [ exact (!q) | ] ;
         cbn ;
         rewrite dep_psh_mor_comp' ;
         apply dep_psh_mor_id' ;
         exact (!(id_left _))).
  Defined.

8. Useful calculational lemmas

  Proposition dep_psh_fiber_comp
              {Γ : C ^op ⟶ HSET}
              {A₁ A₂ A₃ : dep_psh Γ}
              (τ ₁ : (disp_cat_dep_psh [{ Γ }]) ⟦ A₁ , A₂ ⟧)
              (τ ₂ : (disp_cat_dep_psh [{ Γ }]) ⟦ A₂ , A₃ ⟧)
              {x : C}
              {xx : (Γ x : hSet)}
              (a : A₁ x xx)
              (θ₁ := τ ₁ : dep_psh_nat_trans A₁ A₂ (nat_trans_id _))
              (θ₂ := τ ₂ : dep_psh_nat_trans A₂ A₃ (nat_trans_id _))
    : (τ ₁ · τ ₂ : dep_psh_nat_trans A₁ A₃ (nat_trans_id _)) x xx a
      =
      θ₂ x xx (θ₁ x xx a).
  Proof.
    cbn.
    refine (transportf_dep_psh_nat_trans
              (id_right (C := PreShv C) _)
              (dep_psh_comp_nat_trans τ₁ τ₂)
              x xx a
            @ _).
    apply (transportf_set (A₃ x)).
    apply setproperty.
  Qed.

  Proposition dep_psh_fiber_functor_from_cleaving
              {Γ₁ Γ₂ : C ^op ⟶ HSET}
              (s : Γ₁ ⟹ Γ₂)
              {A₁ A₂ : dep_psh Γ₂}
              (τ : dep_psh_nat_trans A₁ A₂ (nat_trans_id _))
              {x : C}
              {xx : (Γ₁ x : hSet)}
              (a : A₁ x (s x xx))
              (HD := cleaving_disp_cat_dep_psh)
    : (#(fiber_functor_from_cleaving _ HD s ) τ : dep_psh_nat_trans _ _ _) x xx a
      =
      τ x _ a.
  Proof.
    cbn.
    refine (transportf_dep_psh_nat_trans
              (id_right (C := PreShv C) _ @ !(id_left _))
              _
              _ _ _
            @ _).
    apply (transportf_set (A₂ x)).
    apply setproperty.
  Qed.
End DispCatDepPsh.