Library UniMath.Bicategories.PseudoFunctors.Display.Base
We construct the bicategory of pseudofunctors as a displayed bicategory.
This is the first layer and it just consists of plain functions mapping objects to objects.
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Adjunctions.
Require Import UniMath.Bicategories.Core.Invertible_2cells.
Require Import UniMath.Bicategories.Core.Univalence.
Require Import UniMath.Bicategories.Core.AdjointUnique.
Local Open Scope cat.
Section BasePseudoFunctor.
Variable (C D : bicat).
Definition ps_base_data : prebicat_data.
Proof.
use build_prebicat_data.
- exact (ob C → ob D).
- exact (λ f g, ∏ (x : C), f x --> g x).
- exact (λ f g α β, ∏ (x : C), α x ==> β x).
- exact (λ f x, id₁ (f x)).
- exact (λ f g h α β x, α x · β x).
- exact (λ f g α x, id₂ (α x)).
- exact (λ f g α β γ m₁ m₂ x, m₁ x • m₂ x).
- exact (λ f g h α β γ m x, α x ◃ m x).
- exact (λ f g h α β γ m x, m x ▹ γ x).
- exact (λ f g α x, lunitor (α x)).
- exact (λ f g α x, linvunitor (α x)).
- exact (λ f g α x, runitor (α x)).
- exact (λ f g α x, rinvunitor (α x)).
- exact (λ f₁ f₂ f₃ f₄ α β γ x, lassociator (α x) (β x) (γ x)).
- exact (λ f₁ f₂ f₃ f₄ α β γ x, rassociator (α x) (β x) (γ x)).
Defined.
Definition ps_base_laws
: prebicat_laws ps_base_data.
Proof.
repeat split ; intros ; apply funextsec ; intro.
- apply id2_left.
- apply id2_right.
- apply vassocr.
- apply lwhisker_id2.
- apply id2_rwhisker.
- apply lwhisker_vcomp.
- apply rwhisker_vcomp.
- apply vcomp_lunitor.
- apply vcomp_runitor.
- apply lwhisker_lwhisker.
- apply rwhisker_lwhisker.
- apply rwhisker_rwhisker.
- apply vcomp_whisker.
- apply lunitor_linvunitor.
- apply linvunitor_lunitor.
- apply runitor_rinvunitor.
- apply rinvunitor_runitor.
- apply lassociator_rassociator.
- apply rassociator_lassociator.
- apply runitor_rwhisker.
- apply lassociator_lassociator.
Qed.
Definition ps_base
: bicat.
Proof.
use build_bicategory.
- exact ps_base_data.
- exact ps_base_laws.
- intros ? ? ? ?.
use impred_isaset ; intro.
apply D.
Defined.
Definition all_is_invertible_to_is_invertible_2cell
{F G : ps_base}
{η ε : F --> G}
(α : η ==> ε)
: (∏ (X : C), is_invertible_2cell (α X)) → is_invertible_2cell α.
Proof.
intros Hα.
use tpair ; cbn in ×.
- exact (λ x, (Hα x)^-1).
- split ; apply funextsec ; intro X ; cbn.
+ apply vcomp_rinv.
+ apply vcomp_linv.
Defined.
Definition is_invertible_2cell_to_all_is_invertible
{F G : ps_base}
{η ε : F --> G}
(α : η ==> ε)
: is_invertible_2cell α → (∏ (X : C), is_invertible_2cell (α X)).
Proof.
intros Hα X.
use tpair.
- exact (Hα^-1 X).
- split ; cbn.
+ exact (maponpaths (λ φ, φ X) (vcomp_rinv Hα)).
+ exact (maponpaths (λ φ, φ X) (vcomp_linv Hα)).
Defined.
Definition all_is_invertible_is_is_invertible_2cell
{F G : ps_base}
{η ε : F --> G}
(α : η ==> ε)
: (∏ (X : C), is_invertible_2cell (α X)) ≃ is_invertible_2cell α.
Proof.
use weqimplimpl.
- exact (all_is_invertible_to_is_invertible_2cell α).
- exact (is_invertible_2cell_to_all_is_invertible α).
- apply impred ; intro.
apply isaprop_is_invertible_2cell.
- apply isaprop_is_invertible_2cell.
Defined.
Definition invertible_2cell_ps_base
{F G : ps_base}
(η ε : F --> G)
: (∏ (X : C), invertible_2cell (η X) (ε X))
→
invertible_2cell η ε.
Proof.
intros α.
use tpair.
- intros X.
exact (α X).
- apply all_is_invertible_is_is_invertible_2cell.
apply α.
Defined.
Definition invertible_2cell_ps_base_inv
{F G : ps_base}
(η ε : F --> G)
: invertible_2cell η ε
→
(∏ (X : C), invertible_2cell (η X) (ε X)).
Proof.
intros α X.
use tpair.
- exact (cell_from_invertible_2cell α X).
- apply is_invertible_2cell_to_all_is_invertible.
apply α.
Defined.
Definition invertible_2cell_ps_base_weq
{F G : ps_base}
(η ε : F --> G)
: (∏ (X : C), invertible_2cell (η X) (ε X))
≃
invertible_2cell η ε.
Proof.
refine (make_weq (invertible_2cell_ps_base η ε) _).
use isweq_iso.
- exact (invertible_2cell_ps_base_inv η ε).
- intros α.
apply funextsec ; intro X.
apply subtypePath.
{ intro ; apply isaprop_is_invertible_2cell. }
reflexivity.
- intros α.
apply subtypePath.
{ intro ; apply isaprop_is_invertible_2cell. }
apply funextsec ; intro X.
reflexivity.
Defined.
Definition ps_base_is_univalent_2_1
(HD_2_1 : is_univalent_2_1 D)
: is_univalent_2_1 ps_base.
Proof.
intros F G η ε.
use weqhomot.
- simple refine (invertible_2cell_ps_base_weq η ε ∘ _)%weq.
simple refine (_ ∘ make_weq _ (isweqtoforallpaths _ _ _))%weq.
simple refine (weqonsecfibers _ _ _).
intro X ; cbn.
exact (make_weq (idtoiso_2_1 (η X) (ε X)) (HD_2_1 _ _ _ _)).
- intros p.
induction p.
use subtypePath.
{ intro ; apply isaprop_is_invertible_2cell. }
reflexivity.
Defined.
Definition all_is_adjequiv_to_is_adjequiv
{F G : ps_base}
(η : F --> G)
: (∏ (X : C), left_adjoint_equivalence (η X)) → left_adjoint_equivalence η.
Proof.
intros Hη.
use tpair.
- use tpair.
+ intros X.
exact (pr11 (Hη X)).
+ split ; intros X ; cbn.
× exact (pr121 (Hη X)).
× exact (pr221 (Hη X)).
- split ; split ; cbn.
+ apply funextsec ; intro X.
exact (pr112 (Hη X)).
+ apply funextsec ; intro X.
exact (pr212 (Hη X)).
+ apply all_is_invertible_is_is_invertible_2cell.
exact (λ X, pr122 (Hη X)).
+ apply all_is_invertible_is_is_invertible_2cell.
exact (λ X, pr222 (Hη X)).
Defined.
Definition is_adjequiv_to_all_is_adjequiv
{F G : ps_base}
(η : F --> G)
: left_adjoint_equivalence η → (∏ (X : C), left_adjoint_equivalence (η X)).
Proof.
intros Hη X.
use tpair.
- use tpair.
+ exact (pr11 Hη X).
+ split ; cbn.
× exact (pr121 Hη X).
× exact (pr221 Hη X).
- split ; split ; cbn.
+ exact (maponpaths (λ φ, φ X) (pr112 Hη)).
+ exact (maponpaths (λ φ, φ X) (pr212 Hη)).
+ exact (is_invertible_2cell_to_all_is_invertible (pr121 Hη) (pr122 Hη) X).
+ exact (is_invertible_2cell_to_all_is_invertible (pr221 Hη) (pr222 Hη) X).
Defined.
Definition all_is_adjequiv_is_is_adjequiv
{F G : ps_base}
(η : F --> G)
: (∏ (X : C), left_adjoint_equivalence (η X)) ≃ left_adjoint_equivalence η.
Proof.
refine (make_weq (all_is_adjequiv_to_is_adjequiv η) _).
use isweq_iso.
- exact (is_adjequiv_to_all_is_adjequiv η).
- intros Hη.
apply funextsec ; intro X.
use subtypePath.
{
intro.
do 2 apply isapropdirprod ; try (apply D)
; apply isaprop_is_invertible_2cell.
}
reflexivity.
- intros Hη.
use subtypePath.
{
intro.
do 2 apply isapropdirprod ; try (apply ps_base)
; apply isaprop_is_invertible_2cell.
}
reflexivity.
Defined.
Definition adjequiv_ps_base
(F G : ps_base)
: (∏ (X : C), adjoint_equivalence (F X) (G X))
→
adjoint_equivalence F G.
Proof.
intros η.
use tpair.
- intros X.
exact (η X).
- apply all_is_adjequiv_is_is_adjequiv.
apply η.
Defined.
Definition adjequiv_ps_base_inv
(F G : ps_base)
: adjoint_equivalence F G
→
(∏ (X : C), adjoint_equivalence (F X) (G X)).
Proof.
intros η X.
use tpair.
- exact (pr1 η X).
- apply is_adjequiv_to_all_is_adjequiv.
apply η.
Defined.
Definition adjequiv_ps_base_weq
(F G : ps_base)
: (∏ (X : C), adjoint_equivalence (F X) (G X))
≃
adjoint_equivalence F G.
Proof.
refine (make_weq (adjequiv_ps_base F G) _).
use isweq_iso.
- exact (adjequiv_ps_base_inv F G).
- intros η.
apply funextsec ; intro X.
use total2_paths_b.
+ reflexivity.
+ cbn ; unfold idfun.
use subtypePath.
{
intro.
do 2 apply isapropdirprod ; try (apply D)
; apply isaprop_is_invertible_2cell.
}
reflexivity.
- intros η.
use total2_paths_b.
+ reflexivity.
+ cbn ; unfold idfun.
use subtypePath.
{
intro.
do 2 apply isapropdirprod ; try (apply ps_base)
; apply isaprop_is_invertible_2cell.
}
reflexivity.
Defined.
Definition ps_base_is_univalent_2_0
(HD : is_univalent_2 D)
: is_univalent_2_0 ps_base.
Proof.
intros F G.
use weqhomot.
- simple refine (adjequiv_ps_base_weq F G ∘ _)%weq.
simple refine (_ ∘ make_weq _ (isweqtoforallpaths _ _ _))%weq.
simple refine (weqonsecfibers _ _ _).
intro X ; cbn.
exact (make_weq (idtoiso_2_0 (F X) (G X)) (pr1 HD _ _)).
- intros p.
induction p.
use subtypePath.
{
intro.
apply isaprop_left_adjoint_equivalence.
exact (ps_base_is_univalent_2_1 (pr2 HD)).
}
reflexivity.
Defined.
Definition ps_base_is_univalent_2
(HD : is_univalent_2 D)
: is_univalent_2 ps_base.
Proof.
split.
- apply ps_base_is_univalent_2_0; assumption.
- apply ps_base_is_univalent_2_1.
exact (pr2 HD).
Defined.
End BasePseudoFunctor.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Adjunctions.
Require Import UniMath.Bicategories.Core.Invertible_2cells.
Require Import UniMath.Bicategories.Core.Univalence.
Require Import UniMath.Bicategories.Core.AdjointUnique.
Local Open Scope cat.
Section BasePseudoFunctor.
Variable (C D : bicat).
Definition ps_base_data : prebicat_data.
Proof.
use build_prebicat_data.
- exact (ob C → ob D).
- exact (λ f g, ∏ (x : C), f x --> g x).
- exact (λ f g α β, ∏ (x : C), α x ==> β x).
- exact (λ f x, id₁ (f x)).
- exact (λ f g h α β x, α x · β x).
- exact (λ f g α x, id₂ (α x)).
- exact (λ f g α β γ m₁ m₂ x, m₁ x • m₂ x).
- exact (λ f g h α β γ m x, α x ◃ m x).
- exact (λ f g h α β γ m x, m x ▹ γ x).
- exact (λ f g α x, lunitor (α x)).
- exact (λ f g α x, linvunitor (α x)).
- exact (λ f g α x, runitor (α x)).
- exact (λ f g α x, rinvunitor (α x)).
- exact (λ f₁ f₂ f₃ f₄ α β γ x, lassociator (α x) (β x) (γ x)).
- exact (λ f₁ f₂ f₃ f₄ α β γ x, rassociator (α x) (β x) (γ x)).
Defined.
Definition ps_base_laws
: prebicat_laws ps_base_data.
Proof.
repeat split ; intros ; apply funextsec ; intro.
- apply id2_left.
- apply id2_right.
- apply vassocr.
- apply lwhisker_id2.
- apply id2_rwhisker.
- apply lwhisker_vcomp.
- apply rwhisker_vcomp.
- apply vcomp_lunitor.
- apply vcomp_runitor.
- apply lwhisker_lwhisker.
- apply rwhisker_lwhisker.
- apply rwhisker_rwhisker.
- apply vcomp_whisker.
- apply lunitor_linvunitor.
- apply linvunitor_lunitor.
- apply runitor_rinvunitor.
- apply rinvunitor_runitor.
- apply lassociator_rassociator.
- apply rassociator_lassociator.
- apply runitor_rwhisker.
- apply lassociator_lassociator.
Qed.
Definition ps_base
: bicat.
Proof.
use build_bicategory.
- exact ps_base_data.
- exact ps_base_laws.
- intros ? ? ? ?.
use impred_isaset ; intro.
apply D.
Defined.
Definition all_is_invertible_to_is_invertible_2cell
{F G : ps_base}
{η ε : F --> G}
(α : η ==> ε)
: (∏ (X : C), is_invertible_2cell (α X)) → is_invertible_2cell α.
Proof.
intros Hα.
use tpair ; cbn in ×.
- exact (λ x, (Hα x)^-1).
- split ; apply funextsec ; intro X ; cbn.
+ apply vcomp_rinv.
+ apply vcomp_linv.
Defined.
Definition is_invertible_2cell_to_all_is_invertible
{F G : ps_base}
{η ε : F --> G}
(α : η ==> ε)
: is_invertible_2cell α → (∏ (X : C), is_invertible_2cell (α X)).
Proof.
intros Hα X.
use tpair.
- exact (Hα^-1 X).
- split ; cbn.
+ exact (maponpaths (λ φ, φ X) (vcomp_rinv Hα)).
+ exact (maponpaths (λ φ, φ X) (vcomp_linv Hα)).
Defined.
Definition all_is_invertible_is_is_invertible_2cell
{F G : ps_base}
{η ε : F --> G}
(α : η ==> ε)
: (∏ (X : C), is_invertible_2cell (α X)) ≃ is_invertible_2cell α.
Proof.
use weqimplimpl.
- exact (all_is_invertible_to_is_invertible_2cell α).
- exact (is_invertible_2cell_to_all_is_invertible α).
- apply impred ; intro.
apply isaprop_is_invertible_2cell.
- apply isaprop_is_invertible_2cell.
Defined.
Definition invertible_2cell_ps_base
{F G : ps_base}
(η ε : F --> G)
: (∏ (X : C), invertible_2cell (η X) (ε X))
→
invertible_2cell η ε.
Proof.
intros α.
use tpair.
- intros X.
exact (α X).
- apply all_is_invertible_is_is_invertible_2cell.
apply α.
Defined.
Definition invertible_2cell_ps_base_inv
{F G : ps_base}
(η ε : F --> G)
: invertible_2cell η ε
→
(∏ (X : C), invertible_2cell (η X) (ε X)).
Proof.
intros α X.
use tpair.
- exact (cell_from_invertible_2cell α X).
- apply is_invertible_2cell_to_all_is_invertible.
apply α.
Defined.
Definition invertible_2cell_ps_base_weq
{F G : ps_base}
(η ε : F --> G)
: (∏ (X : C), invertible_2cell (η X) (ε X))
≃
invertible_2cell η ε.
Proof.
refine (make_weq (invertible_2cell_ps_base η ε) _).
use isweq_iso.
- exact (invertible_2cell_ps_base_inv η ε).
- intros α.
apply funextsec ; intro X.
apply subtypePath.
{ intro ; apply isaprop_is_invertible_2cell. }
reflexivity.
- intros α.
apply subtypePath.
{ intro ; apply isaprop_is_invertible_2cell. }
apply funextsec ; intro X.
reflexivity.
Defined.
Definition ps_base_is_univalent_2_1
(HD_2_1 : is_univalent_2_1 D)
: is_univalent_2_1 ps_base.
Proof.
intros F G η ε.
use weqhomot.
- simple refine (invertible_2cell_ps_base_weq η ε ∘ _)%weq.
simple refine (_ ∘ make_weq _ (isweqtoforallpaths _ _ _))%weq.
simple refine (weqonsecfibers _ _ _).
intro X ; cbn.
exact (make_weq (idtoiso_2_1 (η X) (ε X)) (HD_2_1 _ _ _ _)).
- intros p.
induction p.
use subtypePath.
{ intro ; apply isaprop_is_invertible_2cell. }
reflexivity.
Defined.
Definition all_is_adjequiv_to_is_adjequiv
{F G : ps_base}
(η : F --> G)
: (∏ (X : C), left_adjoint_equivalence (η X)) → left_adjoint_equivalence η.
Proof.
intros Hη.
use tpair.
- use tpair.
+ intros X.
exact (pr11 (Hη X)).
+ split ; intros X ; cbn.
× exact (pr121 (Hη X)).
× exact (pr221 (Hη X)).
- split ; split ; cbn.
+ apply funextsec ; intro X.
exact (pr112 (Hη X)).
+ apply funextsec ; intro X.
exact (pr212 (Hη X)).
+ apply all_is_invertible_is_is_invertible_2cell.
exact (λ X, pr122 (Hη X)).
+ apply all_is_invertible_is_is_invertible_2cell.
exact (λ X, pr222 (Hη X)).
Defined.
Definition is_adjequiv_to_all_is_adjequiv
{F G : ps_base}
(η : F --> G)
: left_adjoint_equivalence η → (∏ (X : C), left_adjoint_equivalence (η X)).
Proof.
intros Hη X.
use tpair.
- use tpair.
+ exact (pr11 Hη X).
+ split ; cbn.
× exact (pr121 Hη X).
× exact (pr221 Hη X).
- split ; split ; cbn.
+ exact (maponpaths (λ φ, φ X) (pr112 Hη)).
+ exact (maponpaths (λ φ, φ X) (pr212 Hη)).
+ exact (is_invertible_2cell_to_all_is_invertible (pr121 Hη) (pr122 Hη) X).
+ exact (is_invertible_2cell_to_all_is_invertible (pr221 Hη) (pr222 Hη) X).
Defined.
Definition all_is_adjequiv_is_is_adjequiv
{F G : ps_base}
(η : F --> G)
: (∏ (X : C), left_adjoint_equivalence (η X)) ≃ left_adjoint_equivalence η.
Proof.
refine (make_weq (all_is_adjequiv_to_is_adjequiv η) _).
use isweq_iso.
- exact (is_adjequiv_to_all_is_adjequiv η).
- intros Hη.
apply funextsec ; intro X.
use subtypePath.
{
intro.
do 2 apply isapropdirprod ; try (apply D)
; apply isaprop_is_invertible_2cell.
}
reflexivity.
- intros Hη.
use subtypePath.
{
intro.
do 2 apply isapropdirprod ; try (apply ps_base)
; apply isaprop_is_invertible_2cell.
}
reflexivity.
Defined.
Definition adjequiv_ps_base
(F G : ps_base)
: (∏ (X : C), adjoint_equivalence (F X) (G X))
→
adjoint_equivalence F G.
Proof.
intros η.
use tpair.
- intros X.
exact (η X).
- apply all_is_adjequiv_is_is_adjequiv.
apply η.
Defined.
Definition adjequiv_ps_base_inv
(F G : ps_base)
: adjoint_equivalence F G
→
(∏ (X : C), adjoint_equivalence (F X) (G X)).
Proof.
intros η X.
use tpair.
- exact (pr1 η X).
- apply is_adjequiv_to_all_is_adjequiv.
apply η.
Defined.
Definition adjequiv_ps_base_weq
(F G : ps_base)
: (∏ (X : C), adjoint_equivalence (F X) (G X))
≃
adjoint_equivalence F G.
Proof.
refine (make_weq (adjequiv_ps_base F G) _).
use isweq_iso.
- exact (adjequiv_ps_base_inv F G).
- intros η.
apply funextsec ; intro X.
use total2_paths_b.
+ reflexivity.
+ cbn ; unfold idfun.
use subtypePath.
{
intro.
do 2 apply isapropdirprod ; try (apply D)
; apply isaprop_is_invertible_2cell.
}
reflexivity.
- intros η.
use total2_paths_b.
+ reflexivity.
+ cbn ; unfold idfun.
use subtypePath.
{
intro.
do 2 apply isapropdirprod ; try (apply ps_base)
; apply isaprop_is_invertible_2cell.
}
reflexivity.
Defined.
Definition ps_base_is_univalent_2_0
(HD : is_univalent_2 D)
: is_univalent_2_0 ps_base.
Proof.
intros F G.
use weqhomot.
- simple refine (adjequiv_ps_base_weq F G ∘ _)%weq.
simple refine (_ ∘ make_weq _ (isweqtoforallpaths _ _ _))%weq.
simple refine (weqonsecfibers _ _ _).
intro X ; cbn.
exact (make_weq (idtoiso_2_0 (F X) (G X)) (pr1 HD _ _)).
- intros p.
induction p.
use subtypePath.
{
intro.
apply isaprop_left_adjoint_equivalence.
exact (ps_base_is_univalent_2_1 (pr2 HD)).
}
reflexivity.
Defined.
Definition ps_base_is_univalent_2
(HD : is_univalent_2 D)
: is_univalent_2 ps_base.
Proof.
split.
- apply ps_base_is_univalent_2_0; assumption.
- apply ps_base_is_univalent_2_1.
exact (pr2 HD).
Defined.
End BasePseudoFunctor.