Library UniMath.Bicategories.ComprehensionCat.InternalLanguageTopos.ToposNatUniv

The internal language of elementary toposes with a NNO and a universe

We have established biequivalences between bicategories of univalent categories with finite limits and various kinds of structure, and univalent DFL full comprehension categories with the corresponding structure. We used these biequivalence to give an internal language theorem for univalent elementary toposes with a natural numbers object. In this file, we give an internal language theorem for elementary toposes with a NNO and a universe. The universe is required to satisfy the following closure conditions.

The natural numbers object must be contained in the universe.
The subobject classifier must be contained in the universe.
The universe must contain every proposition. This corresponds to propositional resizing.
The universe must be closed under ∑-types and ∏-types.

This notion of universe is based on "Universes in toposes" by Streicher, and these closure conditions have various implications. For instance, since the universe contains every proposition, we can directly conclude that the unit type and tne empty type are in the universe. In addition, since the universe contains the subobject classifier, one can show that the universe also is closed under sums and quotients.

References

"Universes in toposes" by Streicher

Contents 1. The bicategory of elementary toposes with a NNO and universe 2. Accessors for elementary toposes with a NNO and universe 3. The bicategory of elementary topos comprehension categories with a NNO and universe 4. Accessors for elementary toposes comprehension categories with a NNO and universe 5. The biequivalence 6. Type formers in a topos with a universe 6.1. Parameterized NNO 6.2. Subobject classifier 6.3. Propositional resizing 6.4. ∑-types 6.5. ∏-types 6.6. Universes for toposes 7. Accessors for topos universes 8. The biequivalence for topos universes

1. The bicategory of elementary toposes with a NNO and universe

Definition disp_bicat_of_univ_topos_with_NNO_univ
  : disp_bicat bicat_of_univ_cat_with_finlim
  := disp_dirprod_bicat
       disp_bicat_of_univ_topos_with_NNO
       disp_bicat_finlim_universe.

Proposition disp_2cells_isaprop_disp_bicat_of_univ_topos_with_NNO_univ
  : disp_2cells_isaprop disp_bicat_of_univ_topos_with_NNO_univ.
Show proof.

  use disp_2cells_isaprop_prod.
  - exact disp_2cells_isaprop_disp_bicat_of_univ_topos_with_NNO.
  - exact disp_2cells_isaprop_disp_bicat_finlim_universe.

Proposition disp_locally_groupoid_disp_bicat_of_univ_topos_with_NNO_univ
: disp_locally_groupoid disp_bicat_of_univ_topos_with_NNO_univ.
Show proof.

  use disp_locally_groupoid_prod.
  - exact disp_locally_groupoid_disp_bicat_of_univ_topos_with_NNO.
  - exact disp_locally_groupoid_disp_bicat_finlim_universe.

Proposition disp_univalent_2_disp_bicat_of_univ_topos_with_NNO_univ
: disp_univalent_2 disp_bicat_of_univ_topos_with_NNO_univ.
Show proof.

  use is_univalent_2_dirprod_bicat.
  - exact is_univalent_2_1_bicat_of_univ_cat_with_finlim.
  - exact disp_univalent_2_disp_bicat_of_univ_topos_with_NNO.
  - exact disp_univalent_2_disp_bicat_finlim_universe.

Proposition disp_univalent_2_0_disp_bicat_of_univ_topos_with_NNO_univ
: disp_univalent_2_0 disp_bicat_of_univ_topos_with_NNO_univ.
Show proof.

apply disp_univalent_2_disp_bicat_of_univ_topos_with_NNO_univ.

Proposition disp_univalent_2_1_disp_bicat_of_univ_topos_with_NNO_univ
: disp_univalent_2_1 disp_bicat_of_univ_topos_with_NNO_univ.
Show proof.

apply disp_univalent_2_disp_bicat_of_univ_topos_with_NNO_univ.

Definition bicat_of_univ_topos_with_NNO_univ
  : bicat
  := total_bicat disp_bicat_of_univ_topos_with_NNO_univ.

Proposition is_univalent_2_bicat_of_univ_topos_with_NNO_univ
  : is_univalent_2 bicat_of_univ_topos_with_NNO_univ.
Show proof.

  use total_is_univalent_2.
  - exact disp_univalent_2_disp_bicat_of_univ_topos_with_NNO_univ.
  - exact is_univalent_2_bicat_of_univ_cat_with_finlim.

