Library UniMath.CategoryTheory.DisplayedCats.FunctorCategory

Functor category as a displayed category

Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.UnivalenceAxiom.
Require Import UniMath.MoreFoundations.Propositions.
Require Import UniMath.CategoryTheory.Categories.
Require Import UniMath.CategoryTheory.categories.HSET.Core.
Require Import UniMath.CategoryTheory.functor_categories.
Require Import UniMath.CategoryTheory.Monads.Monads.

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

Local Open Scope cat.
Local Open Scope mor_disp_scope.

Definition base_precategory_ob_mor (C D:precategory_data)
  : precategory_ob_mor
  := precategory_ob_mor_pair (C → D)
                             (λ F₀ G₀ : C → D, ∏ x : C, D ⟦ F₀ x, G₀ x ⟧).

Definition base_precategory_data (C D:precategory_data) : precategory_data
  := precategory_data_pair
       (base_precategory_ob_mor C D)
       (λ (F₀ : C → D) (x : C), identity (F₀ x))
       (λ (F₀ G₀ H₀ : C → D)
          (FG : ∏ x : C, D ⟦ F₀ x, G₀ x ⟧)
          (GH : ∏ x : C, D ⟦ G₀ x, H₀ x ⟧)
          (x : C),
        FG x · GH x).

Section FunctorsDisplayed.

Context (C D:category).

Base category.

The base category contains:
  • Objects: functions F₀ : C₀ → D₀
  • Morphisms: transformations γₓ : D₀ ⟦F₀ x, G₀ x⟧

Lemma is_precategory_base_precategory_data
  : is_precategory (base_precategory_data C D).
Proof.
  apply mk_is_precategory.
  - intros F₀ G₀. cbn. intros γ.
    apply funextsec. intros x.
    apply id_left.
  - intros F₀ G₀. cbn. intros γ.
    apply funextsec. intros x.
    apply id_right.
  - intros F₀ G₀ H₀ K₀. cbn. intros γ θ μ.
    apply funextsec. intros x.
    apply assoc.
  - intros F₀ G₀ H₀ K₀. cbn. intros γ θ μ.
    apply funextsec. intros x.
    apply assoc'.
Qed.

Definition base_precategory
  : precategory
  := precategory_pair (base_precategory_data C D)
                      is_precategory_base_precategory_data.

Lemma has_homsets_base_precategory_ob_mor
  : has_homsets (base_precategory_ob_mor C D).
Proof.
  intros F₀ G₀. cbn. apply (impred 2). intro. apply D.
Qed.

Definition base_category
  : category
  := category_pair base_precategory
                   has_homsets_base_precategory_ob_mor.

Step 1

  • Objects: actions of functors on maps
  • Morphisms: naturality of transformations
    The univalence of this displayed category can be expressed as a concrete case of the Structure Identity Principle.

Definition disp_morph : disp_cat_data (base_precategory_data C D).
Proof.
  use tpair.
  - ∃ (λ F₀, ∏ {a b : C}, C ⟦a, b⟧ → D ⟦F₀ a, F₀ b⟧).
    cbn. intros F₀ G₀ F₁ G₁ γ.
    exact (∏ (a b : C) (f : C ⟦a, b⟧), F₁ _ _ f · γ b = γ a · G₁ _ _ f).
  - repeat use tpair; cbn.
    + cbn; intros.
      etrans. apply id_right.
      apply pathsinv0. apply id_left.
    + cbn. intros ???????? S1 S2 a b f.
      etrans. apply assoc.
      etrans. apply cancel_postcomposition, S1.
      etrans. apply assoc'.
      etrans. apply cancel_precomposition, S2.
      apply assoc.
Defined.

Lemma step1_disp_axioms
  : disp_cat_axioms base_category disp_morph.
Proof.
  repeat split; intros; repeat (apply impred; intro);
    repeat (apply funextsec; intro); try apply homset_property.
  cbn.
  repeat (apply (impred 2); intro).
  apply hlevelntosn.
  apply homset_property.
Qed.

Definition step1_disp : disp_cat base_category.
Proof.
  ∃ disp_morph.
  exact step1_disp_axioms.
Defined.

Lemma step1_disp_univalent : is_univalent_disp step1_disp.
Proof.
  apply is_univalent_disp_from_fibers.
  hnf; cbn; intros x f g.
  apply isweqimplimpl.
  - intro i.
    unfold iso_disp in i.
    cbn in i.
    apply funextsec. intro.
    destruct i as (ff, Hff).
    apply funextsec. intro.
    apply funextsec. intro.
    etrans.
    { apply pathsinv0. apply id_right. }
    etrans.
    { apply ff. }
    apply id_left.
  - assert (KK : isaset (∏ a b : C, C ⟦ a, b ⟧ → D ⟦ x a, x b ⟧)).
    + repeat (apply (impred 2); intro).
      apply homset_property.
    + apply KK.
  - apply isaproptotal2.
    + unfold isPredicate.
      intro u.
      apply (isaprop_is_iso_disp (D := step1_disp)).
    + cbn.
      intros u v Hu Hv.
      apply funextsec. intro a.
      apply funextsec. intro b.
      apply funextsec. intro t.
      apply homset_property.
