Library UniMath.Bicategories.DisplayedBicats.Examples.CwF

Bicategories

Benedikt Ahrens, Marco Maggesi February 2018 *********************************************************************************


Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.

Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.categories.HSET.All.
Require Import UniMath.CategoryTheory.whiskering.
Require Export UniMath.CategoryTheory.yoneda.
Require Export UniMath.CategoryTheory.limits.pullbacks.

Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.

Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
Require Import UniMath.Bicategories.Morphisms.Adjunctions.
Require Import UniMath.Bicategories.Core.Invertible_2cells.
Require Import UniMath.Bicategories.Core.Univalence.
Require Import UniMath.Bicategories.DisplayedBicats.Examples.ContravariantFunctor.
Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats.
Require Import UniMath.Bicategories.DisplayedBicats.Examples.Cofunctormap.
Require Import UniMath.Bicategories.DisplayedBicats.Examples.FullSub.
Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sigma.
Require Import UniMath.Bicategories.DisplayedBicats.DispBicat.
Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions.
Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.
Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles.
Require Import UniMath.Bicategories.DisplayedBicats.Examples.Prod.
Require Import UniMath.Bicategories.DisplayedBicats.Examples.DisplayedCatToBicat.

Local Open Scope cat.
Local Open Scope mor_disp_scope.

Local Notation "'SET'" := HSET_univalent_category.
Local Notation "'PreShv' C" := [C^op,SET] (at level 4) : cat.
Local Notation "'Yo'" := (yoneda _ : functor _ (PreShv _)).

Section Yoneda.

  Context {C : category} {hsC : has_homsets C}.

  Definition yy {F : PreShv C} {c : C}
    : ((F : C^op ⟶ SET) c : hSet) ≃
      [C^op, HSET, has_homsets_HSET] ⟦ yoneda C c, F⟧.
  Show proof.
    apply invweq. apply yoneda_weq.

  Lemma yy_natural (F : PreShv C) (c : C)
        (A : (F : C^op ⟶ SET) c : hSet)
        c' (f : C⟦c', c⟧)
    : yy (functor_on_morphisms (F : C^op ⟶ SET) f A) =
      functor_on_morphisms (yoneda C) f · yy A.
  Show proof.
    assert (XTT := is_natural_yoneda_iso_inv _ F _ _ f).
    apply (toforallpaths _ _ _ XTT).

  Lemma yy_comp_nat_trans
        (F F' : PreShv C) (p : _ ⟦F, F'⟧)
        A (v : (F : C^op ⟶ SET) A : hSet)
    : yy v · p = yy ((p : nat_trans _ _ ) _ v).
  Show proof.
    apply nat_trans_eq.
    - apply has_homsets_HSET.
    - intro c. simpl.
      apply funextsec. intro f. cbn.
      assert (XR := toforallpaths _ _ _ (nat_trans_ax p _ _ f) v ).
      cbn in XR.
      apply XR.

End Yoneda.