Proposition is_univalent_2_0_bicat_of_univ_topos_with_NNO_univ
: is_univalent_2_0 bicat_of_univ_topos_with_NNO_univ.
Show proof.

apply is_univalent_2_bicat_of_univ_topos_with_NNO_univ.

Proposition is_univalent_2_1_bicat_of_univ_topos_with_NNO_univ
: is_univalent_2_1 bicat_of_univ_topos_with_NNO_univ.
Show proof.

apply is_univalent_2_bicat_of_univ_topos_with_NNO_univ.

2. Accessors for elementary toposes with a NNO and universe

Definition univ_topos_with_NNO_univ
  : UU
  := bicat_of_univ_topos_with_NNO_univ.

Coercion univ_topos_with_NNO_to_univ_pretopos
         (E : univ_topos_with_NNO_univ)
  : univ_pretopos.
Show proof.

  use make_univ_pretopos.
  - exact (pr1 E).
  - exact (pr111 (pr111 (pr112 E))).
  - exact (pr1 (pr211 (pr111 (pr112 E)))).
  - exact (pr2 (pr211 (pr111 (pr112 E)))).
  - exact (pr21 (pr111 (pr112 E))).
  - exact (pr112 (pr111 (pr112 E))).
  - exact (pr212 (pr111 (pr112 E))).
  - exact (pr22 (pr111 (pr112 E))).

  use make_univ_cat_with_finlim_universe.
  - exact E.
  - exact (pr122 E).
  - exact (pr222 E).

Definition make_univ_topos_with_NNO
           (E : univ_pi_pretopos)
           (Ω : subobject_classifier (terminal_univ_cat_with_finlim E))
           (N : parameterized_NNO
                  (terminal_univ_cat_with_finlim E)
                  (binproducts_univ_cat_with_finlim E))
           (u : E)
           (el : cat_stable_el_map (pretopos_to_finlim E ,, u))
           (H : is_coherent_cat_stable_el_map el)
  : univ_topos_with_NNO_univ.
Show proof.

  simple refine (_ ,, (((((((_ ,, (_ ,, _)) ,, _)
                   ,, ((_ ,, _) ,, _)) ,, _) ,, _) ,, tt ) ,, (_ ,, tt ))
                   ,, (_ ,, _ ,, _)) ; cbn.
  - exact (pretopos_to_finlim E).
  - exact (strict_initial_univ_pretopos E).
  - exact (bincoproducts_univ_pretopos E).
  - exact (stable_bincoproducts_univ_pretopos E).
  - exact (disjoint_bincoproducts_univ_pretopos E).
  - exact (is_regular_category_coeqs_of_kernel_pair
             (is_regular_category_univ_pretopos E)).
  - exact (is_regular_category_regular_epi_pb_stable
             (is_regular_category_univ_pretopos E)).
  - exact (all_internal_eqrel_effective_univ_pretopos E).
  - exact Ω.
  - exact N.
  - exact (univ_pi_pretopos_lccc E).
  - exact u.
  - exact el.
  - exact H.

Definition functor_topos_with_NNO_univ
           (E₁ E₂ : univ_topos_with_NNO_univ)
  : UU
  := E₁ --> E₂.

Coercion functor_topos_with_NNO_univ_to_functor_pretopos
         {E₁ E₂ : univ_topos_with_NNO_univ}
         (F : functor_topos_with_NNO_univ E₁ E₂)
  : functor_pretopos E₁ E₂.
Show proof.

  use make_functor_pretopos.
  - exact (pr1 F).
  - exact (pr11 (pr112 (pr112 F))).
  - exact (pr21 (pr112 (pr112 F))).
  - exact (pr12 (pr112 (pr112 F))).

  use make_functor_finlim_universe.
  - exact F.
  - exact (pr122 F).
  - exact (pr222 F).

