Library UniMath.Bicategories.ComprehensionCat.PresheafModel

The presheaf model of type theory

One of the standard models of type theory, is the presheaf model. Specifically, if we have a category `C`, then we have a comprehension category as follows.

Contexts: presheaves over `C`
Morphisms between contexts: natural transformations
Types in context `Γ`: dependent presheaves over `Γ` (i.e., presheaves over `∫ Γ` where `∫ Γ` is the category of elements of `Γ`)
Morphisms between types: natural transformation
Terms are the same as sections

We construct this model as a full comprehension category. In addition, we show that this model supports various type formers, like extensional identity types, a unit type, binary products, ∑-types, natural numbers, and ∏-types. We also show that it supports a subobject classifier type. We use this to deduce that the category of presheaves is an elementary topos.

We also show that functors and natural transformations lift to the presheaf model.

Content 1. The full comprehension category 2. Type formers in the presheaf model 3. The category of presheaves is an elementary topos 4. Functors on the presheaf model 5. Natural transformations on the presheaf model

2. Type formers in the presheaf model

  Definition is_democratic_psh_full_comp_cat
    : is_democratic psh_full_comp_cat.
  Proof.
    intro Γ.
    exact (psh_to_dep_psh Γ ,, psh_to_dep_psh_z_iso Γ).
  Defined.

  Definition dependent_sums_psh_full_comp_cat
    : comp_cat_dependent_sum psh_full_comp_cat.
  Proof.
    use make_comp_cat_dependent_sum_from_chosen.
    use make_comp_cat_dependent_sum_chosen.
    - intros Γ A.
      exact (dependent_sum_dep_psh A).
    - intros Γ₁ Γ₂ A s B.
      use make_is_z_isomorphism.
      + exact (dep_psh_sigma_subst s A B).
      + abstract
          (split ;
           use dep_psh_nat_trans_eq ;
           intros x xx ab ;
           refine (dep_psh_fiber_comp _ _ _ _ @ _) ;
           exact (dep_psh_sigma_beck_chevalley s A B ab _)).
  Defined.

  Definition strong_dependent_sums_psh_full_comp_cat
    : strong_dependent_sums psh_full_comp_cat.
  Proof.
    refine (dependent_sums_psh_full_comp_cat ,, _).
    intros Γ A B.
    use make_is_z_isomorphism.
    - exact (dep_psh_sigma_total_inv A B).
    - abstract
        (split ;
         (use nat_trans_eq ; [ apply homset_property | ]) ;
         intro x ;
         apply idpath).
  Defined.

  Definition psh_dfl_full_comp_cat
    : dfl_full_comp_cat.
  Proof.
    use make_dfl_full_comp_cat.
    - exact psh_full_comp_cat.
    - exact is_democratic_psh_full_comp_cat.
    - exact (dep_psh_fiberwise_terminal C).
    - exact dep_psh_unit_z_iso.
    - exact (dep_psh_fiberwise_binproducts C).
    - exact (dep_psh_fiberwise_equalizers C).
    - exact strong_dependent_sums_psh_full_comp_cat.
  Defined.

  Definition dependent_prod_psh_comp_cat
    : comp_cat_dependent_prod psh_full_comp_cat.
  Proof.
    use make_comp_cat_dependent_prod_from_chosen.
    use make_comp_cat_dependent_prod_chosen.
    - intros Γ A.
      exact (dependent_product_dep_psh A).
    - intros Γ₁ Γ₂ A s B.
      use make_is_z_isomorphism.
      + exact (dep_psh_pi_subst s A B).
      + exact (dep_psh_pi_subst_inv_laws s A B _).
  Defined.

  Definition subobject_classifier_psh_comp_cat
    : fiberwise_cat_property
        subobject_classifier_local_property
        psh_dfl_full_comp_cat.
  Proof.
    use make_fiberwise_cat_property.
    - exact dep_psh_subobject_classifier.
    - intros Γ₁ Γ₂ s.
      exact (dep_psh_subobject_classifier_preservation s).
  Defined.

  Definition pnno_psh_comp_cat
    : fiberwise_cat_property
        parameterized_NNO_local_property
        psh_dfl_full_comp_cat.
  Proof.
    use make_fiberwise_cat_property.
    - intro Γ.
      refine (_ ,, _ ,, _ ,, _).
      exact (is_parameterized_NNO_prod_independent
               (C := univalent_fiber_category
                       (univalent_disp_cat_dep_psh C)
                       Γ)
               _
               (dep_psh_fiberwise_nno Γ)).
    - intros Γ₁ Γ₂ s.
      use preserves_parameterized_NNO_prod_independent.
      exact (dep_psh_fiberwise_nno_stable s).
  Defined.

3. The category of presheaves is an elementary topos

4. Functors on the presheaf model

5. Natural transformations on the presheaf model

Section PShCompCatNatTrans.
  Context {C₁ C₂ : category}
          {F G : C₁ ⟶ C₂}
          (τ : F ⟹ G).

  Definition precomposition_psh_dfl_full_nat_trans_with_terminal_cleaving
    : nat_trans_with_terminal_cleaving
        (precomposition_psh_dfl_full_comp_cat_functor G)
        (precomposition_psh_dfl_full_comp_cat_functor F).
  Proof.
    use make_nat_trans_with_terminal_cleaving.
    use make_nat_trans_with_terminal_disp_cat.
    - exact (precomp_psh_nat_trans τ).
    - exact (precomp_psh_disp_nat_trans τ).
  Defined.

  Definition precomposition_psh_dfl_full_comp_cat_nat_trans
    : dfl_full_comp_cat_nat_trans
        (precomposition_psh_dfl_full_comp_cat_functor G)
        (precomposition_psh_dfl_full_comp_cat_functor F).
  Proof.
    use make_dfl_full_comp_cat_nat_trans.
    use make_full_comp_cat_nat_trans.
    use make_comp_cat_nat_trans.
    - exact precomposition_psh_dfl_full_nat_trans_with_terminal_cleaving.
    - abstract
        (intros Γ A ;
         use nat_trans_eq ; [ apply homset_property | ] ;
         intro x ; cbn ;
         apply idpath).
  Defined.
End PShCompCatNatTrans.