Library TypeTheory.Displayed_Cats.Equivalences_bis

“Displayed equivalences” of displayed (pre)categories

Require Import UniMath.Foundations.Sets.
Require Import UniMath.CategoryTheory.Categories.
Require Import UniMath.CategoryTheory.Adjunctions.
Require Import UniMath.CategoryTheory.equivalences.

Require Import TypeTheory.Auxiliary.Auxiliary.
Require Import TypeTheory.Auxiliary.UnicodeNotations.
Require Import TypeTheory.Displayed_Cats.Auxiliary.
Require Import TypeTheory.Displayed_Cats.Core.
Require Import TypeTheory.Displayed_Cats.Constructions.
Require Import TypeTheory.Displayed_Cats.Fibrations.

Local Set Automatic Introduction.

Local Open Scope type_scope.
Local Open Scope mor_disp_scope.

Section Auxiliary.

End Auxiliary.

Section Essential_Surjectivity.

Definition fiber_functor_ess_split_surj
    {C C' : category} {D} {D'}
    {F : functor C C'} (FF : disp_functor F D D')
    (H : disp_functor_ff FF)
    {X : disp_functor_ess_split_surj FF}
    {Y : is_op_isofibration D}

    (x : C)
  : ∏ yy : D'[{F x }], ∑ xx : D [{x }],
                iso (fiber_functor FF _ xx) yy.