Definition make_functor_topos_with_NNO_univ
           {E₁ E₂ : univ_topos_with_NNO_univ}
           (F : functor_pretopos E₁ E₂)
           (HF : preserves_subobject_classifier
                   F
                   (terminal_univ_cat_with_finlim E₁)
                   (terminal_univ_cat_with_finlim E₂)
                   (functor_finlim_preserves_terminal F))
           (HF' : preserves_locally_cartesian_closed
                    (functor_finlim_preserves_pullback F)
                    (is_locally_cartesian_closed_univ_topos_with_NNO_univ E₁)
                    (is_locally_cartesian_closed_univ_topos_with_NNO_univ E₂))
           (HF'' : preserves_parameterized_NNO
                     (univ_topos_with_NNO_univ_NNO E₁)
                     (univ_topos_with_NNO_univ_NNO E₂)
                     F
                     (functor_finlim_preserves_terminal F))
           (Fu : z_iso
                   (F (univ_cat_universe E₁))
                   (univ_cat_universe E₂))
           (Fel : functor_preserves_el
                    (univ_cat_cat_stable_el_map E₁)
                    (univ_cat_cat_stable_el_map E₂)
                    (pr1 F ,, Fu))
  : functor_topos_with_NNO_univ E₁ E₂.
Show proof.

  simple refine (_ ,, (((tt ,, ((((_ ,, _) ,, (_ ,, tt )) ,, _) ,, _))
                   ,, (tt ,, _)) ,, (_ ,, _))).
  - exact (functor_pretopos_to_functor_finlim F).
  - exact (preserves_initial_functor_pretopos F).
  - exact (preserves_bincoproduct_functor_pretopos F).
  - exact (preserves_regular_epi_functor_pretopos F).
  - exact HF.
  - exact HF''.
  - exact HF'.
  - exact Fu.
  - exact Fel.

  simple refine (pr1 τ ,, _ ,, _).
  - exact (pr122 τ).
  - exact (pr222 τ).

Definition make_nat_trans_topos_with_NNO_univ
           {E₁ E₂ : univ_topos_with_NNO_univ}
           {F G : functor_topos_with_NNO_univ E₁ E₂}
           (τ : F ⟹ G)
           (p : τ (univ_cat_universe E₁)
                · functor_on_universe (functor_topos_with_NNO_universe G)
                =
                functor_on_universe (functor_topos_with_NNO_universe F))
           (q : nat_trans_preserves_el
                  (make_nat_trans_finlim τ ,, p
                    : nat_trans_finlim_ob
                        (functor_topos_with_NNO_universe F)
                        (functor_topos_with_NNO_universe G))
                  (functor_finlim_universe_preserves_el
                     (functor_topos_with_NNO_universe F))
                  (functor_finlim_universe_preserves_el
                     (functor_topos_with_NNO_universe G)))
  : nat_trans_topos_with_NNO_univ F G
  := make_nat_trans_finlim τ ,, (((tt ,, tt ) ,, (tt ,, tt )) ,, p ,, q ).

Proposition nat_trans_topos_with_NNO_eq
            {E₁ E₂ : univ_topos_with_NNO_univ}
            {F G : functor_topos_with_NNO_univ E₁ E₂}
            {τ ₁ τ ₂ : nat_trans_topos_with_NNO_univ F G}
            (p : ∏ (x : E₁ ), τ ₁ x = τ ₂ x)
  : τ ₁ = τ ₂.
Show proof.

  use subtypePath.
  {
    intro.
    use isaproptotal2.
    - intro.
      use isaproptotal2.
      + intro.
        apply isaprop_nat_trans_preserves_el.
      + intros.
        apply homset_property.
    - intros.
      use pathsdirprod ; use pathsdirprod ; apply isapropunit.
  }
  use nat_trans_finlim_eq.
  exact p.

3. The bicategory of elementary topos comprehension categories with a NNO and universe

Definition disp_bicat_univ_topos_with_NNO_univ_language
  : disp_bicat bicat_of_dfl_full_comp_cat
  := disp_dirprod_bicat
       disp_bicat_univ_topos_with_NNO_language
       disp_bicat_dfl_full_comp_cat_with_univ.

Proposition disp_2cells_isaprop_disp_bicat_univ_topos_with_NNO_univ_language
  : disp_2cells_isaprop disp_bicat_univ_topos_with_NNO_univ_language.
Show proof.

  use disp_2cells_isaprop_prod.
  - exact disp_2cells_isaprop_disp_bicat_univ_topos_with_NNO_language.
  - exact disp_2cells_isaprop_disp_bicat_dfl_full_comp_cat_with_univ.

Proposition disp_locally_groupoid_disp_bicat_univ_topos_with_NNO_univ_language
: disp_locally_groupoid disp_bicat_univ_topos_with_NNO_univ_language.
Show proof.

  use disp_locally_groupoid_prod.
  - exact disp_locally_groupoid_disp_bicat_univ_topos_with_NNO_language.
  - exact disp_locally_groupoid_disp_bicat_dfl_full_comp_cat_with_univ.

