Library UniMath.Bicategories.ComprehensionCat.DFLCompCat

1. The bicategory of DFL comprehension categories

Definition disp_bicat_of_dfl_full_comp_cat
  : disp_bicat bicat_full_comp_cat
  := disp_dirprod_bicat
       disp_bicat_of_democracy
       (disp_dirprod_bicat
          disp_bicat_of_strong_unit_type
          (disp_dirprod_bicat
             disp_bicat_of_prod_type_full_comp_cat
             (disp_dirprod_bicat
                disp_bicat_of_equalizer_type_full_comp_cat
                disp_bicat_of_sigma_type_full_comp_cat))).

Definition bicat_of_dfl_full_comp_cat
  : bicat
  := total_bicat disp_bicat_of_dfl_full_comp_cat.

2. This bicategory is univalent

Definition is_univalent_2_1_disp_bicat_of_dfl_full_comp_cat
: disp_univalent_2_1 disp_bicat_of_dfl_full_comp_cat.
Show proof.

  use is_univalent_2_1_dirprod_bicat.
  {
    exact univalent_2_1_disp_bicat_of_democracy.
  }
  use is_univalent_2_1_dirprod_bicat.
  {
    exact univalent_2_1_disp_bicat_of_strong_unit_type.
  }
  use is_univalent_2_1_dirprod_bicat.
  {
    exact univalent_2_1_disp_bicat_of_prod_type_full_comp_cat.
  }
  use is_univalent_2_1_dirprod_bicat.
  {
    exact univalent_2_1_disp_bicat_of_equalizer_type_full_comp_cat.
  }
  exact univalent_2_1_disp_bicat_of_sigma_type_full_comp_cat.

Definition is_univalent_2_0_disp_bicat_of_dfl_full_comp_cat
: disp_univalent_2_0 disp_bicat_of_dfl_full_comp_cat.
Show proof.

  use (is_univalent_2_0_dirprod_bicat _ _ is_univalent_2_1_bicat_full_comp_cat).
  {
    exact univalent_2_disp_bicat_of_democracy.
  }
  use (is_univalent_2_dirprod_bicat _ _ is_univalent_2_1_bicat_full_comp_cat).
  {
    exact univalent_2_disp_bicat_of_strong_unit_type.
  }
  use (is_univalent_2_dirprod_bicat _ _ is_univalent_2_1_bicat_full_comp_cat).
  {
    exact univalent_2_disp_bicat_of_prod_type_full_comp_cat.
  }
  use (is_univalent_2_dirprod_bicat _ _ is_univalent_2_1_bicat_full_comp_cat).
  {
    exact univalent_2_disp_bicat_of_equalizer_type_full_comp_cat.
  }
  exact univalent_2_disp_bicat_of_sigma_type_full_comp_cat.

Definition is_univalent_2_disp_bicat_of_dfl_full_comp_cat
: disp_univalent_2 disp_bicat_of_dfl_full_comp_cat.
Show proof.

  split.
  - exact is_univalent_2_0_disp_bicat_of_dfl_full_comp_cat.
  - exact is_univalent_2_1_disp_bicat_of_dfl_full_comp_cat.

Proposition is_univalent_2_1_bicat_of_dfl_full_comp_cat
: is_univalent_2_1 bicat_of_dfl_full_comp_cat.
Show proof.

  use total_is_univalent_2_1.
  - exact is_univalent_2_1_bicat_full_comp_cat.
  - exact is_univalent_2_1_disp_bicat_of_dfl_full_comp_cat.

Proposition is_univalent_2_0_bicat_of_dfl_full_comp_cat
: is_univalent_2_0 bicat_of_dfl_full_comp_cat.
Show proof.

  use total_is_univalent_2_0.
  - exact is_univalent_2_0_bicat_full_comp_cat.
  - exact is_univalent_2_0_disp_bicat_of_dfl_full_comp_cat.

Proposition is_univalent_2_bicat_of_dfl_full_comp_cat
: is_univalent_2 bicat_of_dfl_full_comp_cat.
Show proof.

  split.
  - exact is_univalent_2_0_bicat_of_dfl_full_comp_cat.
  - exact is_univalent_2_1_bicat_of_dfl_full_comp_cat.

3. Builders and accessors

  use subtypePath.
  {
    intro.
    repeat (use isapropdirprod) ; apply isapropunit.
  }
  exact (full_comp_nat_trans_eq p pp).

Definition dfl_full_comp_cat_fiber
           {C : dfl_full_comp_cat}
           (Γ : C)
  : univ_cat_with_finlim.
Show proof.

  use make_univ_cat_with_finlim.
  - exact (univalent_fiber_category (disp_cat_of_types C) Γ).
  - apply dfl_full_comp_cat_terminal.
  - use Pullbacks_from_Equalizers_BinProducts.
    + apply fiberwise_binproducts_dfl_full_comp_cat.
    + apply fiberwise_equalizers_dfl_full_comp_cat.

