Library UniMath.Bicategories.DoubleCategories.Examples.SpansDoubleCat
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat.
Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor.
Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos.
Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence.
Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.Spans.
Require Import UniMath.CategoryTheory.limits.pullbacks.
Require Import UniMath.Bicategories.Core.Bicat.
Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats.
Require Import UniMath.Bicategories.DoubleCategories.DoubleCategoryBasics.
Require Import UniMath.Bicategories.DoubleCategories.DoubleFunctor.Basics.
Require Import UniMath.Bicategories.DoubleCategories.DoubleCats.
Local Open Scope cat.
Section SpansDoubleCat.
Context {C : univalent_category}
(PC : Pullbacks C).
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat.
Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor.
Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos.
Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence.
Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.Spans.
Require Import UniMath.CategoryTheory.limits.pullbacks.
Require Import UniMath.Bicategories.Core.Bicat.
Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats.
Require Import UniMath.Bicategories.DoubleCategories.DoubleCategoryBasics.
Require Import UniMath.Bicategories.DoubleCategories.DoubleFunctor.Basics.
Require Import UniMath.Bicategories.DoubleCategories.DoubleCats.
Local Open Scope cat.
Section SpansDoubleCat.
Context {C : univalent_category}
(PC : Pullbacks C).
1. Horizontal identities
Definition spans_double_cat_hor_id_data
: hor_id_data (twosided_disp_cat_of_spans C).
Show proof.
Proposition spans_double_cat_hor_id_laws
: hor_id_laws spans_double_cat_hor_id_data.
Show proof.
Definition spans_double_cat_hor_id
: hor_id (twosided_disp_cat_of_spans C).
Show proof.
: hor_id_data (twosided_disp_cat_of_spans C).
Show proof.
Proposition spans_double_cat_hor_id_laws
: hor_id_laws spans_double_cat_hor_id_data.
Show proof.
split.
- intros a.
use span_sqr_eq ; cbn.
apply idpath.
- intros a₁ a₂ a₃ f g.
use span_sqr_eq ; cbn.
apply idpath.
- intros a.
use span_sqr_eq ; cbn.
apply idpath.
- intros a₁ a₂ a₃ f g.
use span_sqr_eq ; cbn.
apply idpath.
Definition spans_double_cat_hor_id
: hor_id (twosided_disp_cat_of_spans C).
Show proof.
2. Horizontal composition
Definition spans_double_cat_hor_comp_data
: hor_comp_data (twosided_disp_cat_of_spans C).
Show proof.
Proposition spans_double_cat_hor_comp_laws
: hor_comp_laws spans_double_cat_hor_comp_data.
Show proof.
Definition spans_double_cat_hor_comp
: hor_comp (twosided_disp_cat_of_spans C).
Show proof.
: hor_comp_data (twosided_disp_cat_of_spans C).
Show proof.
use make_hor_comp_data.
- exact (λ a₁ a₂ a₃ s t, comp_span C PC s t).
- exact (λ _ _ _ _ _ _ _ _ _ _ _ _ _ s₁ s₂, comp_span_mor C PC s₁ s₂).
- exact (λ a₁ a₂ a₃ s t, comp_span C PC s t).
- exact (λ _ _ _ _ _ _ _ _ _ _ _ _ _ s₁ s₂, comp_span_mor C PC s₁ s₂).
Proposition spans_double_cat_hor_comp_laws
: hor_comp_laws spans_double_cat_hor_comp_data.
Show proof.
split.
- intros a₁ a₂ a₃ h₁ h₂.
use span_sqr_eq.
use (MorphismsIntoPullbackEqual (isPullback_Pullback (PC _ _ _ _ _))) ; cbn.
+ unfold mor_of_comp_span_mor.
rewrite PullbackArrow_PullbackPr1 ; cbn.
rewrite id_left, id_right.
apply idpath.
+ unfold mor_of_comp_span_mor.
rewrite PullbackArrow_PullbackPr2 ; cbn.
rewrite id_left, id_right.
apply idpath.
- intros.
use span_sqr_eq.
use (MorphismsIntoPullbackEqual (isPullback_Pullback (PC _ _ _ _ _))) ; cbn.
+ rewrite !assoc'.
unfold mor_of_comp_span_mor.
rewrite !PullbackArrow_PullbackPr1 ; cbn.
rewrite !assoc.
rewrite !PullbackArrow_PullbackPr1.
rewrite !assoc'.
apply idpath.
+ rewrite !assoc'.
unfold mor_of_comp_span_mor.
rewrite !PullbackArrow_PullbackPr2 ; cbn.
rewrite !assoc.
rewrite !PullbackArrow_PullbackPr2.
rewrite !assoc'.
apply idpath.
- intros a₁ a₂ a₃ h₁ h₂.
use span_sqr_eq.
use (MorphismsIntoPullbackEqual (isPullback_Pullback (PC _ _ _ _ _))) ; cbn.
+ unfold mor_of_comp_span_mor.
rewrite PullbackArrow_PullbackPr1 ; cbn.
rewrite id_left, id_right.
apply idpath.
+ unfold mor_of_comp_span_mor.
rewrite PullbackArrow_PullbackPr2 ; cbn.
rewrite id_left, id_right.
apply idpath.
- intros.
use span_sqr_eq.
use (MorphismsIntoPullbackEqual (isPullback_Pullback (PC _ _ _ _ _))) ; cbn.
+ rewrite !assoc'.
unfold mor_of_comp_span_mor.
rewrite !PullbackArrow_PullbackPr1 ; cbn.
rewrite !assoc.
rewrite !PullbackArrow_PullbackPr1.
rewrite !assoc'.
apply idpath.
+ rewrite !assoc'.
unfold mor_of_comp_span_mor.
rewrite !PullbackArrow_PullbackPr2 ; cbn.
rewrite !assoc.
rewrite !PullbackArrow_PullbackPr2.
rewrite !assoc'.
apply idpath.
Definition spans_double_cat_hor_comp
: hor_comp (twosided_disp_cat_of_spans C).
Show proof.
3. The unitors and associators
Definition spans_double_cat_lunitor_data
: double_lunitor_data
spans_double_cat_hor_id
spans_double_cat_hor_comp.
Show proof.
Proposition spans_double_cat_lunitor_laws
: double_lunitor_laws spans_double_cat_lunitor_data.
Show proof.
Definition spans_double_cat_lunitor
: double_cat_lunitor
spans_double_cat_hor_id
spans_double_cat_hor_comp.
Show proof.
Definition spans_double_cat_runitor_data
: double_runitor_data
spans_double_cat_hor_id
spans_double_cat_hor_comp.
Show proof.
Proposition spans_double_cat_runitor_laws
: double_runitor_laws spans_double_cat_runitor_data.
Show proof.
Definition spans_double_cat_runitor
: double_cat_runitor
spans_double_cat_hor_id
spans_double_cat_hor_comp.
Show proof.
Definition spans_double_cat_associator_data
: double_associator_data spans_double_cat_hor_comp.
Show proof.
Proposition spans_double_cat_associator_laws
: double_associator_laws spans_double_cat_associator_data.
Show proof.
Definition spans_double_cat_associator
: double_cat_associator spans_double_cat_hor_comp.
Show proof.
: double_lunitor_data
spans_double_cat_hor_id
spans_double_cat_hor_comp.
Show proof.
intros x y h.
simple refine (_ ,, _).
- exact (span_lunitor C PC h).
- use is_iso_twosided_disp_span_sqr ; cbn.
apply is_z_iso_span_lunitor_mor.
simple refine (_ ,, _).
- exact (span_lunitor C PC h).
- use is_iso_twosided_disp_span_sqr ; cbn.
apply is_z_iso_span_lunitor_mor.
Proposition spans_double_cat_lunitor_laws
: double_lunitor_laws spans_double_cat_lunitor_data.
Show proof.
intros x₁ x₂ y₁ y₂ h₁ h₂ v₁ v₂ sq.
use span_sqr_eq.
rewrite transportb_disp_mor2_span ; cbn.
unfold span_lunitor_mor, mor_of_comp_span_mor.
rewrite PullbackArrow_PullbackPr2.
apply idpath.
use span_sqr_eq.
rewrite transportb_disp_mor2_span ; cbn.
unfold span_lunitor_mor, mor_of_comp_span_mor.
rewrite PullbackArrow_PullbackPr2.
apply idpath.
Definition spans_double_cat_lunitor
: double_cat_lunitor
spans_double_cat_hor_id
spans_double_cat_hor_comp.
Show proof.
use make_double_lunitor.
- exact spans_double_cat_lunitor_data.
- exact spans_double_cat_lunitor_laws.
- exact spans_double_cat_lunitor_data.
- exact spans_double_cat_lunitor_laws.
Definition spans_double_cat_runitor_data
: double_runitor_data
spans_double_cat_hor_id
spans_double_cat_hor_comp.
Show proof.
intros x y h.
simple refine (_ ,, _).
- exact (span_runitor C PC h).
- use is_iso_twosided_disp_span_sqr ; cbn.
apply is_z_iso_span_runitor_mor.
simple refine (_ ,, _).
- exact (span_runitor C PC h).
- use is_iso_twosided_disp_span_sqr ; cbn.
apply is_z_iso_span_runitor_mor.
Proposition spans_double_cat_runitor_laws
: double_runitor_laws spans_double_cat_runitor_data.
Show proof.
intros x₁ x₂ y₁ y₂ h₁ h₂ v₁ v₂ sq.
use span_sqr_eq.
rewrite transportb_disp_mor2_span ; cbn.
unfold span_runitor_mor, mor_of_comp_span_mor.
rewrite PullbackArrow_PullbackPr1.
apply idpath.
use span_sqr_eq.
rewrite transportb_disp_mor2_span ; cbn.
unfold span_runitor_mor, mor_of_comp_span_mor.
rewrite PullbackArrow_PullbackPr1.
apply idpath.
Definition spans_double_cat_runitor
: double_cat_runitor
spans_double_cat_hor_id
spans_double_cat_hor_comp.
Show proof.
use make_double_runitor.
- exact spans_double_cat_runitor_data.
- exact spans_double_cat_runitor_laws.
- exact spans_double_cat_runitor_data.
- exact spans_double_cat_runitor_laws.
Definition spans_double_cat_associator_data
: double_associator_data spans_double_cat_hor_comp.
Show proof.
intros w x y z h₁ h₂ h₃.
simple refine (_ ,, _).
- exact (span_associator C PC h₁ h₂ h₃).
- use is_iso_twosided_disp_span_sqr ; cbn.
apply is_z_iso_span_associator_mor.
simple refine (_ ,, _).
- exact (span_associator C PC h₁ h₂ h₃).
- use is_iso_twosided_disp_span_sqr ; cbn.
apply is_z_iso_span_associator_mor.
Proposition spans_double_cat_associator_laws
: double_associator_laws spans_double_cat_associator_data.
Show proof.
intros w₁ w₂ x₁ x₂ y₁ y₂ z₁ z₂ h₁ h₂ j₁ j₂ k₁ k₂ vw vx vy vz sq₁ sq₂ sq₃.
use span_sqr_eq.
rewrite transportb_disp_mor2_span ; cbn.
use (MorphismsIntoPullbackEqual (isPullback_Pullback (PC _ _ _ _ _))) ; cbn.
- rewrite !assoc'.
unfold span_associator_mor, mor_of_comp_span_mor ; cbn.
rewrite !PullbackArrow_PullbackPr1.
rewrite !assoc.
rewrite PullbackArrow_PullbackPr1.
unfold mor_of_comp_span_mor.
use (MorphismsIntoPullbackEqual (isPullback_Pullback (PC _ _ _ _ _))) ; cbn.
+ rewrite !assoc'.
rewrite !PullbackArrow_PullbackPr1.
rewrite !assoc.
rewrite PullbackArrow_PullbackPr1.
apply idpath.
+ rewrite !assoc'.
rewrite !PullbackArrow_PullbackPr2.
rewrite !assoc.
rewrite !PullbackArrow_PullbackPr2.
rewrite !assoc'.
rewrite !PullbackArrow_PullbackPr1.
apply idpath.
- rewrite !assoc'.
unfold span_associator_mor, mor_of_comp_span_mor ; cbn.
rewrite !PullbackArrow_PullbackPr2.
rewrite !assoc.
rewrite !PullbackArrow_PullbackPr2.
rewrite !assoc'.
apply maponpaths.
unfold mor_of_comp_span_mor.
rewrite !PullbackArrow_PullbackPr2.
apply idpath.
use span_sqr_eq.
rewrite transportb_disp_mor2_span ; cbn.
use (MorphismsIntoPullbackEqual (isPullback_Pullback (PC _ _ _ _ _))) ; cbn.
- rewrite !assoc'.
unfold span_associator_mor, mor_of_comp_span_mor ; cbn.
rewrite !PullbackArrow_PullbackPr1.
rewrite !assoc.
rewrite PullbackArrow_PullbackPr1.
unfold mor_of_comp_span_mor.
use (MorphismsIntoPullbackEqual (isPullback_Pullback (PC _ _ _ _ _))) ; cbn.
+ rewrite !assoc'.
rewrite !PullbackArrow_PullbackPr1.
rewrite !assoc.
rewrite PullbackArrow_PullbackPr1.
apply idpath.
+ rewrite !assoc'.
rewrite !PullbackArrow_PullbackPr2.
rewrite !assoc.
rewrite !PullbackArrow_PullbackPr2.
rewrite !assoc'.
rewrite !PullbackArrow_PullbackPr1.
apply idpath.
- rewrite !assoc'.
unfold span_associator_mor, mor_of_comp_span_mor ; cbn.
rewrite !PullbackArrow_PullbackPr2.
rewrite !assoc.
rewrite !PullbackArrow_PullbackPr2.
rewrite !assoc'.
apply maponpaths.
unfold mor_of_comp_span_mor.
rewrite !PullbackArrow_PullbackPr2.
apply idpath.
Definition spans_double_cat_associator
: double_cat_associator spans_double_cat_hor_comp.
Show proof.
use make_double_associator.
- exact spans_double_cat_associator_data.
- exact spans_double_cat_associator_laws.
- exact spans_double_cat_associator_data.
- exact spans_double_cat_associator_laws.
4. The triangle and pentagon equations
Proposition spans_double_cat_triangle
: triangle_law
spans_double_cat_lunitor
spans_double_cat_runitor
spans_double_cat_associator.
Show proof.
Proposition spans_double_cat_pentagon
: pentagon_law spans_double_cat_associator.
Show proof.
: triangle_law
spans_double_cat_lunitor
spans_double_cat_runitor
spans_double_cat_associator.
Show proof.
intro ; intros.
use span_sqr_eq.
rewrite transportb_disp_mor2_span ; cbn.
use (MorphismsIntoPullbackEqual (isPullback_Pullback (PC _ _ _ _ _))) ; cbn.
- unfold span_associator_mor, mor_of_comp_span_mor ; cbn.
rewrite !assoc'.
rewrite !PullbackArrow_PullbackPr1.
rewrite !assoc.
rewrite PullbackArrow_PullbackPr1.
unfold span_runitor_mor.
rewrite PullbackArrow_PullbackPr1, id_right.
apply idpath.
- unfold span_associator_mor, mor_of_comp_span_mor ; cbn.
rewrite !assoc'.
rewrite !PullbackArrow_PullbackPr2.
rewrite !assoc.
rewrite PullbackArrow_PullbackPr2.
refine (id_right _ @ _).
apply idpath.
use span_sqr_eq.
rewrite transportb_disp_mor2_span ; cbn.
use (MorphismsIntoPullbackEqual (isPullback_Pullback (PC _ _ _ _ _))) ; cbn.
- unfold span_associator_mor, mor_of_comp_span_mor ; cbn.
rewrite !assoc'.
rewrite !PullbackArrow_PullbackPr1.
rewrite !assoc.
rewrite PullbackArrow_PullbackPr1.
unfold span_runitor_mor.
rewrite PullbackArrow_PullbackPr1, id_right.
apply idpath.
- unfold span_associator_mor, mor_of_comp_span_mor ; cbn.
rewrite !assoc'.
rewrite !PullbackArrow_PullbackPr2.
rewrite !assoc.
rewrite PullbackArrow_PullbackPr2.
refine (id_right _ @ _).
apply idpath.
Proposition spans_double_cat_pentagon
: pentagon_law spans_double_cat_associator.
Show proof.
intro ; intros.
use span_sqr_eq.
rewrite transportb_disp_mor2_span ; cbn.
use (MorphismsIntoPullbackEqual (isPullback_Pullback (PC _ _ _ _ _))) ; cbn.
- unfold span_associator_mor, mor_of_comp_span_mor ; cbn.
rewrite !assoc'.
rewrite !PullbackArrow_PullbackPr1.
use (MorphismsIntoPullbackEqual (isPullback_Pullback (PC _ _ _ _ _))) ; cbn.
+ rewrite !assoc'.
unfold span_associator_mor.
rewrite !PullbackArrow_PullbackPr1.
refine (!_).
etrans.
{
apply maponpaths.
refine (assoc _ _ _ @ _).
rewrite PullbackArrow_PullbackPr1.
apply idpath.
}
use (MorphismsIntoPullbackEqual (isPullback_Pullback (PC _ _ _ _ _))) ; cbn.
* rewrite !assoc'.
rewrite !PullbackArrow_PullbackPr1.
apply id_right.
* rewrite !assoc'.
rewrite !PullbackArrow_PullbackPr2.
etrans.
{
apply maponpaths.
refine (assoc _ _ _ @ _).
rewrite !PullbackArrow_PullbackPr2.
apply idpath.
}
rewrite !assoc.
rewrite !PullbackArrow_PullbackPr2.
rewrite !assoc'.
apply maponpaths.
rewrite !assoc.
rewrite !PullbackArrow_PullbackPr1.
apply idpath.
+ rewrite !assoc'.
unfold span_associator_mor.
rewrite !PullbackArrow_PullbackPr2.
refine (!_).
etrans.
{
apply maponpaths.
refine (assoc _ _ _ @ _).
rewrite PullbackArrow_PullbackPr1.
refine (assoc _ _ _ @ _).
rewrite PullbackArrow_PullbackPr2.
apply idpath.
}
rewrite !assoc.
rewrite !PullbackArrow_PullbackPr2.
rewrite !assoc'.
apply maponpaths.
rewrite !assoc.
rewrite PullbackArrow_PullbackPr1.
rewrite PullbackArrow_PullbackPr2.
apply idpath.
- unfold span_associator_mor, mor_of_comp_span_mor.
rewrite !assoc'.
rewrite !PullbackArrow_PullbackPr2.
rewrite !assoc.
rewrite !PullbackArrow_PullbackPr2.
rewrite !assoc'.
refine (!_).
etrans.
{
apply maponpaths.
refine (assoc _ _ _ @ _).
rewrite PullbackArrow_PullbackPr2.
apply idpath.
}
rewrite !assoc.
unfold span_sqr_ob_mor ; cbn.
rewrite id_right.
rewrite PullbackArrow_PullbackPr2.
unfold span_associator_mor .
rewrite !assoc'.
rewrite PullbackArrow_PullbackPr2.
apply idpath.
use span_sqr_eq.
rewrite transportb_disp_mor2_span ; cbn.
use (MorphismsIntoPullbackEqual (isPullback_Pullback (PC _ _ _ _ _))) ; cbn.
- unfold span_associator_mor, mor_of_comp_span_mor ; cbn.
rewrite !assoc'.
rewrite !PullbackArrow_PullbackPr1.
use (MorphismsIntoPullbackEqual (isPullback_Pullback (PC _ _ _ _ _))) ; cbn.
+ rewrite !assoc'.
unfold span_associator_mor.
rewrite !PullbackArrow_PullbackPr1.
refine (!_).
etrans.
{
apply maponpaths.
refine (assoc _ _ _ @ _).
rewrite PullbackArrow_PullbackPr1.
apply idpath.
}
use (MorphismsIntoPullbackEqual (isPullback_Pullback (PC _ _ _ _ _))) ; cbn.
* rewrite !assoc'.
rewrite !PullbackArrow_PullbackPr1.
apply id_right.
* rewrite !assoc'.
rewrite !PullbackArrow_PullbackPr2.
etrans.
{
apply maponpaths.
refine (assoc _ _ _ @ _).
rewrite !PullbackArrow_PullbackPr2.
apply idpath.
}
rewrite !assoc.
rewrite !PullbackArrow_PullbackPr2.
rewrite !assoc'.
apply maponpaths.
rewrite !assoc.
rewrite !PullbackArrow_PullbackPr1.
apply idpath.
+ rewrite !assoc'.
unfold span_associator_mor.
rewrite !PullbackArrow_PullbackPr2.
refine (!_).
etrans.
{
apply maponpaths.
refine (assoc _ _ _ @ _).
rewrite PullbackArrow_PullbackPr1.
refine (assoc _ _ _ @ _).
rewrite PullbackArrow_PullbackPr2.
apply idpath.
}
rewrite !assoc.
rewrite !PullbackArrow_PullbackPr2.
rewrite !assoc'.
apply maponpaths.
rewrite !assoc.
rewrite PullbackArrow_PullbackPr1.
rewrite PullbackArrow_PullbackPr2.
apply idpath.
- unfold span_associator_mor, mor_of_comp_span_mor.
rewrite !assoc'.
rewrite !PullbackArrow_PullbackPr2.
rewrite !assoc.
rewrite !PullbackArrow_PullbackPr2.
rewrite !assoc'.
refine (!_).
etrans.
{
apply maponpaths.
refine (assoc _ _ _ @ _).
rewrite PullbackArrow_PullbackPr2.
apply idpath.
}
rewrite !assoc.
unfold span_sqr_ob_mor ; cbn.
rewrite id_right.
rewrite PullbackArrow_PullbackPr2.
unfold span_associator_mor .
rewrite !assoc'.
rewrite PullbackArrow_PullbackPr2.
apply idpath.
5. The double category of spans
Definition spans_double_cat
: double_cat.
Show proof.
: double_cat.
Show proof.
use make_double_cat.
- exact C.
- exact (twosided_disp_cat_of_spans C).
- exact spans_double_cat_hor_id.
- exact spans_double_cat_hor_comp.
- exact spans_double_cat_lunitor.
- exact spans_double_cat_runitor.
- exact spans_double_cat_associator.
- exact spans_double_cat_triangle.
- exact spans_double_cat_pentagon.
- apply univalent_category_is_univalent.
- use is_univalent_spans_twosided_disp_cat.
apply univalent_category_is_univalent.
End SpansDoubleCat.- exact C.
- exact (twosided_disp_cat_of_spans C).
- exact spans_double_cat_hor_id.
- exact spans_double_cat_hor_comp.
- exact spans_double_cat_lunitor.
- exact spans_double_cat_runitor.
- exact spans_double_cat_associator.
- exact spans_double_cat_triangle.
- exact spans_double_cat_pentagon.
- apply univalent_category_is_univalent.
- use is_univalent_spans_twosided_disp_cat.
apply univalent_category_is_univalent.