Proposition disp_univalent_2_disp_bicat_univ_topos_with_NNO_univ_language
: disp_univalent_2 disp_bicat_univ_topos_with_NNO_univ_language.
Show proof.

  use is_univalent_2_dirprod_bicat.
  - exact is_univalent_2_1_bicat_of_dfl_full_comp_cat.
  - exact disp_univalent_2_disp_bicat_univ_topos_with_NNO_language.
  - exact disp_univalent_2_disp_bicat_dfl_full_comp_cat_with_univ.

Proposition disp_univalent_2_0_disp_bicat_univ_topos_with_NNO_univ_language
: disp_univalent_2_0 disp_bicat_univ_topos_with_NNO_univ_language.
Show proof.

apply disp_univalent_2_disp_bicat_univ_topos_with_NNO_univ_language.

Proposition disp_univalent_2_1_disp_bicat_univ_topos_with_NNO_univ_language
: disp_univalent_2_1 disp_bicat_univ_topos_with_NNO_univ_language.
Show proof.

apply disp_univalent_2_disp_bicat_univ_topos_with_NNO_univ_language.

Definition univ_topos_with_NNO_univ_language
  : bicat
  := total_bicat disp_bicat_univ_topos_with_NNO_univ_language.

Proposition is_univalent_2_univ_topos_with_NNO_univ_language
  : is_univalent_2 univ_topos_with_NNO_univ_language.
Show proof.

  use total_is_univalent_2.
  - exact disp_univalent_2_disp_bicat_univ_topos_with_NNO_univ_language.
  - exact is_univalent_2_bicat_of_dfl_full_comp_cat.

Proposition is_univalent_2_0_univ_topos_with_NNO_univ_language
: is_univalent_2_0 univ_topos_with_NNO_univ_language.
Show proof.

apply is_univalent_2_univ_topos_with_NNO_univ_language.

Proposition is_univalent_2_1_univ_topos_with_NNO_univ_language
: is_univalent_2_1 univ_topos_with_NNO_univ_language.
Show proof.

apply is_univalent_2_univ_topos_with_NNO_univ_language.

4. Accessors for elementary toposes comprehension categories with a NNO and universe

  use make_dfl_full_comp_cat_with_univ.
  - exact (topos_NNO_comp_cat_univ_to_dfl_comp_cat C).
  - exact (pr122 C).
  - exact (pr222 C).

  use make_dfl_full_comp_cat_with_univ_functor.
  - exact F.
  - exact (pr122 F).
  - exact (pr222 F).

  use make_dfl_full_comp_cat_with_univ_nat_trans.
  - simple refine (_ ,, _).
    + exact (pr111 τ).
    + exact (pr122 τ).
  - exact (pr222 τ).

5. The biequivalence

Definition disp_psfunctor_lang_univ_topos_with_NNO_univ
  : disp_psfunctor
      disp_bicat_of_univ_topos_with_NNO_univ
      disp_bicat_univ_topos_with_NNO_univ_language
      finlim_biequiv_dfl_comp_cat_psfunctor.
Show proof.

  refine (prod_disp_psfunctor
            _ _ _ _
            disp_psfunctor_lang_univ_topos_with_NNO
            finlim_to_dfl_comp_cat_disp_psfunctor_universe).
  - use disp_2cells_isaprop_prod.
    + apply disp_2cells_isaprop_disp_bicat_of_cat_property_dfl_full_comp_cat.
    + exact disp_2cells_isaprop_disp_bicat_of_pi_type_dfl_full_comp_cat.
  - use disp_locally_groupoid_prod.
    + apply disp_locally_groupoid_disp_bicat_of_cat_property_dfl_full_comp_cat.
    + exact disp_locally_groupoid_disp_bicat_of_pi_type_dfl_full_comp_cat.
  - exact disp_2cells_isaprop_disp_bicat_dfl_full_comp_cat_with_univ.
  - exact disp_locally_groupoid_disp_bicat_dfl_full_comp_cat_with_univ.

Definition lang_univ_topos_with_NNO_univ
  : psfunctor
      bicat_of_univ_topos_with_NNO_univ
      univ_topos_with_NNO_univ_language
  := total_psfunctor
       _ _ _
       disp_psfunctor_lang_univ_topos_with_NNO_univ.