Definition dfl_full_comp_cat_fiber_functor
           {C : dfl_full_comp_cat}
           {Γ₁ Γ₂ : C}
           (s : Γ₁ --> Γ₂)
  : functor_finlim (dfl_full_comp_cat_fiber Γ₂) (dfl_full_comp_cat_fiber Γ₁).
Show proof.

  use make_functor_finlim.
  - exact (fiber_functor_from_cleaving _ (cleaving_of_types C) s).
  - apply fiberwise_terminal_dfl_full_comp_cat.
  - use preserves_pullback_from_binproduct_equalizer.
    + apply fiberwise_binproducts_dfl_full_comp_cat.
    + apply fiberwise_equalizers_dfl_full_comp_cat.
    + apply fiberwise_binproducts_dfl_full_comp_cat.
    + apply fiberwise_equalizers_dfl_full_comp_cat.

Definition dfl_full_comp_cat_functor_fiber_functor
           {C₁ C₂ : dfl_full_comp_cat}
           (F : dfl_full_comp_cat_functor C₁ C₂)
           (Γ : C₁)
  : functor_finlim (dfl_full_comp_cat_fiber Γ) (dfl_full_comp_cat_fiber (F Γ)).
Show proof.

  use make_functor_finlim.
  - exact (fiber_functor (comp_cat_type_functor F) Γ).
  - apply preserves_terminal_dfl_full_comp_cat_functor.
  - use preserves_pullback_from_binproduct_equalizer.
    + apply fiberwise_binproducts_dfl_full_comp_cat.
    + apply fiberwise_equalizers_dfl_full_comp_cat.
    + apply preserves_binproducts_dfl_full_comp_cat_functor.
    + apply preserves_equalizers_dfl_full_comp_cat_functor.

4. Invertible 2-cells