Lemma transportf_yy
      {C : category}
      (F : opp_precat_data C ⟶ SET) (c c' : C) (A : (F : functor _ _ ) c : hSet)
      (e : c = c')

  : paths
    (pr1weq
       (@yy C F c')
       (@transportf _ (fun d => pr1hSet (functor_on_objects F d : hSet)) _ _ e A))
    (@transportf _ (fun d => nat_trans _ F) _ _ e (pr1weq (@yy C F c) A)).
Show proof.
  induction e.
  apply idpath.

Lemma inv_from_z_iso_iso_from_fully_faithful_reflection {C D : precategory}
      (F : functor C D) (HF : fully_faithful F) (a b : C) (i : z_iso (F a) (F b))
  : inv_from_z_iso
      (iso_from_fully_faithful_reflection HF i) =
    iso_from_fully_faithful_reflection HF (z_iso_inv_from_z_iso i).
Show proof.
  apply idpath.

Section CwFRepresentation.
  Context {C : category}
          {Ty Tm : opp_precat_data C ⟶ SET}
          (pp : Tm ⟹ Ty)
          (HC : is_univalent C).

  Definition cwf_fiber_rep_data {Γ:C} (A : Ty Γ : hSet) : UU
    := ∑ (ΓA : C), C ⟦ΓA, Γ⟧ × (Tm ΓA : hSet).

  Lemma cwf_square_comm {Γ} {A}
        {ΓA : C} {π : ΓA --> Γ}
        {t : Tm ΓA : hSet} (e : (pp : nat_trans _ _) _ t = functor_on_morphisms Ty π A)

    : @paths _
    (@compose _ _
       (@functor_on_objects _ (functor_category _ HSET_univalent_category) _ Γ)
       Ty (functor_on_morphisms _ π)
       (pr1weq (@yy C Ty Γ) A))
    (@compose _
       (@functor_on_objects _ (functor_category _ hset_category) _ ΓA)
       Tm Ty
       (pr1weq (@yy C Tm ΓA) t) pp).
  Show proof.
    apply pathsinv0.
    etrans. 2: apply yy_natural.
    etrans. { apply yy_comp_nat_trans. }
    apply maponpaths, e.

  Definition cwf_fiber_rep_ax
             {Γ:C} {A : Ty Γ : hSet}
             (ΓAπt : cwf_fiber_rep_data A) : UU
    := ∑ (H : pp _ (pr2 (pr2 ΓAπt)) = (#Ty)%cat (pr1 (pr2 ΓAπt)) A),
       isPullback (cwf_square_comm H).

  Definition cwf_fiber_representation {Γ:C} (A : Ty Γ : hSet) : UU
    := ∑ ΓAπt : cwf_fiber_rep_data A, cwf_fiber_rep_ax ΓAπt.

  Lemma isaprop_cwf_fiber_representation {Γ:C} (A : Ty Γ : hSet)
    : is_univalent C -> isaprop (cwf_fiber_representation A).
  Show proof.
    intro isC.
    apply invproofirrelevance.
    intros x x'. apply subtypePath.
    { intro.
      apply isofhleveltotal2.
      - apply setproperty.
      - intro. apply isaprop_isPullback.
    }
    destruct x as [x H].
    destruct x' as [x' H']. cbn.
    destruct x as [ΓA m].
    destruct x' as [ΓA' m']. cbn in *.
    destruct H as [H isP].
    destruct H' as [H' isP'].
    use (total2_paths_f).
    - set (T1 := make_Pullback _ isP).
      set (T2 := make_Pullback _ isP').
      set (i := z_iso_from_Pullback_to_Pullback T1 T2). cbn in i.
      set (i' := invmap (weq_ff_functor_on_z_iso (yoneda_fully_faithful _) _ _ ) i ).
      set (TT := isotoid _ isC i').
      apply TT.
    - cbn.
      set (XT := transportf_dirprod _ (fun a' => C⟦a', Γ⟧) (fun a' => Tm a' : hSet)).
      cbn in XT.
      set (XT' := XT (tpair _ ΓA m : ∑ R : C, C ⟦ R, Γ ⟧ × (Tm R : hSet) )
                     (tpair _ ΓA' m' : ∑ R : C, C ⟦ R, Γ ⟧ × (Tm R : hSet) )).
      cbn in *.
      match goal with | [ |- transportf _ ?e _ = _ ] => set (TT := e) end.
      rewrite XT'. clear XT' XT.
      destruct m as [π te].
      destruct m' as [π' te'].
      cbn.
      apply pathsdirprod.
      + unfold TT; clear TT.
        rewrite transportf_isotoid.
        cbn.
        unfold from_Pullback_to_Pullback.
        cbn in *.
        pose (XR' := nat_trans_eq_pointwise
                       (PullbackArrow_PullbackPr1
                          (make_Pullback _ isP)
                          (yoneda_objects C ΓA')
                          (yoneda_morphisms C ΓA' Γ π')
                          (yoneda_map_2 C ΓA' Tm te')
                          (PullbackSqrCommutes
                             (make_Pullback _ isP')))
                       ΓA').
        cbn in XR'.
        assert (XR'':= toforallpaths _ _ _ XR').
        cbn in XR''.
        etrans. { apply XR''. }
        apply id_left.
      + unfold TT; clear TT.
        match goal with |[|- transportf ?r _ _ = _ ] => set (P:=r) end.
        match goal with |[|- transportf _ (_ _ _ (_ _ ?ii)) _ = _ ] => set (i:=ii) end.
        simpl in i.
        apply (invmaponpathsweq (@yy _ Tm ΓA')).
        etrans.
        {
          apply transportf_yy.
        }
        etrans.
        {
          apply (@transportf_functor_isotoid C (functor_category _ SET)).
        }
        rewrite inv_from_z_iso_iso_from_fully_faithful_reflection.
        assert (XX:=homotweqinvweq (weq_from_fully_faithful
                                      (yoneda_fully_faithful _) ΓA' ΓA )).
        etrans. { apply maponpaths_2. apply XX. }
        clear XX.
        etrans. { apply maponpaths_2. unfold from_Pullback_to_Pullback. apply idpath. }
        pose (XR' := PullbackArrow_PullbackPr2
                       (make_Pullback _ isP)
                       (yoneda_objects C ΓA')
                       (yoneda_morphisms C ΓA' Γ π')
                       (yoneda_map_2 C ΓA' Tm te')
                       (PullbackSqrCommutes
                          (make_Pullback _ isP'))).
        apply XR'.

  Definition cwf_representation : UU
    := ∏ Γ (A : Ty Γ : hSet), cwf_fiber_representation A.

  Definition isaprop_cwf_representation
    : isaprop cwf_representation.
  Show proof.
    do 2 (apply impred ; intro).
    apply isaprop_cwf_fiber_representation.
    exact HC.
End CwFRepresentation.

Section Projections.

  Context {C : category}
          {Ty Tm : opp_precat_data C ⟶ SET}
          {pp : Tm ⟹ Ty}.

  Variable (R : cwf_representation pp).
  Variable (Γ : C) (A : Ty Γ : hSet).

  Definition ext : C := pr1 (pr1 (R Γ A)).

  Definition π : C⟦ext,Γ⟧ := pr121 (R Γ A).

  Definition var : (Tm ext:hSet) := pr221 (R Γ A).

  Definition comm
    : pp ext var = functor_on_morphisms Ty π A
    := pr12 (R Γ A).

  Definition pullback
    : isPullback (cwf_square_comm pp comm)
    := pr2 (pr2 (R Γ A)).
End Projections.

Arguments iso _ _ _ : clear implicits.

Section CwF.
  Definition disp_cwf' : disp_bicat (morphisms_of_presheaves SET).
  Show proof.
    refine (disp_fullsubbicat (morphisms_of_presheaves SET) _).
    intros (C, ((Ty, Tm), pp)).
    cbn in *.
    exact (@cwf_representation C _ _ pp).

  Definition disp_cwf : disp_bicat bicat_of_univ_cats
    := sigma_bicat _ _ disp_cwf'.

  Definition disp_2cells_isaprop_disp_cwf
    : disp_2cells_isaprop disp_cwf.
  Show proof.
    apply disp_2cells_isaprop_sigma.
    - apply disp_2cells_isaprop_morphisms_of_presheaves_display.
    - apply disp_2cells_isaprop_fullsubbicat.

  Definition disp_locally_groupoid_disp_cwf
    : disp_locally_groupoid disp_cwf.
  Show proof.
    apply disp_locally_groupoid_sigma.
    - exact univalent_cat_is_univalent_2.
    - apply disp_2cells_isaprop_morphisms_of_presheaves_display.
    - apply disp_2cells_isaprop_fullsubbicat.
    - apply disp_locally_groupoid_morphisms_of_presheaves_display.
    - apply disp_locally_groupoid_fullsubbicat.

  Definition cwf : bicat
    := total_bicat disp_cwf.

  Lemma disp_univalent_2_1_morphisms_of_presheaf_display
    : disp_univalent_2_1 (morphisms_of_presheaves_display SET).
  Show proof.
    apply sigma_disp_univalent_2_1_with_props.
    - apply disp_2cells_isaprop_prod ; apply disp_2cells_isaprop_presheaf.
    - apply disp_2cells_isaprop_cofunctormaps.
    - apply disp_two_presheaves_is_univalent_2_1.
    - apply disp_cofunctormaps_bicat_univalent_2_1.

  Lemma disp_univalent_2_0_morphisms_of_presheaf_display
    : disp_univalent_2_0 (morphisms_of_presheaves_display SET).
  Show proof.
    apply sigma_disp_univalent_2_0_with_props.
    - exact univalent_cat_is_univalent_2.
    - apply disp_2cells_isaprop_prod ; apply disp_2cells_isaprop_presheaf.
    - apply disp_2cells_isaprop_cofunctormaps.
    - apply disp_two_presheaves_is_univalent_2_1.
    - apply disp_cofunctormaps_bicat_univalent_2_1.
    - apply disp_locally_groupoid_prod ; apply disp_locally_groupoid_presheaf.
    - apply disp_locally_groupoid_cofunctormaps.
    - apply disp_two_presheaves_is_univalent_2_0.
    - apply disp_cofunctormaps_bicat_univalent_2_0.

  Definition cwf_is_univalent_2_1
    : is_univalent_2_1 cwf.
  Show proof.
    apply sigma_is_univalent_2_1.
    - exact univalent_cat_is_univalent_2_1.
    - exact disp_univalent_2_1_morphisms_of_presheaf_display.
    - apply disp_fullsubbicat_univalent_2_1.

  Definition cwf_is_univalent_2_0
    : is_univalent_2_0 cwf.
  Show proof.
    apply sigma_is_univalent_2_0.
    - exact univalent_cat_is_univalent_2.
    - split.
      + exact disp_univalent_2_0_morphisms_of_presheaf_display.
      + exact disp_univalent_2_1_morphisms_of_presheaf_display.
    - split.
      + apply disp_univalent_2_0_fullsubbicat.
        * apply morphisms_of_presheaves_univalent_2.
        * intros C.
          apply isaprop_cwf_representation.
          apply (pr1 C).
      + apply disp_fullsubbicat_univalent_2_1.

  Definition cwf_is_univalent_2
    : is_univalent_2 cwf.
  Show proof.
    split.
    - exact cwf_is_univalent_2_0.
    - exact cwf_is_univalent_2_1.
End CwF.