Definition internal_language_univ_topos_with_NNO_univ
  : is_biequivalence lang_univ_topos_with_NNO_univ.
Show proof.

  refine (total_is_biequivalence
            _ _ _
            (prod_disp_is_biequivalence_data
               _ _ _ _
               _ _ _ _
               _ _ _ _
               _ _ _ _
               (prod_disp_is_biequivalence_data
                  _ _ _ _
                  _ _ _ _
                  _ _ _ _
                  _ _ _ _
                  (finlim_biequiv_dfl_comp_cat_psfunctor_local_property
                     topos_with_NNO_local_property)
                  finlim_biequiv_dfl_comp_cat_psfunctor_pi_types)
               finlim_biequiv_dfl_comp_cat_psfunctor_universe)).
  - use disp_2cells_isaprop_prod.
    + apply disp_2cells_isaprop_disp_bicat_of_univ_cat_with_cat_property.
    + exact disp_2cells_isaprop_univ_lccc.
  - use disp_locally_groupoid_prod.
    + apply disp_locally_groupoid_disp_bicat_of_univ_cat_with_cat_property.
    + exact disp_locally_groupoid_univ_lccc.
  - exact disp_2cells_isaprop_disp_bicat_finlim_universe.
  - exact disp_locally_groupoid_disp_bicat_finlim_universe.
  - apply disp_2cells_isaprop_disp_bicat_of_univ_cat_with_cat_property.
  - apply disp_locally_groupoid_disp_bicat_of_univ_cat_with_cat_property.
  - exact disp_2cells_isaprop_univ_lccc.
  - exact disp_locally_groupoid_univ_lccc.

6. Type formers in a topos with a universe

6.1. Parameterized NNO

Definition disp_cat_ob_mor_topos_with_NNO_univ_nno_type
: disp_cat_ob_mor bicat_of_univ_topos_with_NNO_univ.
Show proof.

  simple refine (_ ,, _).
  - exact (λ (E : univ_topos_with_NNO_univ ),
           pnno_in_cat_univ
             (C := E)
             (univ_topos_with_NNO_univ_NNO E)).
  - exact (λ (E₁ E₂ : univ_topos_with_NNO_univ)
             (c₁ : pnno_in_cat_univ
                     (C := E₁)
                     (univ_topos_with_NNO_univ_NNO E₁))
             (c₂ : pnno_in_cat_univ
                     (C := E₂)
                     (univ_topos_with_NNO_univ_NNO E₂))
             (F : functor_topos_with_NNO_univ E₁ E₂ ),
           functor_preserves_pnno_in_cat_univ
             c₁ c₂
             (functor_topos_with_NNO_universe F)
             (preserves_NNO_functor_topos_with_NNO_univ F)).

Proposition disp_cat_id_comp_topos_with_NNO_univ_nno_type
  : disp_cat_id_comp
      bicat_of_univ_topos_with_NNO_univ
      disp_cat_ob_mor_topos_with_NNO_univ_nno_type.
Show proof.

  split.
  - intros E c.
    refine (transportf
              (functor_preserves_pnno_in_cat_univ _ _ _)
              _
              (id_functor_preserves_pnno_in_cat_univ c)).
    apply isaprop_preserves_parameterized_NNO.
  - intros E₁ E₂ E₃ F G c₁ c₂ c₃ Fc Gc.
    refine (transportf
              (functor_preserves_pnno_in_cat_univ _ _ _)
              _
              (comp_functor_preserves_pnno_in_cat_univ Fc Gc)).
    apply isaprop_preserves_parameterized_NNO.

Definition disp_cat_data_topos_with_NNO_univ_nno_type
: disp_cat_data bicat_of_univ_topos_with_NNO_univ.
Show proof.

  simple refine (_ ,, _).
  - exact disp_cat_ob_mor_topos_with_NNO_univ_nno_type.
  - exact disp_cat_id_comp_topos_with_NNO_univ_nno_type.

Definition disp_bicat_topos_with_NNO_univ_nno_type
: disp_bicat bicat_of_univ_topos_with_NNO_univ.
Show proof.

use disp_cell_unit_bicat.
exact disp_cat_data_topos_with_NNO_univ_nno_type.

