Library UniMath.Bicategories.DisplayedBicats.DispTransformation
Displayed transformation.
Contents:
- Definition of displayed transformation.
- Identity and composition of displayed transformations.
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.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Examples.Initial.
Require Import UniMath.Bicategories.Core.Examples.Final.
Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations.
Require Import UniMath.Bicategories.Core.Univalence.
Require Import UniMath.Bicategories.Core.Invertible_2cells.
Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles.
Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions.
Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.
Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat.
Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor.
Require Import UniMath.Bicategories.PseudoFunctors.Examples.Identity.
Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition.
Require Import UniMath.Bicategories.Transformations.PseudoTransformation.
Require Import UniMath.Bicategories.Transformations.Examples.Whiskering.
Require Import UniMath.Bicategories.Transformations.Examples.Unitality.
Require Import UniMath.Bicategories.Transformations.Examples.Associativity.
Require Import UniMath.Bicategories.DisplayedBicats.DispPseudofunctor.
Import PseudoFunctor.Notations.
Local Open Scope cat.
Section DispTransformation.
Context {B₁ : bicat} {D₁ : disp_bicat B₁}
{B₂ : bicat} {D₂ : disp_bicat B₂}
{F₁ F₂ : psfunctor B₁ B₂}
(FF₁ : disp_psfunctor D₁ D₂ F₁)
(FF₂ : disp_psfunctor D₁ D₂ F₂)
(α : pstrans F₁ F₂).
Definition disp_pstrans_data : UU
:= ∑ αα₁ : ∏ (x : B₁) (xx : D₁ x), FF₁ x xx -->[ α x] FF₂ x xx,
∏ (x y : B₁) (f : B₁ ⟦ x, y ⟧) (xx : D₁ x) (yy : D₁ y) (ff : xx -->[ f] yy),
disp_invertible_2cell (psnaturality_of α f)
(αα₁ x xx;; disp_psfunctor_mor D₁ D₂ F₂ FF₂ ff)
(disp_psfunctor_mor D₁ D₂ F₁ FF₁ ff;; αα₁ y yy).
Definition make_disp_pstrans_data
(αα₁ : ∏ (x : B₁) (xx : D₁ x), FF₁ x xx -->[ α x] FF₂ x xx)
(αα₂ : ∏ (x y : B₁) (f : B₁ ⟦ x, y ⟧) (xx : D₁ x) (yy : D₁ y) (ff : xx -->[ f] yy),
disp_invertible_2cell (psnaturality_of α f)
(αα₁ x xx;; disp_psfunctor_mor D₁ D₂ F₂ FF₂ ff)
(disp_psfunctor_mor D₁ D₂ F₁ FF₁ ff;; αα₁ y yy))
: disp_pstrans_data
:= (αα₁,, αα₂).
Definition disp_pscomponent_of (αα : disp_pstrans_data)
: ∏ (x : B₁) (xx : D₁ x), FF₁ x xx -->[ α x] FF₂ x xx
:= pr1 αα.
Coercion disp_pscomponent_of : disp_pstrans_data >-> Funclass.
Definition disp_psnaturality_of (αα : disp_pstrans_data)
{x y : B₁}
{f : B₁ ⟦ x, y ⟧}
{xx : D₁ x} {yy : D₁ y}
(ff : xx -->[ f] yy)
: disp_invertible_2cell (psnaturality_of α f)
(αα x xx;; disp_psfunctor_mor D₁ D₂ F₂ FF₂ ff)
(disp_psfunctor_mor D₁ D₂ F₁ FF₁ ff;; αα y yy)
:= pr2 αα x y f xx yy ff.
Definition total_pstrans_data (ααdata : disp_pstrans_data)
: pstrans_data (total_psfunctor _ _ _ FF₁) (total_psfunctor _ _ _ FF₂).
Show proof.
use make_pstrans_data.
- exact (λ x, (α (pr1 x),, ααdata _ (pr2 x))).
- exact (λ x y f, iso_in_E_weq _ _ (psnaturality_of α (pr1 f),,
disp_psnaturality_of ααdata (pr2 f))).
- exact (λ x, (α (pr1 x),, ααdata _ (pr2 x))).
- exact (λ x y f, iso_in_E_weq _ _ (psnaturality_of α (pr1 f),,
disp_psnaturality_of ααdata (pr2 f))).
Section DispPstransLaws.
Variable ααdata : disp_pstrans_data.
Definition disp_psnaturality_natural_law : UU
:= ∏ (x y : B₁) (f g : B₁ ⟦ x, y ⟧)
(η : f ==> g)
(xx : D₁ x) (yy : D₁ y)
(ff : xx -->[ f] yy)
(gg : xx -->[ g] yy)
(ηη : ff ==>[ η] gg),
(ααdata x xx ◃◃ disp_psfunctor_cell D₁ D₂ F₂ FF₂ ηη) •• disp_psnaturality_of ααdata gg
=
transportb
(λ p, _ ==>[p] _)
(psnaturality_natural α x y f g η)
(disp_psnaturality_of ααdata ff •• (disp_psfunctor_cell D₁ D₂ F₁ FF₁ ηη ▹▹ ααdata y yy)).
Definition disp_pstrans_id_law : UU
:= ∏ (x : B₁) (xx : D₁ x),
(ααdata x xx ◃◃ disp_psfunctor_id D₁ D₂ F₂ FF₂ xx)
•• disp_psnaturality_of ααdata (id_disp xx)
=
transportb
(λ p, _ ==>[p] _)
(pstrans_id α x)
((disp_runitor (ααdata x xx) •• disp_linvunitor (ααdata x xx))
•• (disp_psfunctor_id D₁ D₂ F₁ FF₁ xx ▹▹ ααdata x xx)).
Definition disp_pstrans_comp_law : UU
:= ∏ (x y z : B₁)
(f : B₁ ⟦ x, y ⟧) (g : B₁ ⟦ y, z ⟧)
(xx : D₁ x) (yy : D₁ y) (zz : D₁ z)
(ff : xx -->[ f] yy) (gg : yy -->[ g] zz),
(ααdata x xx ◃◃ disp_psfunctor_comp D₁ D₂ F₂ FF₂ ff gg)
•• disp_psnaturality_of ααdata (ff;; gg) =
transportb
(λ p, _ ==>[p] _)
(pstrans_comp α f g)
(((((disp_lassociator
(ααdata x xx)
(disp_psfunctor_mor D₁ D₂ F₂ FF₂ ff)
(disp_psfunctor_mor D₁ D₂ F₂ FF₂ gg)
•• (disp_psnaturality_of ααdata ff ▹▹ disp_psfunctor_mor D₁ D₂ F₂ FF₂ gg))
•• disp_rassociator (disp_psfunctor_mor D₁ D₂ F₁ FF₁ ff) (ααdata y yy)
(disp_psfunctor_mor D₁ D₂ F₂ FF₂ gg))
•• (disp_psfunctor_mor D₁ D₂ F₁ FF₁ ff ◃◃ disp_psnaturality_of ααdata gg))
•• disp_lassociator (disp_psfunctor_mor D₁ D₂ F₁ FF₁ ff)
(disp_psfunctor_mor D₁ D₂ F₁ FF₁ gg) (ααdata z zz))
•• (disp_psfunctor_comp D₁ D₂ F₁ FF₁ ff gg ▹▹ ααdata z zz)).
Definition is_disp_pstrans
: UU
:= disp_psnaturality_natural_law
× disp_pstrans_id_law
× disp_pstrans_comp_law.
End DispPstransLaws.
Definition disp_pstrans : UU
:= ∑ αα : disp_pstrans_data, is_disp_pstrans αα.
Coercion disp_pstrans_to_disp_pstrans_data (αα : disp_pstrans)
: disp_pstrans_data
:= pr1 αα.
Lemma total_pstrans_laws (αα : disp_pstrans)
: is_pstrans (total_pstrans_data αα).
Show proof.
repeat apply make_dirprod; intro; intros.
- use total2_paths_b; [apply (psnaturality_natural α) | apply αα].
- use total2_paths_b; [apply (pstrans_id α) | apply αα].
- use total2_paths_b. 2: apply αα.
- use total2_paths_b; [apply (psnaturality_natural α) | apply αα].
- use total2_paths_b; [apply (pstrans_id α) | apply αα].
- use total2_paths_b. 2: apply αα.
Definition total_pstrans (αα : disp_pstrans)
: pstrans (total_psfunctor _ _ _ FF₁) (total_psfunctor _ _ _ FF₂).
Show proof.
Definition is_disp_pstrans_from_total (αα : disp_pstrans_data)
: is_pstrans (total_pstrans_data αα) → is_disp_pstrans αα.
Show proof.
intros Hαα.
pose (Eα := make_pstrans _ Hαα).
repeat split.
- intros x y f g η xx yy ff gg ηη.
pose (P := !fiber_paths (@psnaturality_natural _ _ _ _ Eα (x,,xx) (y,,yy) (f,,ff)
(g,,gg) (η,,ηη))).
symmetry.
etrans. { apply maponpaths. exact P. }
unfold transportb.
rewrite transport_f_f.
rewrite transportf_set.
* apply idpath.
* apply B₂.
- intros x xx.
pose (P := !fiber_paths (@pstrans_id _ _ _ _ Eα (x,,xx))).
symmetry.
etrans. { apply maponpaths. exact P. }
unfold transportb.
rewrite transport_f_f.
rewrite transportf_set.
* apply idpath.
* apply B₂.
- intros x y z f g xx yy zz ff gg.
pose (P := !fiber_paths
(@pstrans_comp _ _ _ _ Eα
(x,,xx) (y,,yy) (z,,zz) (f,,ff) (g,,gg)
)).
symmetry.
etrans. { apply maponpaths. exact P. }
unfold transportb.
rewrite transport_f_f.
rewrite transportf_set.
* apply idpath.
* apply B₂.
pose (Eα := make_pstrans _ Hαα).
repeat split.
- intros x y f g η xx yy ff gg ηη.
pose (P := !fiber_paths (@psnaturality_natural _ _ _ _ Eα (x,,xx) (y,,yy) (f,,ff)
(g,,gg) (η,,ηη))).
symmetry.
etrans. { apply maponpaths. exact P. }
unfold transportb.
rewrite transport_f_f.
rewrite transportf_set.
* apply idpath.
* apply B₂.
- intros x xx.
pose (P := !fiber_paths (@pstrans_id _ _ _ _ Eα (x,,xx))).
symmetry.
etrans. { apply maponpaths. exact P. }
unfold transportb.
rewrite transport_f_f.
rewrite transportf_set.
* apply idpath.
* apply B₂.
- intros x y z f g xx yy zz ff gg.
pose (P := !fiber_paths
(@pstrans_comp _ _ _ _ Eα
(x,,xx) (y,,yy) (z,,zz) (f,,ff) (g,,gg)
)).
symmetry.
etrans. { apply maponpaths. exact P. }
unfold transportb.
rewrite transport_f_f.
rewrite transportf_set.
* apply idpath.
* apply B₂.
End DispTransformation.
Section DispTrans_identity.
Context {B₁ B₂ : bicat}
{D₁ : disp_bicat B₁}
{D₂ : disp_bicat B₂}
{F : psfunctor B₁ B₂}
(FF : disp_psfunctor D₁ D₂ F).
Definition disp_id_pstrans_data
: disp_pstrans_data FF FF (id_pstrans F).
Show proof.
use make_disp_pstrans_data; cbn.
- exact (λ x xx, id_disp (FF x xx)).
- intros.
apply (vcomp_disp_invertible (disp_invertible_2cell_lunitor _)
(disp_invertible_2cell_rinvunitor _)).
- exact (λ x xx, id_disp (FF x xx)).
- intros.
apply (vcomp_disp_invertible (disp_invertible_2cell_lunitor _)
(disp_invertible_2cell_rinvunitor _)).
Lemma disp_id_pstrans_laws : is_disp_pstrans _ _ _ disp_id_pstrans_data.
Show proof.
apply is_disp_pstrans_from_total.
pose (PP := id_pstrans (total_psfunctor _ _ _ FF)).
pose (PP2 := pstrans_to_is_pstrans PP).
assert (pr11 PP = total_pstrans_data FF FF (id_pstrans F) disp_id_pstrans_data).
- use total2_paths_f.
+ apply idpath.
+ apply funextsec. intro x.
apply funextsec. intro y.
apply funextsec. intro f.
use subtypePath.
{ intro. apply isaprop_is_invertible_2cell. }
apply idpath.
- exact (transportf _ X PP2).
pose (PP := id_pstrans (total_psfunctor _ _ _ FF)).
pose (PP2 := pstrans_to_is_pstrans PP).
assert (pr11 PP = total_pstrans_data FF FF (id_pstrans F) disp_id_pstrans_data).
- use total2_paths_f.
+ apply idpath.
+ apply funextsec. intro x.
apply funextsec. intro y.
apply funextsec. intro f.
use subtypePath.
{ intro. apply isaprop_is_invertible_2cell. }
apply idpath.
- exact (transportf _ X PP2).
Definition disp_id_pstrans : disp_pstrans FF FF (id_pstrans F)
:= disp_id_pstrans_data,, disp_id_pstrans_laws.
End DispTrans_identity.
Section DispTrans_comp.
Context {B₁ B₂ : bicat}
{F₁ : psfunctor B₁ B₂}
{F₂ : psfunctor B₁ B₂}
{F₃ : psfunctor B₁ B₂}
{η₁ : pstrans F₁ F₂}
{η₂ : pstrans F₂ F₃}
{D₁ : disp_bicat B₁}
{D₂ : disp_bicat B₂}
{FF₁ : disp_psfunctor D₁ D₂ F₁}
{FF₂ : disp_psfunctor D₁ D₂ F₂}
{FF₃ : disp_psfunctor D₁ D₂ F₃}
(ηη₁ : disp_pstrans FF₁ FF₂ η₁)
(ηη₂ : disp_pstrans FF₂ FF₃ η₂).
Local Notation "αα '••' ββ" := (vcomp_disp_invertible αα ββ).
Local Notation "ff '◃◃' αα" := (disp_invertible_2cell_lwhisker ff αα).
Local Notation "αα '▹▹' ff" := (disp_invertible_2cell_rwhisker ff αα).
Definition disp_comp_pstrans_data : disp_pstrans_data FF₁ FF₃ (comp_pstrans η₁ η₂).
Show proof.
use make_disp_pstrans_data; cbn.
- exact (λ x xx, comp_disp (ηη₁ x xx) (ηη₂ x xx)).
- exact (λ x y f xx yy ff,
(disp_invertible_2cell_rassociator _ _ _)
•• (_ ◃◃ disp_psnaturality_of _ _ _ ηη₂ ff)
•• disp_invertible_2cell_lassociator _ _ _
•• (disp_psnaturality_of _ _ _ ηη₁ ff ▹▹ _)
•• disp_invertible_2cell_rassociator _ _ _).
- exact (λ x xx, comp_disp (ηη₁ x xx) (ηη₂ x xx)).
- exact (λ x y f xx yy ff,
(disp_invertible_2cell_rassociator _ _ _)
•• (_ ◃◃ disp_psnaturality_of _ _ _ ηη₂ ff)
•• disp_invertible_2cell_lassociator _ _ _
•• (disp_psnaturality_of _ _ _ ηη₁ ff ▹▹ _)
•• disp_invertible_2cell_rassociator _ _ _).
Lemma disp_comp_pstrans_laws : is_disp_pstrans _ _ _ disp_comp_pstrans_data.
Show proof.
apply is_disp_pstrans_from_total.
pose (PP := comp_pstrans (total_pstrans _ _ _ ηη₁) (total_pstrans _ _ _ ηη₂)).
pose (PP2 := pstrans_to_is_pstrans PP).
assert (pr11 PP = total_pstrans_data _ _ _ disp_comp_pstrans_data).
- use total2_paths_f.
+ apply idpath.
+ apply funextsec. intro x.
apply funextsec. intro y.
apply funextsec. intro f.
use subtypePath.
{ intro. apply isaprop_is_invertible_2cell. }
apply idpath.
- exact (transportf _ X PP2).
pose (PP := comp_pstrans (total_pstrans _ _ _ ηη₁) (total_pstrans _ _ _ ηη₂)).
pose (PP2 := pstrans_to_is_pstrans PP).
assert (pr11 PP = total_pstrans_data _ _ _ disp_comp_pstrans_data).
- use total2_paths_f.
+ apply idpath.
+ apply funextsec. intro x.
apply funextsec. intro y.
apply funextsec. intro f.
use subtypePath.
{ intro. apply isaprop_is_invertible_2cell. }
apply idpath.
- exact (transportf _ X PP2).
Definition disp_comp_pstrans : disp_pstrans _ _ (comp_pstrans η₁ η₂)
:= disp_comp_pstrans_data,, disp_comp_pstrans_laws.
End DispTrans_comp.
Definition disp_inv_invertible
{B : bicat}
{D : disp_bicat B}
{x y : B}
{f g : x --> y}
{α : invertible_2cell f g}
{xx : D x} {yy : D y}
{ff : xx -->[ f ] yy} {gg : xx -->[ g ] yy}
(αα : disp_invertible_2cell α ff gg)
: disp_invertible_2cell (inv_of_invertible_2cell α) gg ff.
Show proof.
use tpair.
- exact (disp_inv_cell αα).
- use tpair.
+ apply αα.
+ split ; cbn.
* apply disp_vcomp_linv.
* apply disp_vcomp_rinv.
- exact (disp_inv_cell αα).
- use tpair.
+ apply αα.
+ split ; cbn.
* apply disp_vcomp_linv.
* apply disp_vcomp_rinv.
Section DispTrans_lwhisker.
Context {B₁ B₂ B₃ : bicat}
{F₁ F₂ : psfunctor B₁ B₂}
{G : psfunctor B₂ B₃}
{η : pstrans F₁ F₂}
{D₁ : disp_bicat B₁}
{D₂ : disp_bicat B₂}
{D₃ : disp_bicat B₃}
{FF₁ : disp_psfunctor D₁ D₂ F₁}
{FF₂ : disp_psfunctor D₁ D₂ F₂}
(GG : disp_psfunctor D₂ D₃ G)
(ηη : disp_pstrans FF₁ FF₂ η).
Local Notation "αα '••' ββ" := (vcomp_disp_invertible αα ββ).
Definition disp_left_whisker_data
: disp_pstrans_data
(disp_pseudo_comp _ _ _ _ _ FF₁ GG)
(disp_pseudo_comp _ _ _ _ _ FF₂ GG)
(G ◅ η).
Show proof.
use make_disp_pstrans_data; cbn.
- exact (λ x xx, pr121 GG _ _ _ _ _ (pr11 ηη x xx)).
- exact (λ x y f xx yy ff,
(disp_psfunctor_comp _ _ _ GG _ _)
•• disp_psfunctor_invertible_2cell GG (disp_psnaturality_of _ _ _ ηη ff)
•• (disp_inv_invertible (disp_psfunctor_comp _ _ _ GG _ _))).
- exact (λ x xx, pr121 GG _ _ _ _ _ (pr11 ηη x xx)).
- exact (λ x y f xx yy ff,
(disp_psfunctor_comp _ _ _ GG _ _)
•• disp_psfunctor_invertible_2cell GG (disp_psnaturality_of _ _ _ ηη ff)
•• (disp_inv_invertible (disp_psfunctor_comp _ _ _ GG _ _))).
Lemma disp_left_whisker_laws : is_disp_pstrans _ _ _ disp_left_whisker_data.
Show proof.
apply is_disp_pstrans_from_total.
pose (PP := (total_psfunctor _ _ _ GG) ◅ total_pstrans _ _ _ ηη).
pose (PP2 := pstrans_to_is_pstrans PP).
assert (pstrans_to_pstrans_data PP = total_pstrans_data _ _ _ disp_left_whisker_data).
- use total2_paths_f.
+ apply idpath.
+ apply funextsec. intro x.
apply funextsec. intro y.
apply funextsec. intro f.
use subtypePath.
{ intro. apply isaprop_is_invertible_2cell. }
apply idpath.
- exact (transportf is_pstrans X PP2).
pose (PP := (total_psfunctor _ _ _ GG) ◅ total_pstrans _ _ _ ηη).
pose (PP2 := pstrans_to_is_pstrans PP).
assert (pstrans_to_pstrans_data PP = total_pstrans_data _ _ _ disp_left_whisker_data).
- use total2_paths_f.
+ apply idpath.
+ apply funextsec. intro x.
apply funextsec. intro y.
apply funextsec. intro f.
use subtypePath.
{ intro. apply isaprop_is_invertible_2cell. }
apply idpath.
- exact (transportf is_pstrans X PP2).
Definition disp_left_whisker
: disp_pstrans
(disp_pseudo_comp _ _ _ _ _ FF₁ GG)
(disp_pseudo_comp _ _ _ _ _ FF₂ GG)
(G ◅ η)
:= disp_left_whisker_data,, disp_left_whisker_laws.
End DispTrans_lwhisker.
Section DispTrans_rwhisker.
Context {B₁ B₂ B₃ : bicat}
{F : psfunctor B₁ B₂}
{G₁ G₂ : psfunctor B₂ B₃}
{η : pstrans G₁ G₂}
{D₁ : disp_bicat B₁}
{D₂ : disp_bicat B₂}
{D₃ : disp_bicat B₃}
(FF : disp_psfunctor D₁ D₂ F)
{GG₁ : disp_psfunctor D₂ D₃ G₁}
{GG₂ : disp_psfunctor D₂ D₃ G₂}
(ηη : disp_pstrans GG₁ GG₂ η).
Definition disp_right_whisker_data
: disp_pstrans_data
(disp_pseudo_comp _ _ _ _ _ FF GG₁)
(disp_pseudo_comp _ _ _ _ _ FF GG₂)
(η ▻ F).
Show proof.
use make_disp_pstrans_data; cbn.
- exact (λ x xx, (pr11 ηη _ (FF _ xx))).
- exact (λ x y f xx yy ff, disp_psnaturality_of _ _ _ ηη (pr121 FF _ _ _ _ _ ff)).
- exact (λ x xx, (pr11 ηη _ (FF _ xx))).
- exact (λ x y f xx yy ff, disp_psnaturality_of _ _ _ ηη (pr121 FF _ _ _ _ _ ff)).
Lemma disp_right_whisker_laws : is_disp_pstrans _ _ _ disp_right_whisker_data.
Show proof.
apply is_disp_pstrans_from_total.
pose (PP := (total_pstrans _ _ _ ηη) ▻ (total_psfunctor _ _ _ FF)).
pose (PP2 := pstrans_to_is_pstrans PP).
assert (X : pstrans_to_pstrans_data PP
=
total_pstrans_data _ _ _ disp_right_whisker_data).
- use total2_paths_f.
+ apply idpath.
+ apply funextsec. intro x.
apply funextsec. intro y.
apply funextsec. intro f.
use subtypePath.
{ intro. apply isaprop_is_invertible_2cell. }
lazy.
apply idpath.
- exact (transportf is_pstrans X PP2).
pose (PP := (total_pstrans _ _ _ ηη) ▻ (total_psfunctor _ _ _ FF)).
pose (PP2 := pstrans_to_is_pstrans PP).
assert (X : pstrans_to_pstrans_data PP
=
total_pstrans_data _ _ _ disp_right_whisker_data).
- use total2_paths_f.
+ apply idpath.
+ apply funextsec. intro x.
apply funextsec. intro y.
apply funextsec. intro f.
use subtypePath.
{ intro. apply isaprop_is_invertible_2cell. }
lazy.
apply idpath.
- exact (transportf is_pstrans X PP2).
Definition disp_right_whisker
: disp_pstrans
(disp_pseudo_comp _ _ _ _ _ FF GG₁)
(disp_pseudo_comp _ _ _ _ _ FF GG₂)
(η ▻ F)
:= disp_right_whisker_data,, disp_right_whisker_laws.
End DispTrans_rwhisker.
Section DispTransUnitality.
Context {B₁ B₂ : bicat}
{F : psfunctor B₁ B₂}
{D₁ : disp_bicat B₁}
{D₂ : disp_bicat B₂}
(FF : disp_psfunctor D₁ D₂ F).
Definition disp_lunitor_pstrans_data
: disp_pstrans_data
(disp_pseudo_comp _ _ _ _ _ FF (disp_pseudo_id D₂))
FF
(lunitor_pstrans F).
Show proof.
use make_disp_pstrans_data.
- exact (λ x xx, id_disp (FF x xx)).
- cbn.
refine (λ x y f xx yy ff, _).
apply (vcomp_disp_invertible (disp_invertible_2cell_lunitor _)
(disp_invertible_2cell_rinvunitor _)).
- exact (λ x xx, id_disp (FF x xx)).
- cbn.
refine (λ x y f xx yy ff, _).
apply (vcomp_disp_invertible (disp_invertible_2cell_lunitor _)
(disp_invertible_2cell_rinvunitor _)).
Lemma disp_lunitor_pstrans_laws : is_disp_pstrans _ _ _ disp_lunitor_pstrans_data.
Show proof.
apply is_disp_pstrans_from_total.
pose (PP := lunitor_pstrans (total_psfunctor _ _ _ FF)).
pose (PP2 := pstrans_to_is_pstrans PP).
assert (X : pstrans_to_pstrans_data PP
=
total_pstrans_data _ _ _ disp_lunitor_pstrans_data).
- use total2_paths_f.
+ apply idpath.
+ apply funextsec. intro x.
apply funextsec. intro y.
apply funextsec. intro f.
use subtypePath.
{ intro. apply isaprop_is_invertible_2cell. }
apply idpath.
- exact (transportf is_pstrans X PP2).
pose (PP := lunitor_pstrans (total_psfunctor _ _ _ FF)).
pose (PP2 := pstrans_to_is_pstrans PP).
assert (X : pstrans_to_pstrans_data PP
=
total_pstrans_data _ _ _ disp_lunitor_pstrans_data).
- use total2_paths_f.
+ apply idpath.
+ apply funextsec. intro x.
apply funextsec. intro y.
apply funextsec. intro f.
use subtypePath.
{ intro. apply isaprop_is_invertible_2cell. }
apply idpath.
- exact (transportf is_pstrans X PP2).
Definition disp_lunitor_pstrans
: disp_pstrans
(disp_pseudo_comp _ _ _ _ _ FF (disp_pseudo_id D₂))
FF
(lunitor_pstrans F)
:= disp_lunitor_pstrans_data,, disp_lunitor_pstrans_laws.
Definition disp_pstrans_linvunitor_data
: disp_pstrans_data
FF
(disp_pseudo_comp _ _ _ _ _ FF (disp_pseudo_id D₂))
(linvunitor_pstrans F).
Show proof.
use make_disp_pstrans_data.
- exact (λ x xx, id_disp (FF x xx)).
- cbn.
refine (λ x y f xx yy ff, _).
apply (vcomp_disp_invertible (disp_invertible_2cell_lunitor _)
(disp_invertible_2cell_rinvunitor _)).
- exact (λ x xx, id_disp (FF x xx)).
- cbn.
refine (λ x y f xx yy ff, _).
apply (vcomp_disp_invertible (disp_invertible_2cell_lunitor _)
(disp_invertible_2cell_rinvunitor _)).
Lemma disp_pstrans_linvunitor_laws : is_disp_pstrans _ _ _ disp_pstrans_linvunitor_data.
Show proof.
apply is_disp_pstrans_from_total.
pose (PP := linvunitor_pstrans (total_psfunctor _ _ _ FF)).
pose (PP2 := pstrans_to_is_pstrans PP).
assert (X : pstrans_to_pstrans_data PP
=
total_pstrans_data _ _ _ disp_pstrans_linvunitor_data).
- use total2_paths_f.
+ apply idpath.
+ apply funextsec. intro x.
apply funextsec. intro y.
apply funextsec. intro f.
use subtypePath.
{ intro. apply isaprop_is_invertible_2cell. }
apply idpath.
- exact (transportf is_pstrans X PP2).
pose (PP := linvunitor_pstrans (total_psfunctor _ _ _ FF)).
pose (PP2 := pstrans_to_is_pstrans PP).
assert (X : pstrans_to_pstrans_data PP
=
total_pstrans_data _ _ _ disp_pstrans_linvunitor_data).
- use total2_paths_f.
+ apply idpath.
+ apply funextsec. intro x.
apply funextsec. intro y.
apply funextsec. intro f.
use subtypePath.
{ intro. apply isaprop_is_invertible_2cell. }
apply idpath.
- exact (transportf is_pstrans X PP2).
Definition disp_pstrans_linvunitor
: disp_pstrans
FF
(disp_pseudo_comp _ _ _ _ _ FF (disp_pseudo_id D₂))
(linvunitor_pstrans F)
:= disp_pstrans_linvunitor_data,, disp_pstrans_linvunitor_laws.
Definition disp_runitor_pstrans_data
: disp_pstrans_data
(disp_pseudo_comp _ _ _ _ _ (disp_pseudo_id D₁) FF)
FF
(runitor_pstrans F).
Show proof.
use make_disp_pstrans_data.
- exact (λ x xx, id_disp (FF x xx)).
- cbn.
refine (λ x y f xx yy ff, _).
apply (vcomp_disp_invertible (disp_invertible_2cell_lunitor _)
(disp_invertible_2cell_rinvunitor _)).
- exact (λ x xx, id_disp (FF x xx)).
- cbn.
refine (λ x y f xx yy ff, _).
apply (vcomp_disp_invertible (disp_invertible_2cell_lunitor _)
(disp_invertible_2cell_rinvunitor _)).
Lemma disp_runitor_pstrans_laws : is_disp_pstrans _ _ _ disp_runitor_pstrans_data.
Show proof.
apply is_disp_pstrans_from_total.
pose (PP := runitor_pstrans (total_psfunctor _ _ _ FF)).
pose (PP2 := pstrans_to_is_pstrans PP).
assert (X : pstrans_to_pstrans_data PP
=
total_pstrans_data _ _ _ disp_runitor_pstrans_data).
- use total2_paths_f.
+ apply idpath.
+ apply funextsec. intro x.
apply funextsec. intro y.
apply funextsec. intro f.
use subtypePath.
{ intro. apply isaprop_is_invertible_2cell. }
apply idpath.
- exact (transportf is_pstrans X PP2).
pose (PP := runitor_pstrans (total_psfunctor _ _ _ FF)).
pose (PP2 := pstrans_to_is_pstrans PP).
assert (X : pstrans_to_pstrans_data PP
=
total_pstrans_data _ _ _ disp_runitor_pstrans_data).
- use total2_paths_f.
+ apply idpath.
+ apply funextsec. intro x.
apply funextsec. intro y.
apply funextsec. intro f.
use subtypePath.
{ intro. apply isaprop_is_invertible_2cell. }
apply idpath.
- exact (transportf is_pstrans X PP2).
Definition disp_runitor_pstrans
: disp_pstrans
(disp_pseudo_comp _ _ _ _ _ (disp_pseudo_id D₁) FF)
FF
(runitor_pstrans F)
:= disp_runitor_pstrans_data,, disp_runitor_pstrans_laws.
Definition disp_rinvunitor_pstrans_data
: disp_pstrans_data
FF
(disp_pseudo_comp _ _ _ _ _ (disp_pseudo_id D₁) FF)
(rinvunitor_pstrans F).
Show proof.
use make_disp_pstrans_data.
- exact (λ x xx, id_disp (FF x xx)).
- cbn.
refine (λ x y f xx yy ff, _).
apply (vcomp_disp_invertible (disp_invertible_2cell_lunitor _)
(disp_invertible_2cell_rinvunitor _)).
- exact (λ x xx, id_disp (FF x xx)).
- cbn.
refine (λ x y f xx yy ff, _).
apply (vcomp_disp_invertible (disp_invertible_2cell_lunitor _)
(disp_invertible_2cell_rinvunitor _)).
Lemma disp_rinvunitor_pstrans_laws : is_disp_pstrans _ _ _ disp_rinvunitor_pstrans_data.
Show proof.
apply is_disp_pstrans_from_total.
pose (PP := rinvunitor_pstrans (total_psfunctor _ _ _ FF)).
pose (PP2 := pstrans_to_is_pstrans PP).
assert (X : pstrans_to_pstrans_data PP
=
total_pstrans_data _ _ _ disp_rinvunitor_pstrans_data).
- use total2_paths_f.
+ apply idpath.
+ apply funextsec. intro x.
apply funextsec. intro y.
apply funextsec. intro f.
use subtypePath.
{ intro. apply isaprop_is_invertible_2cell. }
apply idpath.
- exact (transportf is_pstrans X PP2).
pose (PP := rinvunitor_pstrans (total_psfunctor _ _ _ FF)).
pose (PP2 := pstrans_to_is_pstrans PP).
assert (X : pstrans_to_pstrans_data PP
=
total_pstrans_data _ _ _ disp_rinvunitor_pstrans_data).
- use total2_paths_f.
+ apply idpath.
+ apply funextsec. intro x.
apply funextsec. intro y.
apply funextsec. intro f.
use subtypePath.
{ intro. apply isaprop_is_invertible_2cell. }
apply idpath.
- exact (transportf is_pstrans X PP2).
Definition disp_rinvunitor_pstrans
: disp_pstrans
FF
(disp_pseudo_comp _ _ _ _ _ (disp_pseudo_id D₁) FF)
(rinvunitor_pstrans F)
:= disp_rinvunitor_pstrans_data,, disp_rinvunitor_pstrans_laws.
End DispTransUnitality.
Section DispTransAssociativiy.
Context {B₁ B₂ B₃ B₄ : bicat}
{F₁ : psfunctor B₁ B₂}
{F₂ : psfunctor B₂ B₃}
{F₃ : psfunctor B₃ B₄}
{D₁ : disp_bicat B₁} {D₂ : disp_bicat B₂}
{D₃ : disp_bicat B₃} {D₄ : disp_bicat B₄}
(FF₁ : disp_psfunctor D₁ D₂ F₁)
(FF₂ : disp_psfunctor D₂ D₃ F₂)
(FF₃ : disp_psfunctor D₃ D₄ F₃).
Definition disp_lassociator_pstrans_data
: disp_pstrans_data
(disp_pseudo_comp
_ _ _ _ _
(disp_pseudo_comp
_ _ _ _ _
FF₁
FF₂)
FF₃
)
(disp_pseudo_comp
_ _ _ _ _
FF₁
(disp_pseudo_comp
_ _ _ _ _
FF₂
FF₃)
)
(lassociator_pstrans F₁ F₂ F₃).
Show proof.
use make_disp_pstrans_data.
- exact (λ x xx, id_disp (_ x xx)).
- cbn.
refine (λ x y f xx yy ff, _).
apply (vcomp_disp_invertible (disp_invertible_2cell_lunitor _)
(disp_invertible_2cell_rinvunitor _)).
- exact (λ x xx, id_disp (_ x xx)).
- cbn.
refine (λ x y f xx yy ff, _).
apply (vcomp_disp_invertible (disp_invertible_2cell_lunitor _)
(disp_invertible_2cell_rinvunitor _)).
Lemma disp_lassociator_pstrans_laws : is_disp_pstrans _ _ _ disp_lassociator_pstrans_data.
Show proof.
apply is_disp_pstrans_from_total.
pose (PP := lassociator_pstrans
(total_psfunctor _ _ _ FF₁)
(total_psfunctor _ _ _ FF₂)
(total_psfunctor _ _ _ FF₃)).
pose (PP2 := pstrans_to_is_pstrans PP).
assert (X : pstrans_to_pstrans_data PP
=
total_pstrans_data _ _ _ disp_lassociator_pstrans_data).
- use total2_paths_f.
+ apply idpath.
+ apply funextsec. intro x.
apply funextsec. intro y.
apply funextsec. intro f.
use subtypePath.
{ intro. apply isaprop_is_invertible_2cell. }
apply idpath.
- exact (transportf is_pstrans X PP2).
pose (PP := lassociator_pstrans
(total_psfunctor _ _ _ FF₁)
(total_psfunctor _ _ _ FF₂)
(total_psfunctor _ _ _ FF₃)).
pose (PP2 := pstrans_to_is_pstrans PP).
assert (X : pstrans_to_pstrans_data PP
=
total_pstrans_data _ _ _ disp_lassociator_pstrans_data).
- use total2_paths_f.
+ apply idpath.
+ apply funextsec. intro x.
apply funextsec. intro y.
apply funextsec. intro f.
use subtypePath.
{ intro. apply isaprop_is_invertible_2cell. }
apply idpath.
- exact (transportf is_pstrans X PP2).
Definition disp_lassociator_pstrans
: disp_pstrans
(disp_pseudo_comp
_ _ _ _ _
(disp_pseudo_comp
_ _ _ _ _
FF₁
FF₂)
FF₃
)
(disp_pseudo_comp
_ _ _ _ _
FF₁
(disp_pseudo_comp
_ _ _ _ _
FF₂
FF₃)
)
(lassociator_pstrans F₁ F₂ F₃)
:= disp_lassociator_pstrans_data,, disp_lassociator_pstrans_laws.
Definition disp_pstrans_rassociator_data
: disp_pstrans_data
(disp_pseudo_comp
_ _ _ _ _
FF₁
(disp_pseudo_comp
_ _ _ _ _
FF₂
FF₃)
)
(disp_pseudo_comp
_ _ _ _ _
(disp_pseudo_comp
_ _ _ _ _
FF₁
FF₂)
FF₃
)
(rassociator_pstrans F₁ F₂ F₃).
Show proof.
use make_disp_pstrans_data.
- exact (λ x xx, id_disp (_ x xx)).
- cbn.
refine (λ x y f xx yy ff, _).
apply (vcomp_disp_invertible (disp_invertible_2cell_lunitor _)
(disp_invertible_2cell_rinvunitor _)).
- exact (λ x xx, id_disp (_ x xx)).
- cbn.
refine (λ x y f xx yy ff, _).
apply (vcomp_disp_invertible (disp_invertible_2cell_lunitor _)
(disp_invertible_2cell_rinvunitor _)).
Lemma disp_pstrans_rassociator_laws : is_disp_pstrans _ _ _ disp_pstrans_rassociator_data.
Show proof.
apply is_disp_pstrans_from_total.
pose (PP := rassociator_pstrans
(total_psfunctor _ _ _ FF₁)
(total_psfunctor _ _ _ FF₂)
(total_psfunctor _ _ _ FF₃)).
pose (PP2 := pstrans_to_is_pstrans PP).
assert (X : pstrans_to_pstrans_data PP
=
total_pstrans_data _ _ _ disp_lassociator_pstrans_data).
- use total2_paths_f.
+ apply idpath.
+ apply funextsec. intro x.
apply funextsec. intro y.
apply funextsec. intro f.
use subtypePath.
{ intro. apply isaprop_is_invertible_2cell. }
apply idpath.
- exact (transportf is_pstrans X PP2).
pose (PP := rassociator_pstrans
(total_psfunctor _ _ _ FF₁)
(total_psfunctor _ _ _ FF₂)
(total_psfunctor _ _ _ FF₃)).
pose (PP2 := pstrans_to_is_pstrans PP).
assert (X : pstrans_to_pstrans_data PP
=
total_pstrans_data _ _ _ disp_lassociator_pstrans_data).
- use total2_paths_f.
+ apply idpath.
+ apply funextsec. intro x.
apply funextsec. intro y.
apply funextsec. intro f.
use subtypePath.
{ intro. apply isaprop_is_invertible_2cell. }
apply idpath.
- exact (transportf is_pstrans X PP2).
Definition disp_pstrans_rassociator
: disp_pstrans
(disp_pseudo_comp
_ _ _ _ _
FF₁
(disp_pseudo_comp
_ _ _ _ _
FF₂
FF₃)
)
(disp_pseudo_comp
_ _ _ _ _
(disp_pseudo_comp
_ _ _ _ _
FF₁
FF₂)
FF₃
)
(rassociator_pstrans F₁ F₂ F₃)
:= disp_pstrans_rassociator_data,, disp_pstrans_rassociator_laws.
End DispTransAssociativiy.