Defined.

Definition step1_total : category
  := total_category step1_disp.

Step 2

  • Objects: functors preserver identities
  • Morphisms: unit

Definition step2_disp : disp_cat step1_total :=
  disp_full_sub step1_total
  (λ F : step1_total,
    let F₁ := pr2 F in
    ∏ (x : C), F₁ _ _ (identity x) = identity _).

Step 3

  • Objects: functors preserver composition
  • Morphisms: unit

Definition step3_disp : disp_cat step1_total :=
  disp_full_sub step1_total
  (λ F : step1_total,
    let F₁ := pr2 F in
    ∏ (a b c: C) (f : C⟦a,b⟧) (g : C⟦b,c⟧),
    F₁ _ _ (f · g) = F₁ _ _ f · F₁ _ _ g).

Step 4

Combine everything together

Definition functor_disp_cat : disp_cat step1_total
  := dirprod_disp_cat step2_disp step3_disp.

Definition functor_total_cat : category
  := total_category functor_disp_cat.

This construction is univalent
Lemma functor_disp_cat_univalent :
  is_univalent_disp functor_disp_cat.
Proof.
  apply dirprod_disp_cat_is_univalent.
  - apply disp_full_sub_univalent.
    intros [F₀ F₁]. apply impred. intros x.
    cbn[pr2].
    apply homset_property.
  - apply disp_full_sub_univalent.
    intros [F₀ F₁].
    repeat (apply impred; intros ?).
    cbn[pr2].
    apply homset_property.
Defined.

Definition base_category_iso_to_iso_fam (F₀ G₀ : base_category) :
  iso F₀ G₀ → (∏ (x : C), iso (F₀ x) (G₀ x)).
Proof.
  intros [γ Hγ].
  apply is_z_iso_from_is_iso in Hγ.
  destruct Hγ as [θ [Hγθ Hθγ]].
  intros x. apply z_iso_to_iso.
  ∃ (γ x), (θ x). split.
  - apply (toforallpaths _ _ _ Hγθ).
  - apply (toforallpaths _ _ _ Hθγ).
Defined.

Definition base_category_iso_fam_to_iso (F₀ G₀ : base_category) :
  (∏ (x : C), iso (F₀ x) (G₀ x)) → iso F₀ G₀.
Proof.
  intros γ.
  apply z_iso_to_iso.
  ∃ γ, (λ x, inv_from_iso (γ x)).
  split.
  - apply funextsec. intros x. cbn.
    apply iso_inv_after_iso.
  - apply funextsec. intros x. cbn.
    apply iso_after_iso_inv.
Defined.

Lemma base_category_iso_weq (F₀ G₀ : base_category) :
  iso F₀ G₀ ≃ (∏ (x : C), iso (F₀ x) (G₀ x)).
Proof.
  ∃ (base_category_iso_to_iso_fam F₀ G₀).
  use gradth.
  - apply base_category_iso_fam_to_iso.
  - intros x. apply eq_iso. reflexivity.
  - intros x. apply funextsec. intros y.
    apply eq_iso. reflexivity.
Defined.

Definition base_category_iso_fam_weq (F₀ G₀ : base_category) :
  is_univalent D →
  F₀ ¬ G₀ ≃ (∏ (x : C), iso (F₀ x) (G₀ x)).
Proof.
  intros HD.
  apply weqonsecfibers. intros x.
  ∃ idtoiso. apply HD.
Defined.

Definition base_category_iso_weq_aux
      (F₀ G₀ : base_category) :
  is_univalent D →
  F₀ = G₀ ≃ iso F₀ G₀.
Proof.
  intros HD.
  eapply weqcomp. apply weqtoforallpaths.
  eapply weqcomp. apply base_category_iso_fam_weq, HD.
  apply invweq. apply base_category_iso_weq.
Defined.

Lemma base_category_univalent
  : is_univalent D → is_univalent base_category.
Proof.
  intros HD.
  unfold is_univalent. split; [ | apply base_category ].
  unfold base_category. simpl.
  intros F₀ G₀.
  use isweqhomot.
  - apply base_category_iso_weq_aux, HD.
  - intros p. induction p. simpl.
    apply eq_iso. reflexivity.
  - apply base_category_iso_weq_aux.
Defined.

Lemma functor_total_cat_univalent
  : is_univalent D → is_univalent functor_total_cat.
Proof.
  intros HD.
  apply is_univalent_total_category.
  - apply is_univalent_total_category.
    + apply base_category_univalent, HD.
    + apply step1_disp_univalent.
  - apply functor_disp_cat_univalent.
Defined.

End FunctorsDisplayed.