Proposition disp_univalent_2_disp_bicat_topos_with_NNO_univ_nno_type
: disp_univalent_2 disp_bicat_topos_with_NNO_univ_nno_type.
Show proof.

  use disp_cell_unit_bicat_univalent_2.
  - exact is_univalent_2_1_bicat_of_univ_topos_with_NNO_univ.
  - intros.
    apply isaprop_functor_preserves_type_in_cat_univ.
  - intros.
    apply isaset_type_in_cat_univ.
  - intros E c₁ c₂ F.
    apply pnno_in_cat_univ_univalence_lemma.
    refine (transportf
              (functor_preserves_pnno_in_cat_univ _ _ _)
              _
              (pr1 F)).
    apply isaprop_preserves_parameterized_NNO.

Proposition disp_univalent_2_0_disp_bicat_topos_with_NNO_univ_nno_type
: disp_univalent_2_0 disp_bicat_topos_with_NNO_univ_nno_type.
Show proof.

apply disp_univalent_2_disp_bicat_topos_with_NNO_univ_nno_type.

Proposition disp_univalent_2_1_disp_bicat_topos_with_NNO_univ_nno_type
: disp_univalent_2_1 disp_bicat_topos_with_NNO_univ_nno_type.
Show proof.

apply disp_univalent_2_disp_bicat_topos_with_NNO_univ_nno_type.

6.2. Subobject classifier

Definition disp_cat_ob_mor_topos_with_NNO_univ_subobj_classifier
: disp_cat_ob_mor bicat_of_univ_topos_with_NNO_univ.
Show proof.

  simple refine (_ ,, _).
  - exact (λ (E : univ_topos_with_NNO_univ ),
           subobject_classifier_in_cat_univ
             (C := E)
             (univ_topos_with_NNO_univ_subobject_classifier E)).
  - exact (λ (E₁ E₂ : univ_topos_with_NNO_univ)
             (c₁ : subobject_classifier_in_cat_univ
                     (C := E₁)
                     (univ_topos_with_NNO_univ_subobject_classifier E₁))
             (c₂ : subobject_classifier_in_cat_univ
                     (C := E₂)
                     (univ_topos_with_NNO_univ_subobject_classifier E₂))
             (F : functor_topos_with_NNO_univ E₁ E₂ ),
           functor_preserves_subobject_classifier_in_cat_univ
             c₁ c₂
             (functor_topos_with_NNO_universe F)
             (preserves_subobject_classifier_functor_topos_with_NNO_univ F)).

Proposition disp_cat_id_comp_topos_with_NNO_univ_subobj_classifier
  : disp_cat_id_comp
      bicat_of_univ_topos_with_NNO_univ
      disp_cat_ob_mor_topos_with_NNO_univ_subobj_classifier.
Show proof.

  split.
  - intros E c.
    refine (transportf
              (functor_preserves_subobject_classifier_in_cat_univ _ _ _)
              _
              (id_functor_preserves_subobject_classifier_in_cat_univ c)).
    apply isaprop_preserves_subobject_classifier.
  - intros E₁ E₂ E₃ F G c₁ c₂ c₃ Fc Gc.
    refine (transportf
              (functor_preserves_subobject_classifier_in_cat_univ _ _ _)
              _
              (comp_functor_preserves_subobject_classifier_in_cat_univ Fc Gc)).
    apply isaprop_preserves_subobject_classifier.

Definition disp_cat_data_topos_with_NNO_univ_subobj_classifier
: disp_cat_data bicat_of_univ_topos_with_NNO_univ.
Show proof.

  simple refine (_ ,, _).
  - exact disp_cat_ob_mor_topos_with_NNO_univ_subobj_classifier.
  - exact disp_cat_id_comp_topos_with_NNO_univ_subobj_classifier.

Definition disp_bicat_topos_with_NNO_univ_subobj_classifier
: disp_bicat bicat_of_univ_topos_with_NNO_univ.
Show proof.

use disp_cell_unit_bicat.
exact disp_cat_data_topos_with_NNO_univ_subobj_classifier.

Proposition disp_univalent_2_disp_bicat_topos_with_NNO_univ_subobj_classifier
: disp_univalent_2 disp_bicat_topos_with_NNO_univ_subobj_classifier.
Show proof.

  use disp_cell_unit_bicat_univalent_2.
  - exact is_univalent_2_1_bicat_of_univ_topos_with_NNO_univ.
  - intros.
    apply isaprop_functor_preserves_type_in_cat_univ.
  - intros.
    apply isaset_type_in_cat_univ.
  - intros E c₁ c₂ F.
    apply subobject_classifier_in_cat_univ_univalence_lemma.
    refine (transportf
              (functor_preserves_subobject_classifier_in_cat_univ _ _ _)
              _
              (pr1 F)).
    apply isaprop_preserves_subobject_classifier.

