Library UniMath.Bicategories.ComprehensionCat.InternalLanguageTopos.PiPretopos

The internal language of ∏-pretoposes

In other files, we gave several extensions of the biequivalence between categories with finite limits and full DFL comprehension categories. Now we put these extensions together in order to obtain internal language theorems for several classes of toposes. The results are split over several files.

In this file we consider ∏-pretoposes with a parameterized natural numbers objects. Recall that a pretopos is a category that is both extensive and exact. A ∏-pretopos is a locally Cartesian closed pretopos. To obtain the desired biequivalence, we combine the biequivalence for locally Cartesian closed categories and ∏-types in comprehension categories with the biequivalence for local properties.

Contents 1. The bicategory of ∏-pretoposes 2. Accessors for ∏-pretoposes 3. The bicategory of ∏-pretopos comprehension categories 4. Accessors for ∏-pretopos comprehension categories 5. The biequivalence

1. The bicategory of ∏-pretoposes

Definition disp_bicat_of_univ_pretopos
  : disp_bicat bicat_of_univ_cat_with_finlim
  := disp_dirprod_bicat
       (disp_bicat_of_univ_cat_with_cat_property pretopos_local_property)
       disp_bicat_univ_lccc.

Proposition disp_2cells_isaprop_disp_bicat_of_univ_pretopos
  : disp_2cells_isaprop disp_bicat_of_univ_pretopos.
Show proof.

  use disp_2cells_isaprop_prod.
  - apply disp_2cells_isaprop_disp_bicat_of_univ_cat_with_cat_property.
  - exact disp_2cells_isaprop_univ_lccc.

Proposition disp_locally_groupoid_disp_bicat_of_univ_pretopos
: disp_locally_groupoid disp_bicat_of_univ_pretopos.
Show proof.

  use disp_locally_groupoid_prod.
  - apply disp_locally_groupoid_disp_bicat_of_univ_cat_with_cat_property.
  - exact disp_locally_groupoid_univ_lccc.

Proposition disp_univalent_2_disp_bicat_of_univ_pretopos
: disp_univalent_2 disp_bicat_of_univ_pretopos.
Show proof.

  use is_univalent_2_dirprod_bicat.
  - exact is_univalent_2_1_bicat_of_univ_cat_with_finlim.
  - apply disp_univalent_2_disp_bicat_univ_cat_with_cat_property.
  - exact disp_univalent_2_disp_bicat_univ_lccc.

Proposition disp_univalent_2_0_disp_bicat_of_univ_pretopos
: disp_univalent_2_0 disp_bicat_of_univ_pretopos.
Show proof.

apply disp_univalent_2_disp_bicat_of_univ_pretopos.

Proposition disp_univalent_2_1_disp_bicat_of_univ_pretopos
: disp_univalent_2_1 disp_bicat_of_univ_pretopos.
Show proof.

apply disp_univalent_2_disp_bicat_of_univ_pretopos.

Definition bicat_of_univ_pi_pretopos
  : bicat
  := total_bicat disp_bicat_of_univ_pretopos.

Proposition is_univalent_2_bicat_of_univ_pi_pretopos
  : is_univalent_2 bicat_of_univ_pi_pretopos.
Show proof.

  use total_is_univalent_2.
  - exact disp_univalent_2_disp_bicat_of_univ_pretopos.
  - exact is_univalent_2_bicat_of_univ_cat_with_finlim.

Proposition is_univalent_2_0_bicat_of_univ_pi_pretopos
: is_univalent_2_0 bicat_of_univ_pi_pretopos.
Show proof.

apply is_univalent_2_bicat_of_univ_pi_pretopos.

Proposition is_univalent_2_1_bicat_of_univ_pi_pretopos
: is_univalent_2_1 bicat_of_univ_pi_pretopos.
Show proof.

apply is_univalent_2_bicat_of_univ_pi_pretopos.

2. Accessors for ∏-pretoposes

Definition univ_pi_pretopos
  : UU
  := bicat_of_univ_pi_pretopos.

Coercion univ_pi_pretopos_to_univ_pretopos
         (E : univ_pi_pretopos)
  : univ_pretopos.
Show proof.

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

Definition univ_pi_pretopos_lccc
          (E : univ_pi_pretopos)
  : is_locally_cartesian_closed (pullbacks_univ_cat_with_finlim E)
  := pr122 E.

Definition make_univ_pi_pretopos
           (E : univ_pretopos)
           (HE : is_locally_cartesian_closed (pullbacks_univ_cat_with_finlim E))
  : univ_pi_pretopos.
Show proof.

  simple refine (_ ,, ((((_ ,, (_ ,, _)) ,, _) ,, ((_ ,, _) ,, _)) ,, tt ) ,, (_ ,, tt )).
  - 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 HE.

Definition functor_pi_pretopos
           (E₁ E₂ : univ_pi_pretopos)
  : UU
  := E₁ --> E₂.

Coercion functor_pi_pretopos_to_functor_pretopos
         {E₁ E₂ : univ_pi_pretopos}
         (F : functor_pi_pretopos E₁ E₂)
  : functor_pretopos E₁ E₂.
Show proof.

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

Definition preserves_locally_cartesian_closed_functor_pi_pretopos
           {E₁ E₂ : univ_pi_pretopos}
           (F : functor_pi_pretopos E₁ E₂)
  : preserves_locally_cartesian_closed
      (functor_finlim_preserves_pullback F)
      (univ_pi_pretopos_lccc E₁)
      (univ_pi_pretopos_lccc E₂)
  := pr222 F.

Definition make_functor_pi_pretopos
           {E₁ E₂ : univ_pi_pretopos}
           (F : functor_pretopos E₁ E₂)
           (HF : preserves_locally_cartesian_closed
                   (functor_finlim_preserves_pullback F)
                   (univ_pi_pretopos_lccc E₁)
                   (univ_pi_pretopos_lccc E₂))
  : functor_pi_pretopos 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.

Definition nat_trans_pi_pretopos
           {E₁ E₂ : univ_pi_pretopos}
           (F G : functor_pi_pretopos E₁ E₂)
  : UU
  := F ==> G.

Coercion nat_trans_pi_pretopos_to_nat_trans_finlim
         {E₁ E₂ : univ_pi_pretopos}
         {F G : functor_pi_pretopos E₁ E₂}
         (τ : nat_trans_pi_pretopos F G)
  : nat_trans_finlim F G
  := pr1 τ.

Definition make_nat_trans_pi_pretopos
           {E₁ E₂ : univ_pi_pretopos}
           {F G : functor_pi_pretopos E₁ E₂}
           (τ : F ⟹ G)
  : nat_trans_pi_pretopos F G
  := make_nat_trans_finlim τ ,, (tt ,, tt ) ,, (tt ,, tt ).

Proposition nat_trans_pi_pretopos_eq
            {E₁ E₂ : univ_pi_pretopos}
            {F G : functor_pi_pretopos E₁ E₂}
            {τ ₁ τ ₂ : nat_trans_pi_pretopos F G}
            (p : ∏ (x : E₁ ), τ ₁ x = τ ₂ x)
  : τ ₁ = τ ₂.
Show proof.

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