Proof.
  intro yy.
  set (XR := X _ yy).
  destruct XR as [c'' [i [xx' ii]]].
  set (YY := Y _ _ i xx').
  destruct YY as [ dd pe ].
  mkpair.
  - apply dd.
  -

    set (XR := disp_functor_on_iso_disp FF pe).
    set (XR' := iso_inv_from_iso_disp XR).
    apply (invweq (iso_disp_iso_fiber _ _ _ _)).
    set (XRt := iso_disp_comp XR' ii).
    transparent assert (XH :
           (iso_comp (iso_inv_from_iso (functor_on_iso F i))
             (functor_on_iso F i) = identity_iso _ )).
    { apply eq_iso. cbn. simpl. unfold precomp_with.
      etrans. apply maponpaths_2. apply id_right.
      etrans. eapply pathsinv0. apply functor_comp.
      etrans. Focus 2. apply functor_id.
      apply maponpaths. apply iso_after_iso_inv.
   }
    set (XRT := transportf (fun r => iso_disp r (FF x dd) yy )
                           XH).
    apply XRT.
    assumption.
Defined.

End Essential_Surjectivity.

General definition of displayed adjunctions and equivalences

Section adjunction.

Definition adjunction (A B : precategory) : UU
  := ∑ X : adjunction_data A B, form_adjunction' X.
Coercion data_from_adjunction {A B} (X : adjunction A B)
  : adjunction_data _ _ := pr1 X.
Coercion are_adjoints_from_adjunction {A B} (X : adjunction A B)
  : are_adjoints (left_functor X) (right_functor X).
Proof.
  exists (adjunit X,,adjcounit X).
  exists (pr1 (pr2 X)).
  exact (pr2 (pr2 X)).
Defined.

Definition adjunitiso {A B : precategory} (X : equivalence_of_precats A B)
           (a : A) : iso a (right_functor X (left_functor X a)).
Proof.
  use isopair.
  - exact (adjunit X a).
  - exact (pr1 (pr2 X) a).
Defined.
Definition adjcounitiso {A B : precategory} (X : equivalence_of_precats A B)
           (b : B) : iso (left_functor X (right_functor X b)) b.
Proof.
  use isopair.
  - exact (adjcounit X b).
  - exact (pr2 (pr2 X) b).
Defined.

Definition adj_equiv (A B : precategory) : UU
:= ∑ F : functor A B, adj_equivalence_of_precats F.

Coercion left_adjequiv (A B : precategory) (F : adj_equiv A B)
: functor A B := pr1 F.

Coercion adj_equiv_of_precats_from_adj {A B : precategory} (E : adj_equiv A B)
  : adj_equivalence_of_precats E := pr2 E.

Coercion adj_from_adj_equiv {A B} (F : adj_equiv A B) : adjunction A B.
Proof.
  mkpair.
  - mkpair.
    + exact (pr1 F).
    + exists (right_adjoint F).
      exists (adjunit F).
      exact (adjcounit F).
  - exists (triangle_id_left_ad (pr2 (pr1 (pr2 F)))).
    exact (triangle_id_right_ad (pr2 (pr1 (pr2 F)))).
Defined.

Coercion equiv_from_adj_equiv {A B} (F : adj_equiv A B) : equivalence_of_precats A B.
Proof.
  mkpair.
  - exact F.
  - exists (pr1 (pr2 (pr2 F))).
    exact (pr2 (pr2 (pr2 F))).
Defined.
End adjunction.

Main definitions

Adjunctions

Section Adjunctions.

In general, one can define displayed equivalences/adjunctions over any equivalences/adjunctions between the bases (and probably more generally still). For now we just give the case over a single base precategory — i.e. over an identity functor.

We give the “bidirectional” version first, and then the “handed” versions afterwards, with enough coercions between the two to (hopefully) make it easy to work with both versions.

Definition disp_adjunction_data {C C' : category} (A : adjunction_data C C')
           (F := left_functor A) (G := right_functor A)
           (eta := adjunit A) (eps := adjcounit A)
           (D : disp_cat C) (D' : disp_cat C') : UU
  := ∑ (FF : disp_functor F D D') (GG : disp_functor G D' D),
     (disp_nat_trans eta (disp_functor_identity _ )
                     (disp_functor_composite FF GG))
       ×
       (disp_nat_trans eps (disp_functor_composite GG FF) (disp_functor_identity _ )).

Section notation.

Context {C C' : category} {A : adjunction_data C C'}
        {D D'} (X : disp_adjunction_data A D D').
Definition left_adj_over : disp_functor _ _ _ := pr1 X.
Definition right_adj_over : disp_functor _ _ _ := pr1 (pr2 X).
Definition unit_over : disp_nat_trans _ _ _ := pr1 (pr2 (pr2 X)).
Definition counit_over : disp_nat_trans _ _ _ := pr2 (pr2 (pr2 X)).

End notation.

Triangle identies for an adjunction

Note: the statements of these axioms include _statement_ to distinguish them from the instances of these statements given by the access functions of form_adjunction.

This roughly follows the pattern of univalenceStatement, funextfunStatement, etc., but departs from it slightly to follow our more general convention of using underscores instead of camelcase.

Definition triangle_1_statement_over
           {C C' : category} {A : adjunction C C'}
           {D D'} (X : disp_adjunction_data A D D')
           (FF := left_adj_over X)
           (ηη := unit_over X)
           (εε := counit_over X) : UU
  := ∏ x xx, #FF (ηη x xx) ;; εε _ (FF _ xx)
             = transportb _ (triangle_id_left_ad A x ) (id_disp _) .

Definition triangle_2_statement_over
           {C C' : category} {A : adjunction C C'}
           {D D'} (AA : disp_adjunction_data A D D')
           (GG := right_adj_over AA)
           (ηη := unit_over AA)
           (εε := counit_over AA) : UU
  := ∏ x xx, ηη _ (GG x xx) ;; # GG (εε _ xx)
           = transportb _ (triangle_id_right_ad A _ ) (id_disp _).

Definition form_disp_adjunction {C C' : category}
           (A : adjunction C C') {D : disp_cat C} {D' : disp_cat C'}
           (AA : disp_adjunction_data A D D')
  : UU
:= triangle_1_statement_over AA × triangle_2_statement_over AA.

Definition disp_adjunction {C C' : category} (A : adjunction C C') D D' : UU
  := ∑ AA : disp_adjunction_data A D D',
           triangle_1_statement_over AA × triangle_2_statement_over AA.

Coercion data_of_disp_adjunction (C C' : category) (A : adjunction C C')
         D D' (AA : disp_adjunction A D D') : disp_adjunction_data _ _ _ := pr1 AA.

Definition triangle_1_over {C C' : category}
           {A : adjunction C C'} {D : disp_cat C}
           {D' : disp_cat C'} (AA : disp_adjunction A D D')
: triangle_1_statement_over AA
:= pr1 (pr2 AA).

Definition triangle_2_over {C C' : category}
           {A : adjunction C C'} {D : disp_cat C}
           {D' : disp_cat C'} (AA : disp_adjunction A D D')
: triangle_2_statement_over AA
:= pr2 (pr2 AA).

The “left-handed” version: right adjoints to a given functor

The terminology is difficult to choose here: the proposition “F is a left adjoint” is the same as the type of “right adjoints to F”, so should this type be called something more like left_adjoint F or right_adjoint F?

Our choice here does not agree with that of the base UniMath category theory library. TODO: consider these conventions, and eventually harmonise them by changing it either here or in UniMath.

Definition right_adjoint_over_data {C C' : category}
           {A : adjunction_data C C'} {D : disp_cat C} {D' : disp_cat C'}
  (FF : disp_functor (left_functor A) D D') : UU
:= ∑ (GG : disp_functor (right_functor A) D' D),
     (disp_nat_trans (adjunit A)
            (disp_functor_identity _) (disp_functor_composite FF GG))
   × (disp_nat_trans (adjcounit A )
            (disp_functor_composite GG FF) (disp_functor_identity _)).

Definition functor_of_right_adjoint_over {C C' : category}
           {A : adjunction_data C C'} {D : disp_cat C} {D' : disp_cat C'}
           {FF : disp_functor (left_functor A) D D'}
  (GG : right_adjoint_over_data FF)
:= pr1 GG.
Coercion functor_of_right_adjoint_over
  : right_adjoint_over_data >-> disp_functor.

Definition adjunction_of_right_adjoint_over_data {C C' : category}
           {A : adjunction_data C C'} {D : disp_cat C} {D' : disp_cat C'}
           {FF : disp_functor (left_functor A) D D'}
  (GG : right_adjoint_over_data FF)
  : disp_adjunction_data A D D'
:= (FF,, GG).
Coercion adjunction_of_right_adjoint_over_data
  : right_adjoint_over_data >-> disp_adjunction_data.

Definition right_adjoint_of_disp_adjunction_data
           {C C' : category} {A : adjunction_data C C'}
           {D : disp_cat C} {D' : disp_cat C'}
           (AA : disp_adjunction_data A D D')
  : right_adjoint_over_data (left_adj_over AA)
:= pr2 AA.

Definition right_adjoint_over
           {C C' : category} {A : adjunction C C'}
           {D : disp_cat C} {D' : disp_cat C'}
           (FF : disp_functor (left_functor A) D D') : UU
:= ∑ GG : right_adjoint_over_data FF,
   form_disp_adjunction A GG.

Definition data_of_right_adjoint_over
                      {C C' : category} {A : adjunction C C'}
                      {D : disp_cat C} {D' : disp_cat C'}
  {FF : disp_functor (left_functor A) D D'}
  (GG : right_adjoint_over FF)
:= pr1 GG.
Coercion data_of_right_adjoint_over
  : right_adjoint_over >-> right_adjoint_over_data.

Definition adjunction_of_right_adjoint_over {C C' : category}
           {A : adjunction C C'} {D : disp_cat C} {D' : disp_cat C'}
           (FF : disp_functor (left_functor A) D D')
           (GG : right_adjoint_over FF)
: disp_adjunction A D D'
:= (adjunction_of_right_adjoint_over_data GG ,, pr2 GG).

Definition right_adjoint_of_disp_adjunction {C C' : category}
           {A : adjunction C C'} {D : disp_cat C} {D' : disp_cat C'}
           (AA : disp_adjunction A D D')
: right_adjoint_over (left_adj_over AA)
:= (right_adjoint_of_disp_adjunction_data AA ,, pr2 AA).

End Adjunctions.

Section Equivalences.

Equivalences (adjoint and quasi)

Definition form_equiv_over {C C' : category} {E : equivalence_of_precats C C'}
           {D : disp_cat C} {D' : disp_cat C'}
           (AA : disp_adjunction_data E D D') : UU
  := (∏ x xx, is_iso_disp (adjunitiso E x) (unit_over AA x xx))
     ×
     (∏ x xx, is_iso_disp (adjcounitiso E x) (counit_over AA x xx)).

Definition is_iso_unit_over
           {C C' : category} (E : equivalence_of_precats C C') {D D'}
           (AA : disp_adjunction_data E D D')
           (EE : form_equiv_over AA)
: ∏ (x : C) (xx : D x), is_iso_disp (adjunitiso E x) ((unit_over AA) x xx)
:= pr1 EE.

Definition is_iso_counit_over
           {C C' : category} (E : equivalence_of_precats C C') {D D'}
           (AA : disp_adjunction_data E D D')
           (EE : form_equiv_over AA)
: ∏ (x0 : C') (xx : D' x0), is_iso_disp (adjcounitiso E x0) ((counit_over AA) x0 xx)
:= pr2 EE.

Definition equiv_over {C C' : category} (E : adj_equiv C C')
           (D : disp_cat C) (D' : disp_cat C')
         : UU
:= ∑ AA : disp_adjunction E D D', @form_equiv_over _ _ E _ _ (pr1 AA).

Coercion adjunction_of_equiv_over {C C' : category} (E : adj_equiv C C')
          {D : disp_cat C} {D': disp_cat C'} (EE : equiv_over E D D')
: disp_adjunction _ _ _ := pr1 EE.

Coercion axioms_of_equiv_over {C C' : category} (E : adj_equiv C C')
            {D : disp_cat C} {D': disp_cat C'}
            (EE : equiv_over E D D') : form_equiv_over _
:= pr2 EE.

Definition is_equiv_over {C C' : category} (E : adj_equiv C C')
           {D : disp_cat C} {D': disp_cat C'}
           (FF : disp_functor (left_functor E) D D') : UU
  := ∑ GG : @right_adjoint_over _ _ E _ _ FF,
            @form_equiv_over _ _ E _ _ GG.

Definition right_adjoint_of_is_equiv_over {C C' : category} (E : adj_equiv C C')
           {D : disp_cat C} {D': disp_cat C'}
           {FF : disp_functor (left_functor E) D D'}
           (EE : is_equiv_over E FF) := pr1 EE.
Coercion right_adjoint_of_is_equiv_over
  : is_equiv_over >-> right_adjoint_over.

Definition equiv_of_is_equiv_over {C C' : category} (E : adj_equiv C C')
           {D : disp_cat C} {D': disp_cat C'}
           {FF : disp_functor (left_functor E) D D'}
           (EE : is_equiv_over E FF)
: equiv_over E D D'
:= (adjunction_of_right_adjoint_over _ EE ,, pr2 EE).
Coercion equiv_of_is_equiv_over
  : is_equiv_over >-> equiv_over.

Lemmas on the triangle identities

Local Open Scope hide_transport_scope.

Lemma triangle_2_from_1_for_equiv_over
  {C C' : category} (E : adj_equiv C C')
  {D : disp_cat C} {D' : disp_cat C'}
  (AA : disp_adjunction_data E D D')
  (EE : form_equiv_over (E:=E) AA)
: triangle_1_statement_over (A:=E) AA -> triangle_2_statement_over (A:=E) AA.
Proof.
  destruct AA as [FF [GG [η ε]]].
  destruct EE as [Hη Hε]; cbn in Hη, Hε.
  unfold triangle_1_statement_over, triangle_2_statement_over; cbn.
  intros T1 x yy.
  etrans. apply id_left_disp_var.
  etrans. eapply transportf_bind.
    eapply cancel_postcomposition_disp.
    etrans. eapply transportf_transpose. apply @pathsinv0.
      refine (iso_disp_after_inv_mor _).
      refine (disp_functor_on_is_iso_disp GG _).
      apply Hε.     eapply transportf_bind.
    eapply cancel_postcomposition_disp.
    etrans. apply id_right_disp_var.
    eapply transportf_bind.
    etrans. eapply cancel_precomposition_disp.
    eapply transportf_transpose. apply @pathsinv0.
      refine (iso_disp_after_inv_mor _).
      apply (Hη).     eapply transportf_bind, assoc_disp.
  etrans. eapply transportf_bind.
    etrans. apply assoc_disp_var.
    eapply transportf_bind.
    etrans. apply assoc_disp_var.
    eapply transportf_bind.
    eapply cancel_precomposition_disp.
    etrans. eapply cancel_precomposition_disp.
      etrans. apply assoc_disp.
      eapply transportf_bind.
      etrans. eapply cancel_postcomposition_disp.
        refine (disp_nat_trans_ax η (# GG (ε x yy))).       eapply transportf_bind.
      etrans. apply assoc_disp_var.
      eapply transportf_bind.
      eapply cancel_precomposition_disp.
      cbn.
      etrans. eapply transportf_transpose.
        apply @pathsinv0, (disp_functor_comp GG).
      eapply transportf_bind.
      etrans. apply maponpaths.
        apply (disp_nat_trans_ax ε).       cbn.
      etrans. apply (disp_functor_transportf _ GG).
      eapply transportf_bind.
      apply (disp_functor_comp GG).
    eapply transportf_bind.
    etrans. apply assoc_disp.
    eapply transportf_bind.
    etrans. eapply cancel_postcomposition_disp.
      apply (disp_nat_trans_ax η (η _ (GG x yy))).     cbn.
    eapply transportf_bind.
    etrans. apply assoc_disp_var.
    eapply transportf_bind.
    eapply cancel_precomposition_disp.
    etrans. apply assoc_disp.
    eapply transportf_bind.
    etrans. eapply cancel_postcomposition_disp.
      etrans. eapply transportf_transpose.
        apply @pathsinv0, (disp_functor_comp GG).       eapply transportf_bind.
      etrans. apply maponpaths, T1.       etrans. apply (disp_functor_transportf _ GG).
      eapply transportf_bind. apply (disp_functor_id GG).
    eapply transportf_bind. apply id_left_disp.
  etrans. eapply transportf_bind.
    etrans. apply assoc_disp_var.
    eapply transportf_bind.
    etrans. eapply cancel_precomposition_disp.
      etrans. apply assoc_disp.
      eapply transportf_bind.
      etrans. eapply cancel_postcomposition_disp.
        exact (iso_disp_after_inv_mor _).       eapply transportf_bind. apply id_left_disp.
    apply maponpaths. exact (iso_disp_after_inv_mor _).   etrans. apply transport_f_f.
  unfold transportb. apply maponpaths_2, homset_property.
Time Qed.

Lemma triangle_1_from_2_for_equiv_over_id
      {C C' : category} (E : adj_equiv C C')
      {D : disp_cat C} {D' : disp_cat C'}
      (AA : disp_adjunction_data E D D')
      (EE : form_equiv_over (E:=E) AA)
: triangle_2_statement_over (A:=E) AA -> triangle_1_statement_over (A:=E) AA.
Proof.
Abort.

End Equivalences.

Constructions on and of equivalences

Full + faithful + ess split => equivalence

Section Equiv_from_ff_plus_ess_split.

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

Utility lemmas from fullness+faithfulness

Let FFweq {x y} xx yy (f : x --> y) : xx -->[ f ] yy ≃ FF x xx -->[ (# F)%Cat f ] FF y yy
  := disp_functor_ff_weq _ FF_ff xx yy f.
Let FFinv {x y} {xx} {yy} {f} : FF x xx -->[ (# F)%Cat f ] FF y yy → xx -->[ f ] yy
  := @disp_functor_ff_inv _ _ _ _ _ _ FF_ff x y xx yy f.

Lemma FFinv_transportf
    {x y : C} {f f' : x --> y} (e : f = f')
    {xx : D x} {yy : D y} (ff : FF _ xx -->[(#F)%cat f ] FF _ yy)
  : FFinv (transportf (fun f' => _ -->[ (#F)%Cat f'] _ ) e ff) = transportf _ e (FFinv ff).
Proof.
  destruct e. apply idpath.
Qed.

Definition disp_functor_id_ff_reflects_isos
  {x y} {xx : D x} {yy : D y} {f : iso x y}
  (ff : xx -->[ f ] yy) (isiso: is_iso_disp (functor_on_iso F f) (# FF ff))
  : is_iso_disp _ ff.
Proof.
  set (FFffinv := inv_mor_disp_from_iso isiso).
  set (FFffinv':= transportf (fun f' => _ -->[ _ ] _ ) (functor_on_inv_from_iso F f) FFffinv). cbn in FFffinv'. unfold precomp_with in FFffinv'.
  set (FFffinv'' := transportf (fun f' => _ -->[f'] _ ) (id_right _ ) FFffinv').
  cbn in FFffinv''.
  set (ffinv := FFinv FFffinv'').
  exists ffinv.
  split.
  - unfold ffinv, FFffinv''; clear ffinv FFffinv''.
    apply (invmaponpathsweq (@FFweq _ _ _ _ _ )). cbn.
    etrans. apply (disp_functor_comp FF).
    etrans. apply maponpaths. apply maponpaths_2. apply (homotweqinvweq (@FFweq _ _ _ _ _ )).
    etrans. apply maponpaths. apply mor_disp_transportf_postwhisker.
    etrans. apply transport_f_f.
    unfold FFffinv'; clear FFffinv'.
    etrans. apply maponpaths. eapply maponpaths_2. apply transportf_const.
    etrans. apply maponpaths. unfold FFffinv. apply (iso_disp_after_inv_mor isiso).
    etrans. apply transport_f_f.
    apply pathsinv0.
    etrans. apply (disp_functor_transportf _ FF).
    etrans. apply maponpaths. apply disp_functor_id.
    etrans. apply transport_f_f.
    apply maponpaths_2. apply homset_property.
  - unfold ffinv, FFffinv''; clear ffinv FFffinv''.
    apply (invmaponpathsweq (@FFweq _ _ _ _ _ )). cbn.
    etrans. apply (disp_functor_comp FF).
    etrans. apply maponpaths. apply maponpaths. apply (homotweqinvweq (@FFweq _ _ _ _ _ )).
        etrans. apply maponpaths. apply mor_disp_transportf_prewhisker.
    etrans. apply transport_f_f.
    unfold FFffinv'; clear FFffinv'.
    etrans. apply maponpaths. eapply maponpaths. apply transportf_const.
    etrans. apply maponpaths. unfold FFffinv. apply (inv_mor_after_iso_disp isiso).
    etrans. apply transport_f_f.
    apply pathsinv0.
    etrans. apply (disp_functor_transportf _ FF).
    etrans. apply maponpaths. apply disp_functor_id.
    etrans. apply transport_f_f.
    apply maponpaths_2. apply homset_property.
Qed.

Definition FFinv_on_iso_is_iso {x y} {xx : D x} {yy : D y} {f : iso x y}
  (ff : FF _ xx -->[ (#F)%cat f ] FF _ yy) (Hff: is_iso_disp (functor_on_iso F f) ff)
  : is_iso_disp _ (FFinv ff).
Proof.
  apply disp_functor_id_ff_reflects_isos.
  refine (transportf _ _ Hff).
  apply @pathsinv0. use homotweqinvweq.
Qed.

TypeTheory