Proposition disp_univalent_2_0_disp_bicat_topos_with_NNO_univ_subobj_classifier
: disp_univalent_2_0 disp_bicat_topos_with_NNO_univ_subobj_classifier.
Show proof.

apply disp_univalent_2_disp_bicat_topos_with_NNO_univ_subobj_classifier.

Proposition disp_univalent_2_1_disp_bicat_topos_with_NNO_univ_subobj_classifier
: disp_univalent_2_1 disp_bicat_topos_with_NNO_univ_subobj_classifier.
Show proof.

apply disp_univalent_2_disp_bicat_topos_with_NNO_univ_subobj_classifier.

6.3. Propositional resizing

Definition disp_cat_ob_mor_topos_with_NNO_univ_resizing
: disp_cat_ob_mor bicat_of_univ_topos_with_NNO_univ.
Show proof.

  simple refine (_ ,, _).
  - exact (λ (E : univ_topos_with_NNO_univ ),
           cat_univ_stable_codes_resizing E).
  - exact (λ (E₁ E₂ : univ_topos_with_NNO_univ)
             (c₁ : cat_univ_stable_codes_resizing E₁)
             (c₂ : cat_univ_stable_codes_resizing E₂)
             (F : functor_topos_with_NNO_univ E₁ E₂ ),
           functor_preserves_stable_resizing_codes
             c₁ c₂
             (functor_topos_with_NNO_universe F)).

Proposition disp_cat_id_comp_topos_with_NNO_univ_resizing
  : disp_cat_id_comp
      bicat_of_univ_topos_with_NNO_univ
      disp_cat_ob_mor_topos_with_NNO_univ_resizing.
Show proof.

  split.
  - intros E c.
    exact (identity_preserves_resizing_codes c).
  - intros E₁ E₂ E₃ F G c₁ c₂ c₃ Fc Gc.
    exact (comp_preserves_resizing_codes Fc Gc).

Definition disp_cat_data_topos_with_NNO_univ_resizing
: disp_cat_data bicat_of_univ_topos_with_NNO_univ.
Show proof.

  simple refine (_ ,, _).
  - exact disp_cat_ob_mor_topos_with_NNO_univ_resizing.
  - exact disp_cat_id_comp_topos_with_NNO_univ_resizing.

Definition disp_bicat_topos_with_NNO_univ_resizing
: disp_bicat bicat_of_univ_topos_with_NNO_univ.
Show proof.

use disp_cell_unit_bicat.
exact disp_cat_data_topos_with_NNO_univ_resizing.

Proposition disp_univalent_2_disp_bicat_topos_with_NNO_univ_resizing
: disp_univalent_2 disp_bicat_topos_with_NNO_univ_resizing.
Show proof.

  use disp_cell_unit_bicat_univalent_2.
  - exact is_univalent_2_1_bicat_of_univ_topos_with_NNO_univ.
  - intros.
    apply isaprop_functor_preserves_stable_resizing_codes.
  - intros.
    apply isaset_cat_univ_stable_codes_resizing.
  - intros E c₁ c₂ F.
    apply cat_univ_stable_codes_resizing_univalence_lemma.
    exact (pr1 F).

Proposition disp_univalent_2_0_disp_bicat_topos_with_NNO_univ_resizing
: disp_univalent_2_0 disp_bicat_topos_with_NNO_univ_resizing.
Show proof.

apply disp_univalent_2_disp_bicat_topos_with_NNO_univ_resizing.

Proposition disp_univalent_2_1_disp_bicat_topos_with_NNO_univ_resizing
: disp_univalent_2_1 disp_bicat_topos_with_NNO_univ_resizing.
Show proof.

apply disp_univalent_2_disp_bicat_topos_with_NNO_univ_resizing.

6.4. ∑-types

Definition disp_cat_ob_mor_topos_with_NNO_univ_sigma
: disp_cat_ob_mor bicat_of_univ_topos_with_NNO_univ.
Show proof.

  simple refine (_ ,, _).
  - exact (λ (E : univ_topos_with_NNO_univ ),
           cat_univ_stable_codes_sigma E).
  - exact (λ (E₁ E₂ : univ_topos_with_NNO_univ)
             (c₁ : cat_univ_stable_codes_sigma E₁)
             (c₂ : cat_univ_stable_codes_sigma E₂)
             (F : functor_topos_with_NNO_univ E₁ E₂ ),
           functor_preserves_stable_codes_sigma
             c₁ c₂
             (functor_topos_with_NNO_universe F)).