Section Invertible.
  Context {C₁ C₂ : dfl_full_comp_cat}
          {F G : dfl_full_comp_cat_functor C₁ C₂}
          (τ : dfl_full_comp_cat_nat_trans F G)
          (H τ : ∏ (x : C₁ ), is_z_isomorphism (τ x)).

  Let τ iso : nat_z_iso F G := _ ,, H τ.

  Context (H τ' : is_disp_nat_z_iso τ iso (comp_cat_type_nat_trans τ)).

  Let ττ iso
    : disp_nat_z_iso (comp_cat_type_functor F) (comp_cat_type_functor G) τ iso
    := _ ,, H τ'.

  Definition is_invertible_dfl_full_comp_cat_nat_trans_inv_cleaving
    : nat_trans_with_terminal_cleaving G F.
  Show proof.

    use make_nat_trans_with_terminal_cleaving.
    use make_nat_trans_with_terminal_disp_cat.
    - exact (nat_z_iso_inv τ iso).
    - exact (disp_nat_z_iso_inv ττ iso).

  Proposition is_invertible_dfl_full_comp_cat_nat_trans_inv_eq
    : comprehension_nat_trans_eq
        is_invertible_dfl_full_comp_cat_nat_trans_inv_cleaving
        (comp_cat_functor_comprehension G)
        (comp_cat_functor_comprehension F).
  Show proof.

    intros x xx.
    cbn.
    refine (!_).
    use (z_iso_inv_on_right _ _ _ (_ ,, H τ _)).
    cbn.
    rewrite !assoc.
    refine (!_).
    etrans.
    {
      apply maponpaths_2.
      exact (!(comp_cat_nat_trans_comprehension τ xx)).
    }
    rewrite !assoc'.
    refine (_ @ id_right _).
    apply maponpaths.
    rewrite <- comprehension_functor_mor_comp.
    etrans.
    {
      apply maponpaths.
      exact (disp_nat_z_iso_iso_inv ττ iso x xx).
    }
    rewrite comprehension_functor_mor_transportb.
    rewrite comprehension_functor_mor_id.
    apply idpath.

  Definition is_invertible_dfl_full_comp_cat_nat_trans_inv
    : dfl_full_comp_cat_nat_trans G F.
  Show proof.

    use make_dfl_full_comp_cat_nat_trans.
    use make_full_comp_cat_nat_trans.
    use make_comp_cat_nat_trans.
    - exact is_invertible_dfl_full_comp_cat_nat_trans_inv_cleaving.
    - exact is_invertible_dfl_full_comp_cat_nat_trans_inv_eq.

  Proposition is_invertible_dfl_full_comp_cat_nat_trans_left
    : τ • is_invertible_dfl_full_comp_cat_nat_trans_inv = id₂ F.
  Show proof.

    use dfl_full_comp_cat_nat_trans_eq.
    - intro x.
      apply (z_iso_inv_after_z_iso (_ ,, H τ x)).
    - intros x xx.
      etrans.
      {
        apply maponpaths.
        exact (disp_nat_z_iso_iso_inv ττ iso x xx).
      }
      unfold transportb.
      rewrite transport_f_f.
      use transportf_set.
      apply homset_property.

  Proposition is_invertible_dfl_full_comp_cat_nat_trans_right
    : is_invertible_dfl_full_comp_cat_nat_trans_inv • τ = id₂ G.
  Show proof.

    use dfl_full_comp_cat_nat_trans_eq.
    - intro x.
      apply (z_iso_after_z_iso_inv (_ ,, H τ x)).
    - intros x xx.
      etrans.
      {
        apply maponpaths.
        exact (disp_nat_z_iso_inv_iso ττ iso x xx).
      }
      unfold transportb.
      rewrite transport_f_f.
      use transportf_set.
      apply homset_property.

  Definition is_invertible_dfl_full_comp_cat_nat_trans
    : is_invertible_2cell τ.
  Show proof.

    use make_is_invertible_2cell.
    - exact is_invertible_dfl_full_comp_cat_nat_trans_inv.
    - exact is_invertible_dfl_full_comp_cat_nat_trans_left.
    - exact is_invertible_dfl_full_comp_cat_nat_trans_right.

End Invertible.

5. The adjoint equivalence coming from democracy

Definition dfl_full_comp_cat_adjequiv_empty
           (C : dfl_full_comp_cat)
  : adj_equivalence_of_cats
      (fiber_functor (comp_cat_comprehension C) []).
Show proof.

  use rad_equivalence_of_cats.
  - use is_univalent_fiber.
    apply disp_univalent_category_is_univalent_disp.
  - use full_comp_cat_comprehension_fiber_fully_faithful.
  - abstract
      (intro y ;
       use hinhpr ;
       exact (is_democratic_weq_split_essentially_surjective
                C
                (is_democratic_dfl_full_comp_cat C)
                y)).

Definition dfl_full_comp_cat_adjequiv_terminal
           (C : dfl_full_comp_cat)
           (T : Terminal C)
  : adj_equivalence_of_cats
      (fiber_functor (comp_cat_comprehension C) T).
Show proof.

  enough ([] = T) as p.
  {
    induction p.
    exact (dfl_full_comp_cat_adjequiv_empty C).
  }
  use subtypePath.
  {
    intro.
    apply isaprop_isTerminal.
  }
  use (isotoid _ (univalent_category_is_univalent C)).
  apply z_iso_Terminals.

Definition dfl_full_comp_cat_adjequiv_base
           (C : dfl_full_comp_cat)
  : adj_equivalence_of_cats
      (fiber_functor (comp_cat_comprehension C) []
       ∙ cod_fib_terminal_to_base _).
Show proof.

  use comp_adj_equivalence_of_cats.
  - exact (dfl_full_comp_cat_adjequiv_empty C).
  - exact (cod_fib_terminal _).

6. Adjoint equivalences of DFL comprehension categories

Definition dfl_full_comp_cat_left_adjoint_equivalence_from_full_comp_cat
           {C₁ C₂ : dfl_full_comp_cat}
           (F : dfl_full_comp_cat_functor C₁ C₂)
           (HF : left_adjoint_equivalence (pr1 F))
  : left_adjoint_equivalence F.
Show proof.

  use (invmap (left_adjoint_equivalence_total_disp_weq _ _)).
  refine (HF ,, _).
  use (pair_left_adjoint_equivalence _ _ (_ ,, HF)).
  split.
  - apply disp_left_adjoint_equivalence_fullsubbicat.
  - use (pair_left_adjoint_equivalence _ _ (_ ,, HF)).
    split.
    + apply disp_adjoint_equiv_disp_bicat_of_strong_unit_type.
    + use (pair_left_adjoint_equivalence _ _ (_ ,, HF)).
      split.
      * apply disp_adjoint_equiv_disp_bicat_of_prod_type_full_comp_cat.
      * use (pair_left_adjoint_equivalence _ _ (_ ,, HF)).
        split.
        ** apply disp_adjoint_equiv_disp_bicat_of_equalizer_type_full_comp_cat.
        ** apply disp_adjoint_equiv_disp_bicat_of_sigma_type_full_comp_cat.

Definition dfl_full_comp_cat_left_adjoint_equivalence
           {C₁ C₂ : dfl_full_comp_cat}
           (F : dfl_full_comp_cat_functor C₁ C₂)
           (HF : adj_equivalence_of_cats F)
           (HF' : is_equiv_over (_ ,, HF) (comp_cat_type_functor F))
  : left_adjoint_equivalence F.
Show proof.

  use dfl_full_comp_cat_left_adjoint_equivalence_from_full_comp_cat.
  use full_comp_cat_left_adjoint_equivalence.
  use comp_cat_left_adjoint_equivalence.
  - use cat_with_terminal_cleaving_left_adjoint_equivalence.
    + exact HF.
    + exact HF'.
  - intros x xx.
    use is_z_iso_disp_codomain.
    exact (full_comp_cat_functor_is_z_iso F xx).