Library UniMath.CategoryTheory.DisplayedCats.Functors


Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.PartA.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.Isos.

Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Isos.

Local Open Scope cat.

Functors over functors between bases

One could define these in terms of functor-liftings, as:

Definition disp_functor {C C' : category} (F : functor C C')
    (D : disp_cat C) (D' : disp_cat C')
  := functor_lifting D' (functor_composite (pr1_category D) F).
However, it seems like it may probably be cleaner to define these independently.
TODO: reassess this design decision after some experience using it!

Section Disp_Functor.

  Definition disp_functor_data {C' C : precategory_data} (F : functor_data C' C)
             (D' : disp_cat_data C') (D : disp_cat_data C)
    := ∑ (Fob : ∏ x, D' x -> D (F x)),
      ∏ x y (xx : D' x) (yy : D' y) (f : x --> y),
      (xx -->[f] yy) -> (Fob _ xx -->[ # F f ] Fob _ yy).

  Definition disp_functor_on_objects {C' C : precategory_data} {F : functor_data C' C}
             {D' : disp_cat_data C'} {D : disp_cat_data C}
             (FF : disp_functor_data F D' D) {x : C'} (xx : D' x)
    : D (F x)
    := pr1 FF x xx.

  Coercion disp_functor_on_objects : disp_functor_data >-> Funclass.

Unfortunately, the coercion loses implicitness of the {x:C'} argument: we have to write FF _ xx instead of just FF xx .
If anyone knows a way to avoid this, we would be happy to hear it!

  Definition disp_functor_on_morphisms {C' C : precategory_data} {F : functor_data C' C}
             {D' : disp_cat_data C'} {D : disp_cat_data C}
             (FF : disp_functor_data F D' D)
             {x y : C'} {xx : D' x} {yy} {f : x --> y} (ff : xx -->[f] yy)
    : (FF _ xx) -->[ # F f ] (FF _ yy)
    := pr2 FF x y xx yy f ff.

  Local Open Scope mor_disp_scope.
  Notation "♯ F" := (disp_functor_on_morphisms F)
                      (at level 3) : mor_disp_scope.

  Definition disp_functor_axioms {C' C : category} {F : functor C' C}
             {D' : disp_cat C'} {D : disp_cat C} (FF : disp_functor_data F D' D)
    := (∏ x (xx : D' x),
          ♯ FF (id_disp xx) = transportb _ (functor_id F x) (id_disp (FF _ xx)))
          × (∏ x y z (xx : D' x) yy zz (f : x --> y) (g : y --> z)
               (ff : xx -->[f] yy) (gg : yy -->[g] zz),
              ♯ FF (ff ;; gg)
              = transportb _ (functor_comp F f g) (♯ FF ff ;; ♯ FF gg)).

  Lemma isaprop_disp_functor_axioms {C' C : category} {F : functor C' C}
        {D' : disp_cat C'} {D : disp_cat C} (FF : disp_functor_data F D' D)
    : isaprop (disp_functor_axioms FF).
  Show proof.
    apply isapropdirprod;
      repeat (apply impred; intros);
      apply homsets_disp.

  Definition disp_functor {C' C : category} (F : functor C' C)
             (D' : disp_cat C') (D : disp_cat C)
    := ∑ FF : disp_functor_data F D' D, disp_functor_axioms FF.

  Definition disp_functor_data_from_disp_functor
             {C' C} {F} {D' : disp_cat C'} {D : disp_cat C}
             (FF : disp_functor F D' D)
    : disp_functor_data F D' D
    := pr1 FF.

  Coercion disp_functor_data_from_disp_functor
    : disp_functor >-> disp_functor_data.

  Definition disp_functor_id {C' C} {F} {D' : disp_cat C'} {D : disp_cat C}
             (FF : disp_functor F D' D)
             {x} (xx : D' x)
    : ♯ FF (id_disp xx) = transportb _ (functor_id F x) (id_disp (FF _ xx))
    := pr1 (pr2 FF) x xx.

  Proposition disp_functor_id_var
              {C₁ C₂ : category}
              {F : C₁ ⟶ C₂}
              {D₁ : disp_cat C₁}
              {D₂ : disp_cat C₂}
              (FF : disp_functor F D₁ D₂)
              {x : C₁}
              (xx : D₁ x)
    : id_disp (FF x xx)
      =
      transportf
        (λ z, _ -->[ z ] _)
        (functor_id F x)
        (♯ FF (id_disp xx)).
  Show proof.
    rewrite disp_functor_id.
    rewrite transportfbinv.
    apply idpath.

  Definition disp_functor_comp {C' C} {F} {D' : disp_cat C'} {D : disp_cat C}
             (FF : disp_functor F D' D)
             {x y z} {xx : D' x} {yy} {zz} {f : x --> y} {g : y --> z}
             (ff : xx -->[f] yy) (gg : yy -->[g] zz)
    : ♯ FF (ff ;; gg)
      = transportb _ (functor_comp F f g) (♯ FF ff ;; ♯ FF gg)
    := pr2 (pr2 FF) _ _ _ _ _ _ _ _ ff gg.

variant access function
  Definition disp_functor_comp_var {C' C} {F} {D' : disp_cat C'} {D : disp_cat C}
             (FF : disp_functor F D' D)
             {x y z} {xx : D' x} {yy} {zz} {f : x --> y} {g : y --> z}
             (ff : xx -->[f] yy) (gg : yy -->[g] zz)
    : transportf _ (functor_comp F f g) (♯ FF (ff ;; gg))
      = ♯ FF ff ;; ♯ FF gg.
  Show proof.
    apply transportf_pathsinv0.
    apply pathsinv0, disp_functor_comp.

Useful transport lemma for disp_functor.

 Lemma disp_functor_eq {C C':category} {F: functor C C'} {D:disp_cat C} {D':disp_cat C'}
 (DF DF': disp_functor F D D')
  : pr1 DF = pr1 DF' -> DF = DF'.
 Show proof.
  intro H.
  apply (total2_paths_f H).
  apply proofirrelevance.
  apply isaprop_disp_functor_axioms.

  Lemma disp_functor_transportf {C' C : category}
        {D' : disp_cat C'} {D : disp_cat C}
        (F : functor C' C) (FF : disp_functor F D' D)
        (x' x : C') (f' f : x' --> x) (p : f' = f)
        (xx' : D' x') (xx : D' x)
        (ff : xx' -->[ f' ] xx)
    :
    ♯ FF (transportf _ p ff)
    =
      transportf _ (maponpaths (# F) p) (♯FF ff).
  Show proof.
    induction p.
    apply idpath.

Composite and identity functors.


  Definition disp_functor_composite_data
             {C C' C'' : category} {D} {D'} {D''}
             {F : functor C C'} {F' : functor C' C''}
             (FF : disp_functor F D D')
             (FF' : disp_functor F' D' D'')
    : disp_functor_data (functor_composite F F') D D''.
  Show proof.
    use tpair.
    + intros x xx. exact (FF' _ (FF _ xx)).
    + intros x y xx yy f ff. exact (♯ FF' (♯ FF ff)).

  Lemma disp_functor_composite_axioms
        {C C' C'' : category} {D} {D'} {D''}
        {F : functor C C'} {F' : functor C' C''}
        (FF : disp_functor F D D')
        (FF' : disp_functor F' D' D'')
    : disp_functor_axioms (disp_functor_composite_data FF FF').
  Show proof.
    split; simpl.
    + intros x xx.
      etrans. apply maponpaths. apply disp_functor_id.
      etrans. apply disp_functor_transportf.
      etrans. apply maponpaths. apply disp_functor_id.
      etrans. apply transport_f_f.
      unfold transportb.
      apply maponpaths_2, homset_property.
    + intros.
      etrans. apply maponpaths. apply disp_functor_comp.
      etrans. apply disp_functor_transportf.
      etrans. apply maponpaths. apply disp_functor_comp.
      etrans. apply transport_f_f.
      unfold transportb.
      apply maponpaths_2, homset_property.

  Definition disp_functor_composite
             {C C' C'' : category} {D} {D'} {D''}
             {F : functor C C'} {F' : functor C' C''}
             (FF : disp_functor F D D')
             (FF' : disp_functor F' D' D'')
    : disp_functor (functor_composite F F') D D''.
  Show proof.
    use tpair.
    - apply (disp_functor_composite_data FF FF').
    - apply disp_functor_composite_axioms.

  Definition disp_functor_identity
             {C : category} (D : disp_cat C)
    : disp_functor (functor_identity _ ) D D.
  Show proof.
    use tpair.
    - use tpair.
      + intros; assumption.
      + cbn. intros. assumption.
    - split; simpl.
      + intros; apply idpath.
      + intros; apply idpath.

Action of functors on z_isos.

  Section Functors_on_z_isos.


    Lemma disp_functor_on_z_iso_disp_aux1 {C C'} {F}
          {D : disp_cat C} {D' : disp_cat C'}
          (FF : disp_functor F D D')
          {x y} {xx : D x} {yy} {f : z_iso x y}
          (ff : xx -->[f] yy)
          (Hff : is_z_iso_disp f ff)
      : transportf _ (functor_on_inv_from_z_iso F f)
                   (♯ FF (inv_mor_disp_from_z_iso Hff))
        ;; ♯ FF ff
        = transportb _ (z_iso_after_z_iso_inv _) (id_disp _).
    Show proof.
      etrans. apply mor_disp_transportf_postwhisker.
      etrans. apply maponpaths, @pathsinv0, disp_functor_comp_var.
      etrans. apply transport_f_f.
      etrans. apply maponpaths, maponpaths, z_iso_disp_after_inv_mor.
      etrans. apply maponpaths, disp_functor_transportf.
      etrans. apply transport_f_f.
      etrans. apply maponpaths, disp_functor_id.
      etrans. apply transport_f_b.
      unfold transportb. apply maponpaths_2, homset_property.

    Lemma disp_functor_on_z_iso_disp_aux2 {C C'} {F}
          {D : disp_cat C} {D' : disp_cat C'}
          (FF : disp_functor F D D')
          {x y} {xx : D x} {yy} {f : z_iso x y}
          (ff : xx -->[f] yy)
          (Hff : is_z_iso_disp f ff)
      : ♯ FF ff
        ;; transportf _ (functor_on_inv_from_z_iso F f)
                      (♯ FF (inv_mor_disp_from_z_iso Hff))
        =
          transportb _ (z_iso_inv_after_z_iso (functor_on_z_iso _ _)) (id_disp (FF x xx)).
    Show proof.
      etrans. apply mor_disp_transportf_prewhisker.
      etrans. apply maponpaths, @pathsinv0, disp_functor_comp_var.
      etrans. apply transport_f_f.
      etrans. apply maponpaths, maponpaths, inv_mor_after_z_iso_disp.
      etrans. apply maponpaths, disp_functor_transportf.
      etrans. apply transport_f_f.
      etrans. apply maponpaths, disp_functor_id.
      etrans. apply transport_f_f.
      unfold transportb. apply maponpaths_2, homset_property.

Let's see how disp_functors behave on z_iso_disps TODO: consider naming
    Definition disp_functor_on_is_z_iso_disp {C C'} {F}
               {D : disp_cat C} {D' : disp_cat C'}
               (FF : disp_functor F D D')
               {x y} {xx : D x} {yy} {f : z_iso x y}
               {ff : xx -->[f] yy} (Hff : is_z_iso_disp f ff)
      : is_z_iso_disp (functor_on_z_iso F f) (♯ FF ff).
    Show proof.
      exists (transportf _ (functor_on_inv_from_z_iso F f)
                    (♯ FF (inv_mor_disp_from_z_iso Hff))); split.
      - apply disp_functor_on_z_iso_disp_aux1.
      - apply disp_functor_on_z_iso_disp_aux2.

    Definition disp_functor_on_z_iso_disp {C C'} {F}
               {D : disp_cat C} {D' : disp_cat C'}
               (FF : disp_functor F D D')
               {x y} {xx : D x} {yy} {f : z_iso x y}
               (ff : z_iso_disp f xx yy)
      : z_iso_disp (functor_on_z_iso F f) (FF _ xx) (FF _ yy)
      := (_ ,, disp_functor_on_is_z_iso_disp _ ff).

  End Functors_on_z_isos.

Properties of functors


  Section Functor_Properties.

    Definition disp_functor_ff {C C'} {F}
               {D : disp_cat C} {D' : disp_cat C'} (FF : disp_functor F D D')
      :=
      ∏ x y (xx : D x) (yy : D y) (f : x --> y),
        isweq (fun ff : xx -->[f] yy => ♯ FF ff).

    Proposition isaprop_disp_functor_ff
                {C₁ C₂ : category}
                {F : C₁ ⟶ C₂}
                {D₁ : disp_cat C₁}
                {D₂ : disp_cat C₂}
                (FF : disp_functor F D₁ D₂)
      : isaprop (disp_functor_ff FF).
    Show proof.
      do 5 (use impred ; intro).
      apply isapropisweq.

    Section ff_reflects_isos.

      Context {C C' : category}
              {F : functor C C'}
              {D : disp_cat C}
              {D' : disp_cat C'}
              (FF : disp_functor F D D')
              (FF_ff : disp_functor_ff FF).

      Definition disp_functor_ff_weq {x y} xx yy f
        := make_weq _ (FF_ff x y xx yy f).
      Definition disp_functor_ff_inv {x y} {xx} {yy} {f : x --> y}
        := invmap (disp_functor_ff_weq xx yy f).

      Lemma disp_functor_ff_inv_transportf
            {x y : C} {f f' : x --> y} (e : f = f')
            {xx : D x} {yy : D y} (ff : FF _ xx -->[#F f] FF _ yy)
        : disp_functor_ff_inv (transportf _ (maponpaths (# F) e) ff)
          =
            transportf _ e (disp_functor_ff_inv ff).
      Show proof.
        induction e.
        apply idpath.

      Lemma disp_functor_ff_inv_identity {x : C} (xx : D x)
        : disp_functor_ff_inv (transportb _ (functor_id F _ ) (id_disp (FF _ xx)))
          = id_disp xx.
      Show proof.
        apply invmap_eq.
        apply pathsinv0.
        apply (disp_functor_id FF).

      Lemma disp_functor_ff_inv_compose {x y z : C} {f : x --> y} {g : y --> z}
            {xx} {yy} {zz}
            (ff : FF _ xx -->[#F f] FF _ yy) (gg : FF _ yy -->[#F g] FF _ zz)
        : disp_functor_ff_inv (transportb _ (functor_comp F _ _ ) (ff ;; gg))
          = disp_functor_ff_inv ff ;; disp_functor_ff_inv gg.
      Show proof.
        apply invmap_eq. cbn.
        apply pathsinv0.
        etrans. apply (disp_functor_comp FF).
        apply maponpaths.
        etrans. apply maponpaths. exact (homotweqinvweq _ _).
        apply maponpaths_2. exact (homotweqinvweq _ _).

      Definition disp_functor_ff_reflects_isos
                 {x y} {xx : D x} {yy : D y} {f : z_iso x y}
                 (ff : xx -->[f] yy) (isiso: is_z_iso_disp (functor_on_z_iso F f) (♯ FF ff))
        : is_z_iso_disp _ ff.
      Show proof.
        set (FFffinv := inv_mor_disp_from_z_iso isiso).
        set (FFffinv' := transportb _ (functor_on_inv_from_z_iso _ _ ) FFffinv).
        set (ffinv := disp_functor_ff_inv FFffinv').
        exists ffinv.
        split.
        - unfold ffinv. unfold FFffinv'.
          admit.
        - admit.
      Abort.

    End ff_reflects_isos.

    Proposition FF_disp_functor_ff_inv
                {C₁ C₂ : category}
                {F : C₁ ⟶ C₂}
                {D₁ : disp_cat C₁}
                {D₂ : disp_cat C₂}
                {FF : disp_functor F D₁ D₂}
                (HFF : disp_functor_ff FF)
                {x y : C₁}
                {f : x --> y}
                {xx : D₁ x}
                {yy : D₁ y}
                (ff : FF x xx -->[ (#F f)%Cat ] FF y yy)
      : ♯FF (disp_functor_ff_inv FF HFF ff) = ff.
    Proof.
      apply (homotweqinvweq ((disp_functor_ff_weq FF HFF xx yy f))).

Given a base functor F : C —> C' and a displayed functor FF : D' -> D over it, there are two different “essential surjectivity” conditions one can put on FF.
Given c : C and d : D' (F c), one can ask for a lift of d either in D c itself, or more generally in some fiber D c' with c' isomorphic to c.
The second version is better-behaved in general; but the stricter first version is equivalent when D is an isofibration, and is simpler to work with. So we call the second version “essentially split surjective”, disp_functor_ess_split_surj, and the first “displayed ess. split surj.”, disp_functor_disp_ess_split_surj.

    Definition disp_functor_ess_split_surj {C' C} {F}
               {D' : disp_cat C'} {D : disp_cat C} (FF : disp_functor F D D')
      : UU
      :=
      ∏ x (xx : D' (F x)),
        ∑ y : C,
          ∑ i : z_iso y x,
            ∑ yy : D y,
              z_iso_disp (functor_on_z_iso F i) (FF _ yy) xx.

    Definition disp_functor_disp_ess_split_surj {C' C} {F}
               {D' : disp_cat C'} {D : disp_cat C} (FF : disp_functor F D D')
      : UU
      :=
      ∏ x (xx : D' (F x)),
        ∑ (yy : D x),
        z_iso_disp (identity_z_iso _) (FF _ yy) xx.


    Definition disp_functor_disp_ess_surj
               {C₁ C₂ : category}
               {F : C₁ ⟶ C₂}
               {D₁ : disp_cat C₁}
               {D₂ : disp_cat C₂}
               (FF : disp_functor F D₁ D₂)
      : hProp
      := ∀ (x : C₁)
           (yy : D₂ (F x)),
         ∃ (xx : D₁ x),
         z_iso_disp
           (identity_z_iso _)
           (FF x xx)
           yy.

  End Functor_Properties.
End Disp_Functor.


Local Open Scope mor_disp_scope.
Notation "♯ F" := (disp_functor_on_morphisms F)
                    (at level 3) : mor_disp_scope.

#[deprecated(note="Use '♯' (input: \# or \sharp) instead.")]
Notation "# F" := ♯ F (only parsing) : mor_disp_scope.

Operations on displayed functors/transformations over the identity
Section CompDispFunctorOverIdentity.
  Context {C : category}
          {D₁ D₂ D₃ : disp_cat C}
          (FF : disp_functor (functor_identity C) D₁ D₂)
          (GG : disp_functor (functor_identity C) D₂ D₃).

  Definition disp_functor_over_id_composite_data
    : disp_functor_data (functor_identity C) D₁ D₃.
  Show proof.
    simple refine (_ ,, _).
    - exact (λ x xx, GG x (FF x xx)).
    - exact (λ x y xx yy f ff, (♯GG (♯FF ff))).

  Definition disp_functor_over_id_composite_axioms
    : disp_functor_axioms disp_functor_over_id_composite_data.
  Show proof.
    split.
    - intros x xx ; cbn.
      rewrite (disp_functor_id FF) ; cbn.
      rewrite (disp_functor_id GG) ; cbn.
      apply idpath.
    - intros x y z xx yy zz f g ff gg ; cbn.
      etrans.
      {
        apply maponpaths.
        exact (disp_functor_comp FF ff gg).
      }
      cbn.
      exact (disp_functor_comp GG (♯ FF ff) (♯ FF gg)).

  Definition disp_functor_over_id_composite
    : disp_functor (functor_identity C) D₁ D₃.
  Show proof.
    simple refine (_ ,, _).
    - exact disp_functor_over_id_composite_data.
    - exact disp_functor_over_id_composite_axioms.
End CompDispFunctorOverIdentity.

Various lemmas
Proposition pr1_idtoiso_disp_functor
            {C₁ C₂ : category}
            {F : C₁ ⟶ C₂}
            {D₁ : disp_cat C₁}
            {D₂ : disp_cat C₂}
            (FF : disp_functor F D₁ D₂)
            {x : C₁}
            {xx yy : D₁ x}
            (p : xx = yy)
  : pr1 (idtoiso_disp (idpath (F x)) (maponpaths (FF x) p))
    =
    transportf
      (λ z, _ -->[ z ] _)
      (functor_id F _)
      (♯FF (idtoiso_disp (idpath x) p)).
Show proof.
  induction p.
  cbn.
  rewrite disp_functor_id.
  rewrite transportfbinv.
  apply idpath.