Proposition disp_cat_id_comp_topos_with_NNO_univ_sigma
  : disp_cat_id_comp
      bicat_of_univ_topos_with_NNO_univ
      disp_cat_ob_mor_topos_with_NNO_univ_sigma.
Show proof.

  split.
  - intros E c.
    exact (identity_preserves_stable_codes_sigma c).
  - intros E₁ E₂ E₃ F G c₁ c₂ c₃ Fc Gc.
    exact (comp_preserves_stable_codes_sigma Fc Gc).

Definition disp_cat_data_topos_with_NNO_univ_sigma
: disp_cat_data bicat_of_univ_topos_with_NNO_univ.
Show proof.

  simple refine (_ ,, _).
  - exact disp_cat_ob_mor_topos_with_NNO_univ_sigma.
  - exact disp_cat_id_comp_topos_with_NNO_univ_sigma.

Definition disp_bicat_topos_with_NNO_univ_sigma
: disp_bicat bicat_of_univ_topos_with_NNO_univ.
Show proof.

use disp_cell_unit_bicat.
exact disp_cat_data_topos_with_NNO_univ_sigma.

Proposition disp_univalent_2_disp_bicat_topos_with_NNO_univ_sigma
: disp_univalent_2 disp_bicat_topos_with_NNO_univ_sigma.
Show proof.

  use disp_cell_unit_bicat_univalent_2.
  - exact is_univalent_2_1_bicat_of_univ_topos_with_NNO_univ.
  - intros.
    apply isaprop_functor_preserves_stable_codes_sigma.
  - intros.
    apply isaset_cat_univ_stable_codes_sigma.
  - intros E c₁ c₂ F.
    apply sigma_univ_univalence_lemma.
    exact (pr1 F).

Proposition disp_univalent_2_0_disp_bicat_topos_with_NNO_univ_sigma
: disp_univalent_2_0 disp_bicat_topos_with_NNO_univ_sigma.
Show proof.

apply disp_univalent_2_disp_bicat_topos_with_NNO_univ_sigma.

Proposition disp_univalent_2_1_disp_bicat_topos_with_NNO_univ_sigma
: disp_univalent_2_1 disp_bicat_topos_with_NNO_univ_sigma.
Show proof.

apply disp_univalent_2_disp_bicat_topos_with_NNO_univ_sigma.

6.5. ∏-types

Definition disp_cat_ob_mor_topos_with_NNO_univ_pi
: disp_cat_ob_mor bicat_of_univ_topos_with_NNO_univ.
Show proof.

  simple refine (_ ,, _).
  - exact (λ (E : univ_topos_with_NNO_univ ),
           cat_univ_stable_codes_pi
             (C := E)
             (is_locally_cartesian_closed_univ_topos_with_NNO_univ E)).
  - exact (λ (E₁ E₂ : univ_topos_with_NNO_univ)
             (c₁ : cat_univ_stable_codes_pi
                     (C := E₁)
                     (is_locally_cartesian_closed_univ_topos_with_NNO_univ E₁))
             (c₂ : cat_univ_stable_codes_pi
                     (C := E₂)
                     (is_locally_cartesian_closed_univ_topos_with_NNO_univ E₂))
             (F : functor_topos_with_NNO_univ E₁ E₂ ),
           functor_preserves_stable_codes_pi
             c₁ c₂
             (functor_topos_with_NNO_universe F)
             (preserves_locally_cartesian_closed_functor_topos_with_NNO_univ F)).

Proposition disp_cat_id_comp_topos_with_NNO_univ_pi
  : disp_cat_id_comp
      bicat_of_univ_topos_with_NNO_univ
      disp_cat_ob_mor_topos_with_NNO_univ_pi.
Show proof.

  split.
  - intros E c.
    exact (identity_preserves_stable_codes_pi c).
  - intros E₁ E₂ E₃ F G c₁ c₂ c₃ Fc Gc.
    exact (comp_preserves_stable_codes_pi Fc Gc).

Definition disp_cat_data_topos_with_NNO_univ_pi
: disp_cat_data bicat_of_univ_topos_with_NNO_univ.
Show proof.