Library UniMath.Bicategories.WkCatEnrichment.hcomp_bicat
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.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.Bicategories.WkCatEnrichment.prebicategory.
Require Import UniMath.Bicategories.Core.Bicat.
Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.BicategoryLaws.
Local Open Scope cat.
Definition hcomp_bicat_data
: UU
:= ∑ (ob : UU)
(mor : ob → ob → UU)
(cell : ∏ (x y : ob), mor x y → mor x y → UU)
(id1 : ∏ (x : ob), mor x x)
(comp1 : ∏ (x y z : ob), mor x y → mor y z → mor x z),
(∏ (x y : ob) (f : mor x y), cell _ _ f f)
× (∏ (x y : ob) (f g h : mor x y),
cell _ _ f g → cell _ _ g h → cell _ _ f h)
× (∏ (x y : ob) (f : mor x y),
cell _ _ (comp1 _ _ _ f (id1 y)) f)
× (∏ (x y : ob) (f : mor x y),
cell _ _ f (comp1 _ _ _ f (id1 y)))
× (∏ (x y : ob) (f : mor x y),
cell _ _ (comp1 _ _ _ (id1 x) f) f)
× (∏ (x y : ob) (f : mor x y),
cell _ _ f (comp1 _ _ _ (id1 x) f))
× (∏ (w x y z : ob) (f : mor w x) (g : mor x y) (h : mor y z),
cell _ _
(comp1 _ _ _ (comp1 _ _ _ f g) h)
(comp1 _ _ _ f (comp1 _ _ _ g h)))
× (∏ (w x y z : ob) (f : mor w x) (g : mor x y) (h : mor y z),
cell _ _
(comp1 _ _ _ f (comp1 _ _ _ g h))
(comp1 _ _ _ (comp1 _ _ _ f g) h))
× (∏ (x y z : ob) (f₁ f₂ : mor x y) (g₁ g₂ : mor y z),
cell _ _ f₁ f₂
→ cell _ _ g₁ g₂
→ cell _ _ (comp1 _ _ _ f₁ g₁) (comp1 _ _ _ f₂ g₂)).
Coercion hcomp_bicat_ob
(B : hcomp_bicat_data)
: UU
:= pr1 B.
Definition hb_mor
{B : hcomp_bicat_data}
(b₁ b₂ : B)
: UU
:= pr12 B b₁ b₂.
Definition hb_cell
{B : hcomp_bicat_data}
{b₁ b₂ : B}
(f g : hb_mor b₁ b₂)
: UU
:= pr122 B _ _ f g.
Definition hb_id1
{B : hcomp_bicat_data}
(b : B)
: hb_mor b b
:= pr1 (pr222 B) b .
Definition hb_comp1
{B : hcomp_bicat_data}
{b₁ b₂ b₃ : B}
(f : hb_mor b₁ b₂)
(g : hb_mor b₂ b₃)
: hb_mor b₁ b₃
:= pr12 (pr222 B) _ _ _ f g.
Definition hb_id2
{B : hcomp_bicat_data}
{b₁ b₂ : B}
(f : hb_mor b₁ b₂)
: hb_cell f f
:= pr122 (pr222 B) _ _ f.
Definition hb_vcomp
{B : hcomp_bicat_data}
{b₁ b₂ : B}
{f g h : hb_mor b₁ b₂}
(α : hb_cell f g)
(β : hb_cell g h)
: hb_cell f h
:= pr1 (pr222 (pr222 B)) _ _ _ _ _ α β.
Definition hb_runit
{B : hcomp_bicat_data}
{b₁ b₂ : B}
(f : hb_mor b₁ b₂)
: hb_cell (hb_comp1 f (hb_id1 b₂)) f
:= pr12 (pr222 (pr222 B)) _ _ f.
Definition hb_rinvunit
{B : hcomp_bicat_data}
{b₁ b₂ : B}
(f : hb_mor b₁ b₂)
: hb_cell f (hb_comp1 f (hb_id1 b₂))
:= pr122 (pr222 (pr222 B)) _ _ f.
Definition hb_lunit
{B : hcomp_bicat_data}
{b₁ b₂ : B}
(f : hb_mor b₁ b₂)
: hb_cell (hb_comp1 (hb_id1 b₁) f) f
:= pr1 (pr222 (pr222 (pr222 B))) _ _ f.
Definition hb_linvunit
{B : hcomp_bicat_data}
{b₁ b₂ : B}
(f : hb_mor b₁ b₂)
: hb_cell f (hb_comp1 (hb_id1 b₁) f)
:= pr12 (pr222 (pr222 (pr222 B))) _ _ f.
Definition hb_lassoc
{B : hcomp_bicat_data}
{b₁ b₂ b₃ b₄ : B}
(f : hb_mor b₁ b₂)
(g : hb_mor b₂ b₃)
(h : hb_mor b₃ b₄)
: hb_cell (hb_comp1 (hb_comp1 f g) h) (hb_comp1 f (hb_comp1 g h))
:= pr122 (pr222 (pr222 (pr222 B))) _ _ _ _ f g h.
Definition hb_rassoc
{B : hcomp_bicat_data}
{b₁ b₂ b₃ b₄ : B}
(f : hb_mor b₁ b₂)
(g : hb_mor b₂ b₃)
(h : hb_mor b₃ b₄)
: hb_cell (hb_comp1 f (hb_comp1 g h)) (hb_comp1 (hb_comp1 f g) h)
:= pr1 (pr222 (pr222 (pr222 (pr222 B)))) _ _ _ _ f g h.
Definition hb_hcomp
{B : hcomp_bicat_data}
{b₁ b₂ b₃ : B}
{f₁ f₂ : hb_mor b₁ b₂}
{g₁ g₂ : hb_mor b₂ b₃}
(α : hb_cell f₁ f₂)
(β : hb_cell g₁ g₂)
: hb_cell (hb_comp1 f₁ g₁) (hb_comp1 f₂ g₂)
:= pr2 (pr222 (pr222 (pr222 (pr222 B)))) _ _ _ _ _ _ _ α β.
Definition hcomp_bicat_laws
(B : hcomp_bicat_data)
: UU
:= (∏ (b₁ b₂ : B)
(f g : hb_mor b₁ b₂)
(α : hb_cell f g),
hb_vcomp (hb_id2 _) α = α)
× (∏ (b₁ b₂ : B)
(f g : hb_mor b₁ b₂)
(α : hb_cell f g),
hb_vcomp α (hb_id2 _) = α)
× (∏ (b₁ b₂ : B)
(f₁ f₂ f₃ f₄ : hb_mor b₁ b₂)
(α : hb_cell f₁ f₂)
(β : hb_cell f₂ f₃)
(γ : hb_cell f₃ f₄),
hb_vcomp α (hb_vcomp β γ) = hb_vcomp (hb_vcomp α β) γ)
× (∏ (b₁ b₂ : B)
(f₁ f₂ f₃ f₄ : hb_mor b₁ b₂)
(α : hb_cell f₁ f₂)
(β : hb_cell f₂ f₃)
(γ : hb_cell f₃ f₄),
hb_vcomp (hb_vcomp α β) γ = hb_vcomp α (hb_vcomp β γ))
× (∏ (b₁ b₂ : B)
(f g : hb_mor b₁ b₂),
isaset (hb_cell f g))
× (∏ (b₁ b₂ b₃ : B)
(f : hb_mor b₁ b₂)
(g : hb_mor b₂ b₃),
hb_hcomp (hb_id2 f) (hb_id2 g)
=
hb_id2 (hb_comp1 f g))
× (∏ (b₁ b₂ b₃ : B)
(f₁ g₁ h₁ : hb_mor b₁ b₂)
(f₂ g₂ h₂ : hb_mor b₂ b₃)
(α₁ : hb_cell f₁ g₁)
(α₂ : hb_cell f₂ g₂)
(β₁ : hb_cell g₁ h₁)
(β₂ : hb_cell g₂ h₂),
hb_hcomp (hb_vcomp α₁ β₁) (hb_vcomp α₂ β₂)
=
hb_vcomp (hb_hcomp α₁ α₂) (hb_hcomp β₁ β₂))
× (∏ (a b c d : B)
(f₁ f₂ : hb_mor a b)
(g₁ g₂ : hb_mor b c)
(h₁ h₂ : hb_mor c d)
(α₁ : hb_cell f₁ f₂)
(α₂ : hb_cell g₁ g₂)
(α₃ : hb_cell h₁ h₂),
hb_vcomp
(hb_hcomp α₁ (hb_hcomp α₂ α₃))
(hb_rassoc _ _ _)
=
hb_vcomp
(hb_rassoc _ _ _)
(hb_hcomp (hb_hcomp α₁ α₂) α₃))
× (∏ (a b : B)
(f₁ f₂ : hb_mor a b)
(α : hb_cell f₁ f₂),
hb_vcomp (hb_hcomp (hb_id2 (hb_id1 a)) α) (hb_lunit f₂)
=
hb_vcomp (hb_lunit f₁) α)
× (∏ (a b : B)
(f₁ f₂ : hb_mor a b)
(α : hb_cell f₁ f₂),
hb_vcomp (hb_hcomp α (hb_id2 (hb_id1 b))) (hb_runit f₂)
=
hb_vcomp (hb_runit f₁) α)
× (∏ (b₁ b₂ b₃ b₄ : B)
(f : hb_mor b₁ b₂)
(g : hb_mor b₂ b₃)
(h : hb_mor b₃ b₄),
hb_vcomp
(hb_rassoc f g h)
(hb_lassoc f g h)
=
hb_id2 _)
× (∏ (b₁ b₂ b₃ b₄ : B)
(f : hb_mor b₁ b₂)
(g : hb_mor b₂ b₃)
(h : hb_mor b₃ b₄),
hb_vcomp
(hb_lassoc f g h)
(hb_rassoc f g h)
=
hb_id2 _)
× (∏ (b₁ b₂ : B)
(f : hb_mor b₁ b₂),
hb_vcomp
(hb_lunit f)
(hb_linvunit f)
=
hb_id2 _)
× (∏ (b₁ b₂ : B)
(f : hb_mor b₁ b₂),
hb_vcomp
(hb_linvunit f)
(hb_lunit f)
=
hb_id2 _)
× (∏ (b₁ b₂ : B)
(f : hb_mor b₁ b₂),
hb_vcomp
(hb_runit f)
(hb_rinvunit f)
=
hb_id2 _)
× (∏ (b₁ b₂ : B)
(f : hb_mor b₁ b₂),
hb_vcomp
(hb_rinvunit f)
(hb_runit f)
=
hb_id2 _)
× (∏ (a b c d e : B)
(k : hb_mor a b)
(h : hb_mor b c)
(g : hb_mor c d)
(f : hb_mor d e),
hb_vcomp
(hb_rassoc k h (hb_comp1 g f))
(hb_rassoc (hb_comp1 k h) g f)
=
hb_vcomp
(hb_vcomp
(hb_hcomp (hb_id2 k) (hb_rassoc h g f))
(hb_rassoc k (hb_comp1 h g) f))
(hb_hcomp (hb_rassoc k h g) (hb_id2 f)))
× (∏ (a b c : B)
(f : hb_mor a b)
(g : hb_mor b c),
hb_hcomp (hb_id2 f) (hb_lunit g)
=
hb_vcomp
(hb_rassoc f (hb_id1 b) g)
(hb_hcomp (hb_runit f) (hb_id2 g))).
Lemma isaprop_hcomp_prebicat_laws
(B : hcomp_bicat_data)
(H : ∏ (a b : B) (f g : hb_mor a b), isaset (hb_cell f g))
: isaprop (hcomp_bicat_laws B).
Show proof.
Definition hcomp_bicat
: UU
:= ∑ (B : hcomp_bicat_data), hcomp_bicat_laws B.
Coercion hcomp_bicat_to_data
(B : hcomp_bicat)
: hcomp_bicat_data
:= pr1 B.
Definition hcomp_bicat_hom_cat
(B : hcomp_bicat)
(b₁ b₂ : B)
: category.
Show proof.
Definition hcomp_bicat_hcomp
(B : hcomp_bicat)
(b₁ b₂ b₃ : pr11 B)
: precategory_binproduct_data
(hcomp_bicat_hom_cat B b₁ b₂)
(hcomp_bicat_hom_cat B b₂ b₃)
⟶
hcomp_bicat_hom_cat B b₁ b₃.
Show proof.
Definition hcomp_bicat_to_prebicategory_ob_hom
(B : hcomp_bicat)
: prebicategory_ob_hom.
Show proof.
Definition hcomp_bicat_to_prebicategory_id_comp
(B : hcomp_bicat)
: prebicategory_id_comp.
Show proof.
Definition hcomp_bicat_associator
(B : hcomp_bicat)
(a b c d : hcomp_bicat_to_prebicategory_id_comp B)
: associator_trans_type a b c d.
Show proof.
Definition hcomp_bicat_lunitor
(B : hcomp_bicat)
(a b : hcomp_bicat_to_prebicategory_id_comp B)
: left_unitor_trans_type a b.
Show proof.
Definition hcomp_bicat_runitor
(B : hcomp_bicat)
(a b : hcomp_bicat_to_prebicategory_id_comp B)
: right_unitor_trans_type a b.
Show proof.
Definition hcomp_bicat_to_prebicategory_data
(B : hcomp_bicat)
: prebicategory_data.
Show proof.
Definition hcomp_bicat_is_prebicategory
(B : hcomp_bicat)
: is_prebicategory (hcomp_bicat_to_prebicategory_data B).
Show proof.
Definition hcomp_bicat_to_prebicategory
(B : hcomp_bicat)
: prebicategory.
Show proof.
Definition prebicategory_to_hcomp_bicat_data
(B : prebicategory)
: hcomp_bicat_data.
Show proof.
Definition prebicategory_to_hcomp_bicat
(B : prebicategory)
: hcomp_bicat.
Show proof.
Definition hcomp_bicat_weq_prebicategory
: hcomp_bicat ≃ prebicategory.
Show proof.
Definition hcomp_bicat_to_precategory_ob_mor
(B : hcomp_bicat)
: precategory_ob_mor.
Show proof.
Definition hcomp_bicat_to_precategory_id_comp
(B : hcomp_bicat)
: precategory_id_comp (hcomp_bicat_to_precategory_ob_mor B).
Show proof.
Definition hcomp_bicat_to_precategory_data
(B : hcomp_bicat)
: precategory_data.
Show proof.
Definition hcomp_bicat_to_prebicat_1_id_comp_cells
(B : hcomp_bicat)
: prebicat_1_id_comp_cells.
Show proof.
Definition hcomp_bicat_to_prebicat_2_id_comp_struct
(B : hcomp_bicat)
: prebicat_2_id_comp_struct (hcomp_bicat_to_prebicat_1_id_comp_cells B).
Show proof.
Definition hcomp_bicat_to_prebicat_data
(B : hcomp_bicat)
: prebicat_data.
Show proof.
Definition hcomp_bicat_to_prebicat_laws
(B : hcomp_bicat)
: prebicat_laws (hcomp_bicat_to_prebicat_data B).
Show proof.
Definition hcomp_bicat_to_prebicat
(B : hcomp_bicat)
: prebicat.
Show proof.
Definition hcomp_bicat_to_bicat
(B : hcomp_bicat)
: bicat.
Show proof.
Definition bicat_to_hcomp_bicat_data
(B : bicat)
: hcomp_bicat_data.
Show proof.
Definition bicat_to_hcomp_bicat_laws
(B : bicat)
: hcomp_bicat_laws (bicat_to_hcomp_bicat_data B).
Show proof.
Definition bicat_to_hcomp_bicat
(B : bicat)
: hcomp_bicat.
Show proof.
Definition hcomp_bicat_to_bicat_to_hcomp_bicat
(B : hcomp_bicat)
: bicat_to_hcomp_bicat (hcomp_bicat_to_bicat B) = B.
Show proof.
Definition bicat_to_hcomp_bicat_to_bicat
(B : bicat)
: hcomp_bicat_to_bicat (bicat_to_hcomp_bicat B) = B.
Show proof.
Definition hcomp_bicat_weq_bicat
: hcomp_bicat ≃ bicat.
Show proof.
Definition weq_bicat_prebicategory : bicat ≃ prebicategory.
Show proof.
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.PrecategoryBinProduct.
Require Import UniMath.Bicategories.WkCatEnrichment.prebicategory.
Require Import UniMath.Bicategories.Core.Bicat.
Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.BicategoryLaws.
Local Open Scope cat.
Definition hcomp_bicat_data
: UU
:= ∑ (ob : UU)
(mor : ob → ob → UU)
(cell : ∏ (x y : ob), mor x y → mor x y → UU)
(id1 : ∏ (x : ob), mor x x)
(comp1 : ∏ (x y z : ob), mor x y → mor y z → mor x z),
(∏ (x y : ob) (f : mor x y), cell _ _ f f)
× (∏ (x y : ob) (f g h : mor x y),
cell _ _ f g → cell _ _ g h → cell _ _ f h)
× (∏ (x y : ob) (f : mor x y),
cell _ _ (comp1 _ _ _ f (id1 y)) f)
× (∏ (x y : ob) (f : mor x y),
cell _ _ f (comp1 _ _ _ f (id1 y)))
× (∏ (x y : ob) (f : mor x y),
cell _ _ (comp1 _ _ _ (id1 x) f) f)
× (∏ (x y : ob) (f : mor x y),
cell _ _ f (comp1 _ _ _ (id1 x) f))
× (∏ (w x y z : ob) (f : mor w x) (g : mor x y) (h : mor y z),
cell _ _
(comp1 _ _ _ (comp1 _ _ _ f g) h)
(comp1 _ _ _ f (comp1 _ _ _ g h)))
× (∏ (w x y z : ob) (f : mor w x) (g : mor x y) (h : mor y z),
cell _ _
(comp1 _ _ _ f (comp1 _ _ _ g h))
(comp1 _ _ _ (comp1 _ _ _ f g) h))
× (∏ (x y z : ob) (f₁ f₂ : mor x y) (g₁ g₂ : mor y z),
cell _ _ f₁ f₂
→ cell _ _ g₁ g₂
→ cell _ _ (comp1 _ _ _ f₁ g₁) (comp1 _ _ _ f₂ g₂)).
Coercion hcomp_bicat_ob
(B : hcomp_bicat_data)
: UU
:= pr1 B.
Definition hb_mor
{B : hcomp_bicat_data}
(b₁ b₂ : B)
: UU
:= pr12 B b₁ b₂.
Definition hb_cell
{B : hcomp_bicat_data}
{b₁ b₂ : B}
(f g : hb_mor b₁ b₂)
: UU
:= pr122 B _ _ f g.
Definition hb_id1
{B : hcomp_bicat_data}
(b : B)
: hb_mor b b
:= pr1 (pr222 B) b .
Definition hb_comp1
{B : hcomp_bicat_data}
{b₁ b₂ b₃ : B}
(f : hb_mor b₁ b₂)
(g : hb_mor b₂ b₃)
: hb_mor b₁ b₃
:= pr12 (pr222 B) _ _ _ f g.
Definition hb_id2
{B : hcomp_bicat_data}
{b₁ b₂ : B}
(f : hb_mor b₁ b₂)
: hb_cell f f
:= pr122 (pr222 B) _ _ f.
Definition hb_vcomp
{B : hcomp_bicat_data}
{b₁ b₂ : B}
{f g h : hb_mor b₁ b₂}
(α : hb_cell f g)
(β : hb_cell g h)
: hb_cell f h
:= pr1 (pr222 (pr222 B)) _ _ _ _ _ α β.
Definition hb_runit
{B : hcomp_bicat_data}
{b₁ b₂ : B}
(f : hb_mor b₁ b₂)
: hb_cell (hb_comp1 f (hb_id1 b₂)) f
:= pr12 (pr222 (pr222 B)) _ _ f.
Definition hb_rinvunit
{B : hcomp_bicat_data}
{b₁ b₂ : B}
(f : hb_mor b₁ b₂)
: hb_cell f (hb_comp1 f (hb_id1 b₂))
:= pr122 (pr222 (pr222 B)) _ _ f.
Definition hb_lunit
{B : hcomp_bicat_data}
{b₁ b₂ : B}
(f : hb_mor b₁ b₂)
: hb_cell (hb_comp1 (hb_id1 b₁) f) f
:= pr1 (pr222 (pr222 (pr222 B))) _ _ f.
Definition hb_linvunit
{B : hcomp_bicat_data}
{b₁ b₂ : B}
(f : hb_mor b₁ b₂)
: hb_cell f (hb_comp1 (hb_id1 b₁) f)
:= pr12 (pr222 (pr222 (pr222 B))) _ _ f.
Definition hb_lassoc
{B : hcomp_bicat_data}
{b₁ b₂ b₃ b₄ : B}
(f : hb_mor b₁ b₂)
(g : hb_mor b₂ b₃)
(h : hb_mor b₃ b₄)
: hb_cell (hb_comp1 (hb_comp1 f g) h) (hb_comp1 f (hb_comp1 g h))
:= pr122 (pr222 (pr222 (pr222 B))) _ _ _ _ f g h.
Definition hb_rassoc
{B : hcomp_bicat_data}
{b₁ b₂ b₃ b₄ : B}
(f : hb_mor b₁ b₂)
(g : hb_mor b₂ b₃)
(h : hb_mor b₃ b₄)
: hb_cell (hb_comp1 f (hb_comp1 g h)) (hb_comp1 (hb_comp1 f g) h)
:= pr1 (pr222 (pr222 (pr222 (pr222 B)))) _ _ _ _ f g h.
Definition hb_hcomp
{B : hcomp_bicat_data}
{b₁ b₂ b₃ : B}
{f₁ f₂ : hb_mor b₁ b₂}
{g₁ g₂ : hb_mor b₂ b₃}
(α : hb_cell f₁ f₂)
(β : hb_cell g₁ g₂)
: hb_cell (hb_comp1 f₁ g₁) (hb_comp1 f₂ g₂)
:= pr2 (pr222 (pr222 (pr222 (pr222 B)))) _ _ _ _ _ _ _ α β.
Definition hcomp_bicat_laws
(B : hcomp_bicat_data)
: UU
:= (∏ (b₁ b₂ : B)
(f g : hb_mor b₁ b₂)
(α : hb_cell f g),
hb_vcomp (hb_id2 _) α = α)
× (∏ (b₁ b₂ : B)
(f g : hb_mor b₁ b₂)
(α : hb_cell f g),
hb_vcomp α (hb_id2 _) = α)
× (∏ (b₁ b₂ : B)
(f₁ f₂ f₃ f₄ : hb_mor b₁ b₂)
(α : hb_cell f₁ f₂)
(β : hb_cell f₂ f₃)
(γ : hb_cell f₃ f₄),
hb_vcomp α (hb_vcomp β γ) = hb_vcomp (hb_vcomp α β) γ)
× (∏ (b₁ b₂ : B)
(f₁ f₂ f₃ f₄ : hb_mor b₁ b₂)
(α : hb_cell f₁ f₂)
(β : hb_cell f₂ f₃)
(γ : hb_cell f₃ f₄),
hb_vcomp (hb_vcomp α β) γ = hb_vcomp α (hb_vcomp β γ))
× (∏ (b₁ b₂ : B)
(f g : hb_mor b₁ b₂),
isaset (hb_cell f g))
× (∏ (b₁ b₂ b₃ : B)
(f : hb_mor b₁ b₂)
(g : hb_mor b₂ b₃),
hb_hcomp (hb_id2 f) (hb_id2 g)
=
hb_id2 (hb_comp1 f g))
× (∏ (b₁ b₂ b₃ : B)
(f₁ g₁ h₁ : hb_mor b₁ b₂)
(f₂ g₂ h₂ : hb_mor b₂ b₃)
(α₁ : hb_cell f₁ g₁)
(α₂ : hb_cell f₂ g₂)
(β₁ : hb_cell g₁ h₁)
(β₂ : hb_cell g₂ h₂),
hb_hcomp (hb_vcomp α₁ β₁) (hb_vcomp α₂ β₂)
=
hb_vcomp (hb_hcomp α₁ α₂) (hb_hcomp β₁ β₂))
× (∏ (a b c d : B)
(f₁ f₂ : hb_mor a b)
(g₁ g₂ : hb_mor b c)
(h₁ h₂ : hb_mor c d)
(α₁ : hb_cell f₁ f₂)
(α₂ : hb_cell g₁ g₂)
(α₃ : hb_cell h₁ h₂),
hb_vcomp
(hb_hcomp α₁ (hb_hcomp α₂ α₃))
(hb_rassoc _ _ _)
=
hb_vcomp
(hb_rassoc _ _ _)
(hb_hcomp (hb_hcomp α₁ α₂) α₃))
× (∏ (a b : B)
(f₁ f₂ : hb_mor a b)
(α : hb_cell f₁ f₂),
hb_vcomp (hb_hcomp (hb_id2 (hb_id1 a)) α) (hb_lunit f₂)
=
hb_vcomp (hb_lunit f₁) α)
× (∏ (a b : B)
(f₁ f₂ : hb_mor a b)
(α : hb_cell f₁ f₂),
hb_vcomp (hb_hcomp α (hb_id2 (hb_id1 b))) (hb_runit f₂)
=
hb_vcomp (hb_runit f₁) α)
× (∏ (b₁ b₂ b₃ b₄ : B)
(f : hb_mor b₁ b₂)
(g : hb_mor b₂ b₃)
(h : hb_mor b₃ b₄),
hb_vcomp
(hb_rassoc f g h)
(hb_lassoc f g h)
=
hb_id2 _)
× (∏ (b₁ b₂ b₃ b₄ : B)
(f : hb_mor b₁ b₂)
(g : hb_mor b₂ b₃)
(h : hb_mor b₃ b₄),
hb_vcomp
(hb_lassoc f g h)
(hb_rassoc f g h)
=
hb_id2 _)
× (∏ (b₁ b₂ : B)
(f : hb_mor b₁ b₂),
hb_vcomp
(hb_lunit f)
(hb_linvunit f)
=
hb_id2 _)
× (∏ (b₁ b₂ : B)
(f : hb_mor b₁ b₂),
hb_vcomp
(hb_linvunit f)
(hb_lunit f)
=
hb_id2 _)
× (∏ (b₁ b₂ : B)
(f : hb_mor b₁ b₂),
hb_vcomp
(hb_runit f)
(hb_rinvunit f)
=
hb_id2 _)
× (∏ (b₁ b₂ : B)
(f : hb_mor b₁ b₂),
hb_vcomp
(hb_rinvunit f)
(hb_runit f)
=
hb_id2 _)
× (∏ (a b c d e : B)
(k : hb_mor a b)
(h : hb_mor b c)
(g : hb_mor c d)
(f : hb_mor d e),
hb_vcomp
(hb_rassoc k h (hb_comp1 g f))
(hb_rassoc (hb_comp1 k h) g f)
=
hb_vcomp
(hb_vcomp
(hb_hcomp (hb_id2 k) (hb_rassoc h g f))
(hb_rassoc k (hb_comp1 h g) f))
(hb_hcomp (hb_rassoc k h g) (hb_id2 f)))
× (∏ (a b c : B)
(f : hb_mor a b)
(g : hb_mor b c),
hb_hcomp (hb_id2 f) (hb_lunit g)
=
hb_vcomp
(hb_rassoc f (hb_id1 b) g)
(hb_hcomp (hb_runit f) (hb_id2 g))).
Lemma isaprop_hcomp_prebicat_laws
(B : hcomp_bicat_data)
(H : ∏ (a b : B) (f g : hb_mor a b), isaset (hb_cell f g))
: isaprop (hcomp_bicat_laws B).
Show proof.
repeat (apply isapropdirprod)
; try (repeat (apply impred ; intro)
; apply H).
do 4 (apply impred ; intro).
apply isapropisaset.
; try (repeat (apply impred ; intro)
; apply H).
do 4 (apply impred ; intro).
apply isapropisaset.
Definition hcomp_bicat
: UU
:= ∑ (B : hcomp_bicat_data), hcomp_bicat_laws B.
Coercion hcomp_bicat_to_data
(B : hcomp_bicat)
: hcomp_bicat_data
:= pr1 B.
Definition hcomp_bicat_hom_cat
(B : hcomp_bicat)
(b₁ b₂ : B)
: category.
Show proof.
use make_category.
- use make_precategory.
+ use make_precategory_data.
* use make_precategory_ob_mor.
** exact (hb_mor b₁ b₂).
** exact (λ f g, hb_cell f g).
* exact (λ f, hb_id2 f).
* exact (λ _ _ _ f g, hb_vcomp f g).
+ repeat split ; simpl ; cbn.
* exact (pr12 B b₁ b₂).
* exact (pr122 B b₁ b₂).
* exact (pr1 (pr222 B) b₁ b₂).
* exact (pr12 (pr222 B) b₁ b₂).
- exact (pr122 (pr222 B) b₁ b₂).
- use make_precategory.
+ use make_precategory_data.
* use make_precategory_ob_mor.
** exact (hb_mor b₁ b₂).
** exact (λ f g, hb_cell f g).
* exact (λ f, hb_id2 f).
* exact (λ _ _ _ f g, hb_vcomp f g).
+ repeat split ; simpl ; cbn.
* exact (pr12 B b₁ b₂).
* exact (pr122 B b₁ b₂).
* exact (pr1 (pr222 B) b₁ b₂).
* exact (pr12 (pr222 B) b₁ b₂).
- exact (pr122 (pr222 B) b₁ b₂).
Definition hcomp_bicat_hcomp
(B : hcomp_bicat)
(b₁ b₂ b₃ : pr11 B)
: precategory_binproduct_data
(hcomp_bicat_hom_cat B b₁ b₂)
(hcomp_bicat_hom_cat B b₂ b₃)
⟶
hcomp_bicat_hom_cat B b₁ b₃.
Show proof.
use make_functor.
- use make_functor_data.
+ exact (λ fg, hb_comp1 (pr1 fg) (pr2 fg)).
+ exact (λ fg fg' α, hb_hcomp (pr1 α) (pr2 α)).
- split.
+ intros f ; cbn in *.
exact (pr1 (pr222 (pr222 B)) b₁ b₂ b₃ (pr1 f) (pr2 f)).
+ intros f g h α β ; cbn in *.
exact (pr12 (pr222 (pr222 B)) b₁ b₂ b₃ _ _ _ _ _ _ (pr1 α) (pr2 α) (pr1 β) (pr2 β)).
- use make_functor_data.
+ exact (λ fg, hb_comp1 (pr1 fg) (pr2 fg)).
+ exact (λ fg fg' α, hb_hcomp (pr1 α) (pr2 α)).
- split.
+ intros f ; cbn in *.
exact (pr1 (pr222 (pr222 B)) b₁ b₂ b₃ (pr1 f) (pr2 f)).
+ intros f g h α β ; cbn in *.
exact (pr12 (pr222 (pr222 B)) b₁ b₂ b₃ _ _ _ _ _ _ (pr1 α) (pr2 α) (pr1 β) (pr2 β)).
Definition hcomp_bicat_to_prebicategory_ob_hom
(B : hcomp_bicat)
: prebicategory_ob_hom.
Show proof.
Definition hcomp_bicat_to_prebicategory_id_comp
(B : hcomp_bicat)
: prebicategory_id_comp.
Show proof.
simple refine (_ ,, _ ,, _).
- exact (hcomp_bicat_to_prebicategory_ob_hom B).
- exact (λ a, hb_id1 a).
- exact (hcomp_bicat_hcomp B).
- exact (hcomp_bicat_to_prebicategory_ob_hom B).
- exact (λ a, hb_id1 a).
- exact (hcomp_bicat_hcomp B).
Definition hcomp_bicat_associator
(B : hcomp_bicat)
(a b c d : hcomp_bicat_to_prebicategory_id_comp B)
: associator_trans_type a b c d.
Show proof.
use make_nat_trans.
- exact (λ f, hb_rassoc (pr1 f) (pr12 f) (pr22 f)).
- intros f₁ f₂ α.
apply (pr122 (pr222 (pr222 B))).
- exact (λ f, hb_rassoc (pr1 f) (pr12 f) (pr22 f)).
- intros f₁ f₂ α.
apply (pr122 (pr222 (pr222 B))).
Definition hcomp_bicat_lunitor
(B : hcomp_bicat)
(a b : hcomp_bicat_to_prebicategory_id_comp B)
: left_unitor_trans_type a b.
Show proof.
use make_nat_trans.
- exact (λ f, hb_lunit f).
- intros f₁ f₂ α.
apply (pr1 (pr222 (pr222 (pr222 B)))).
- exact (λ f, hb_lunit f).
- intros f₁ f₂ α.
apply (pr1 (pr222 (pr222 (pr222 B)))).
Definition hcomp_bicat_runitor
(B : hcomp_bicat)
(a b : hcomp_bicat_to_prebicategory_id_comp B)
: right_unitor_trans_type a b.
Show proof.
use make_nat_trans.
- exact (λ f, hb_runit f).
- intros f₁ f₂ α.
apply (pr2 (pr222 (pr222 (pr222 B)))).
- exact (λ f, hb_runit f).
- intros f₁ f₂ α.
apply (pr2 (pr222 (pr222 (pr222 B)))).
Definition hcomp_bicat_to_prebicategory_data
(B : hcomp_bicat)
: prebicategory_data.
Show proof.
simple refine (_ ,, _ ,, _ ,, _).
- exact (hcomp_bicat_to_prebicategory_id_comp B).
- exact (hcomp_bicat_associator B).
- exact (hcomp_bicat_lunitor B).
- exact (hcomp_bicat_runitor B).
- exact (hcomp_bicat_to_prebicategory_id_comp B).
- exact (hcomp_bicat_associator B).
- exact (hcomp_bicat_lunitor B).
- exact (hcomp_bicat_runitor B).
Definition hcomp_bicat_is_prebicategory
(B : hcomp_bicat)
: is_prebicategory (hcomp_bicat_to_prebicategory_data B).
Show proof.
repeat split.
- intros b₁ b₂ b₃ b₄ f g h ; cbn in *.
use make_is_z_isomorphism.
+ exact (hb_lassoc f g h).
+ split ; apply (pr2 B).
- intros b₁ b₂ f ; cbn in *.
use make_is_z_isomorphism.
+ exact (hb_linvunit f).
+ split ; apply (pr2 B).
- intros b₁ b₂ f ; cbn in *.
use make_is_z_isomorphism.
+ exact (hb_rinvunit f).
+ split ; apply (pr2 B).
- apply (pr2 B).
- apply (pr2 B).
- intros b₁ b₂ b₃ b₄ f g h ; cbn in *.
use make_is_z_isomorphism.
+ exact (hb_lassoc f g h).
+ split ; apply (pr2 B).
- intros b₁ b₂ f ; cbn in *.
use make_is_z_isomorphism.
+ exact (hb_linvunit f).
+ split ; apply (pr2 B).
- intros b₁ b₂ f ; cbn in *.
use make_is_z_isomorphism.
+ exact (hb_rinvunit f).
+ split ; apply (pr2 B).
- apply (pr2 B).
- apply (pr2 B).
Definition hcomp_bicat_to_prebicategory
(B : hcomp_bicat)
: prebicategory.
Show proof.
simple refine (_ ,, _).
- exact (hcomp_bicat_to_prebicategory_data B).
- exact (hcomp_bicat_is_prebicategory B).
- exact (hcomp_bicat_to_prebicategory_data B).
- exact (hcomp_bicat_is_prebicategory B).
Definition prebicategory_to_hcomp_bicat_data
(B : prebicategory)
: hcomp_bicat_data.
Show proof.
simple refine (_ ,, _ ,, _ ,, _ ,, _ ,, _ ,, _ ,, _ ,, _ ,, _ ,, _ ,, _ ,, _ ,, _).
- exact (pr1 (pr111 B)).
- intros b₁ b₂.
exact (pr2 (pr111 B) b₁ b₂).
- intros b₁ b₂ f g.
exact (f --> g).
- exact (pr1 (pr211 B)).
- intros b₁ b₂ b₃ f g.
exact (pr2 (pr211 B) b₁ b₂ b₃ (f ,, g)).
- intros ; simpl.
apply identity.
- exact (λ _ _ _ _ _ α β, α · β).
- cbn in *.
intros b₁ b₂ f.
exact (pr1 (pr2 (pr221 B) b₁ b₂) f).
- intros a b f.
apply (pr2 (pr212 B) _ _ f).
- cbn in *.
intros b₁ b₂ f.
exact (pr1 (pr1 (pr221 B) b₁ b₂) f).
- intros a b f.
apply (pr1 (pr212 B) _ _ f).
- intros b₁ b₂ b₃ b₄ f g h ; cbn in *.
apply ((pr112 B) _ _ _ _ f g h).
- intros b₁ b₂ b₃ b₄ f g h ; cbn in *.
exact (pr1 ((pr121 B) _ _ _ _) (f ,, g ,, h)).
- intros b₁ b₂ b₃ f₁ f₂ g₁ g₂ α β ; simpl in *.
apply (#(pr2 (pr211 B) b₁ b₂ b₃)).
exact (α ,, β).
- exact (pr1 (pr111 B)).
- intros b₁ b₂.
exact (pr2 (pr111 B) b₁ b₂).
- intros b₁ b₂ f g.
exact (f --> g).
- exact (pr1 (pr211 B)).
- intros b₁ b₂ b₃ f g.
exact (pr2 (pr211 B) b₁ b₂ b₃ (f ,, g)).
- intros ; simpl.
apply identity.
- exact (λ _ _ _ _ _ α β, α · β).
- cbn in *.
intros b₁ b₂ f.
exact (pr1 (pr2 (pr221 B) b₁ b₂) f).
- intros a b f.
apply (pr2 (pr212 B) _ _ f).
- cbn in *.
intros b₁ b₂ f.
exact (pr1 (pr1 (pr221 B) b₁ b₂) f).
- intros a b f.
apply (pr1 (pr212 B) _ _ f).
- intros b₁ b₂ b₃ b₄ f g h ; cbn in *.
apply ((pr112 B) _ _ _ _ f g h).
- intros b₁ b₂ b₃ b₄ f g h ; cbn in *.
exact (pr1 ((pr121 B) _ _ _ _) (f ,, g ,, h)).
- intros b₁ b₂ b₃ f₁ f₂ g₁ g₂ α β ; simpl in *.
apply (#(pr2 (pr211 B) b₁ b₂ b₃)).
exact (α ,, β).
Definition prebicategory_to_hcomp_bicat
(B : prebicategory)
: hcomp_bicat.
Show proof.
simple refine (_ ,, _).
- exact (prebicategory_to_hcomp_bicat_data B).
- repeat split ; cbn ; intros.
+ apply id_left.
+ apply id_right.
+ apply assoc.
+ apply assoc'.
+ apply homset_property.
+ apply (functor_id ((pr221 (pr1 B)) b₁ b₂ b₃)).
+ apply (@functor_comp
_ _
((pr221 (pr1 B)) b₁ b₂ b₃)
(_ ,, _) (_ ,, _) (_ ,, _)
(_ ,, _) (_ ,, _)).
+ apply (@nat_trans_ax
_ _ _ _
((pr121 B) a b c d)
(_ ,, (_ ,, _))
(_ ,, (_ ,, _))
(_ ,, (_ ,, _))).
+ apply (nat_trans_ax ((pr122 (pr1 B)) a b)).
+ apply (nat_trans_ax ((pr222 (pr1 B)) a b)).
+ apply (z_iso_inv_after_z_iso (make_z_iso _ _ ((pr112 B) b₁ b₂ b₃ b₄ f g h))).
+ apply (z_iso_after_z_iso_inv (make_z_iso _ _ ((pr112 B) b₁ b₂ b₃ b₄ f g h))).
+ apply (z_iso_inv_after_z_iso (make_z_iso _ _ ((pr121 (pr2 B)) b₁ b₂ f))).
+ apply (z_iso_after_z_iso_inv (make_z_iso _ _ ((pr121 (pr2 B)) b₁ b₂ f))).
+ apply (z_iso_inv_after_z_iso (make_z_iso _ _ ((pr221 (pr2 B)) b₁ b₂ f))).
+ apply (z_iso_after_z_iso_inv (make_z_iso _ _ ((pr221 (pr2 B)) b₁ b₂ f))).
+ apply B.
+ apply B.
- exact (prebicategory_to_hcomp_bicat_data B).
- repeat split ; cbn ; intros.
+ apply id_left.
+ apply id_right.
+ apply assoc.
+ apply assoc'.
+ apply homset_property.
+ apply (functor_id ((pr221 (pr1 B)) b₁ b₂ b₃)).
+ apply (@functor_comp
_ _
((pr221 (pr1 B)) b₁ b₂ b₃)
(_ ,, _) (_ ,, _) (_ ,, _)
(_ ,, _) (_ ,, _)).
+ apply (@nat_trans_ax
_ _ _ _
((pr121 B) a b c d)
(_ ,, (_ ,, _))
(_ ,, (_ ,, _))
(_ ,, (_ ,, _))).
+ apply (nat_trans_ax ((pr122 (pr1 B)) a b)).
+ apply (nat_trans_ax ((pr222 (pr1 B)) a b)).
+ apply (z_iso_inv_after_z_iso (make_z_iso _ _ ((pr112 B) b₁ b₂ b₃ b₄ f g h))).
+ apply (z_iso_after_z_iso_inv (make_z_iso _ _ ((pr112 B) b₁ b₂ b₃ b₄ f g h))).
+ apply (z_iso_inv_after_z_iso (make_z_iso _ _ ((pr121 (pr2 B)) b₁ b₂ f))).
+ apply (z_iso_after_z_iso_inv (make_z_iso _ _ ((pr121 (pr2 B)) b₁ b₂ f))).
+ apply (z_iso_inv_after_z_iso (make_z_iso _ _ ((pr221 (pr2 B)) b₁ b₂ f))).
+ apply (z_iso_after_z_iso_inv (make_z_iso _ _ ((pr221 (pr2 B)) b₁ b₂ f))).
+ apply B.
+ apply B.
Definition hcomp_bicat_weq_prebicategory
: hcomp_bicat ≃ prebicategory.
Show proof.
use make_weq.
- exact hcomp_bicat_to_prebicategory.
- use isweq_iso.
+ exact prebicategory_to_hcomp_bicat.
+ intros b.
apply idpath.
+ intros b.
apply idpath.
- exact hcomp_bicat_to_prebicategory.
- use isweq_iso.
+ exact prebicategory_to_hcomp_bicat.
+ intros b.
apply idpath.
+ intros b.
apply idpath.
Definition hcomp_bicat_to_precategory_ob_mor
(B : hcomp_bicat)
: precategory_ob_mor.
Show proof.
Definition hcomp_bicat_to_precategory_id_comp
(B : hcomp_bicat)
: precategory_id_comp (hcomp_bicat_to_precategory_ob_mor B).
Show proof.
Definition hcomp_bicat_to_precategory_data
(B : hcomp_bicat)
: precategory_data.
Show proof.
simple refine (_ ,, _).
- exact (hcomp_bicat_to_precategory_ob_mor B).
- exact (hcomp_bicat_to_precategory_id_comp B).
- exact (hcomp_bicat_to_precategory_ob_mor B).
- exact (hcomp_bicat_to_precategory_id_comp B).
Definition hcomp_bicat_to_prebicat_1_id_comp_cells
(B : hcomp_bicat)
: prebicat_1_id_comp_cells.
Show proof.
simple refine (_ ,, _).
- exact (hcomp_bicat_to_precategory_data B).
- exact (λ x y f g, hb_cell f g).
- exact (hcomp_bicat_to_precategory_data B).
- exact (λ x y f g, hb_cell f g).
Definition hcomp_bicat_to_prebicat_2_id_comp_struct
(B : hcomp_bicat)
: prebicat_2_id_comp_struct (hcomp_bicat_to_prebicat_1_id_comp_cells B).
Show proof.
repeat split ; cbn.
- intros.
apply hb_id2.
- intros.
apply hb_lunit.
- intros.
apply hb_runit.
- intros.
apply hb_linvunit.
- intros.
apply hb_rinvunit.
- intros.
apply hb_lassoc.
- intros.
apply hb_rassoc.
- intros ? ? ? ? ? α β.
exact (hb_vcomp α β).
- intros ? ? ? f ? ? α.
exact (hb_hcomp (hb_id2 _) α).
- intros ? ? ? f ? ? α.
exact (hb_hcomp α (hb_id2 _)).
- intros.
apply hb_id2.
- intros.
apply hb_lunit.
- intros.
apply hb_runit.
- intros.
apply hb_linvunit.
- intros.
apply hb_rinvunit.
- intros.
apply hb_lassoc.
- intros.
apply hb_rassoc.
- intros ? ? ? ? ? α β.
exact (hb_vcomp α β).
- intros ? ? ? f ? ? α.
exact (hb_hcomp (hb_id2 _) α).
- intros ? ? ? f ? ? α.
exact (hb_hcomp α (hb_id2 _)).
Definition hcomp_bicat_to_prebicat_data
(B : hcomp_bicat)
: prebicat_data.
Show proof.
simple refine (_ ,, _).
- exact (hcomp_bicat_to_prebicat_1_id_comp_cells B).
- exact (hcomp_bicat_to_prebicat_2_id_comp_struct B).
- exact (hcomp_bicat_to_prebicat_1_id_comp_cells B).
- exact (hcomp_bicat_to_prebicat_2_id_comp_struct B).
Definition hcomp_bicat_to_prebicat_laws
(B : hcomp_bicat)
: prebicat_laws (hcomp_bicat_to_prebicat_data B).
Show proof.
repeat split ; try (intros ; apply (pr2 B)).
- intros ; cbn.
etrans.
{
refine (!_).
apply (pr12 (pr222 (pr222 B))).
}
apply maponpaths_2.
apply B.
- intros ; cbn.
etrans.
{
refine (!_).
apply (pr12 (pr222 (pr222 B))).
}
apply maponpaths.
apply B.
- intros ; cbn.
etrans.
{
apply (pr122 (pr222 ((pr222 B)))).
}
apply maponpaths.
apply maponpaths_2.
apply B.
- intros a b c d f₁ f₂ g h α ; cbn.
pose (pr122 (pr222 ((pr222 B))) a b c d f₁ f₂ g g h h α (hb_id2 _) (hb_id2 _)) as p.
cbn in p.
etrans.
{
exact (!p).
}
apply maponpaths_2.
apply maponpaths.
apply B.
- intros a b c f₁ f₂ g h α β ; cbn.
etrans.
{
refine (!_).
apply (pr12 (pr222 (pr222 B))).
}
refine (!_).
etrans.
{
refine (!_).
apply (pr12 (pr222 (pr222 B))).
}
etrans.
{
apply maponpaths.
apply B.
}
etrans.
{
apply maponpaths_2.
apply B.
}
refine (!_).
etrans.
{
apply maponpaths.
apply B.
}
apply maponpaths_2.
apply B.
- intros ; cbn.
refine (!_).
apply B.
- intros ; cbn.
refine (!_).
apply B.
- intros ; cbn.
etrans.
{
refine (!_).
apply (pr12 (pr222 (pr222 B))).
}
apply maponpaths_2.
apply B.
- intros ; cbn.
etrans.
{
refine (!_).
apply (pr12 (pr222 (pr222 B))).
}
apply maponpaths.
apply B.
- intros ; cbn.
etrans.
{
apply (pr122 (pr222 ((pr222 B)))).
}
apply maponpaths.
apply maponpaths_2.
apply B.
- intros a b c d f₁ f₂ g h α ; cbn.
pose (pr122 (pr222 ((pr222 B))) a b c d f₁ f₂ g g h h α (hb_id2 _) (hb_id2 _)) as p.
cbn in p.
etrans.
{
exact (!p).
}
apply maponpaths_2.
apply maponpaths.
apply B.
- intros a b c f₁ f₂ g h α β ; cbn.
etrans.
{
refine (!_).
apply (pr12 (pr222 (pr222 B))).
}
refine (!_).
etrans.
{
refine (!_).
apply (pr12 (pr222 (pr222 B))).
}
etrans.
{
apply maponpaths.
apply B.
}
etrans.
{
apply maponpaths_2.
apply B.
}
refine (!_).
etrans.
{
apply maponpaths.
apply B.
}
apply maponpaths_2.
apply B.
- intros ; cbn.
refine (!_).
apply B.
- intros ; cbn.
refine (!_).
apply B.
Definition hcomp_bicat_to_prebicat
(B : hcomp_bicat)
: prebicat.
Show proof.
simple refine (_ ,, _).
- exact (hcomp_bicat_to_prebicat_data B).
- exact (hcomp_bicat_to_prebicat_laws B).
- exact (hcomp_bicat_to_prebicat_data B).
- exact (hcomp_bicat_to_prebicat_laws B).
Definition hcomp_bicat_to_bicat
(B : hcomp_bicat)
: bicat.
Show proof.
simple refine (_ ,, _).
- exact (hcomp_bicat_to_prebicat B).
- simpl.
intro ; intros.
apply (pr122 (pr222 B)).
- exact (hcomp_bicat_to_prebicat B).
- simpl.
intro ; intros.
apply (pr122 (pr222 B)).
Definition bicat_to_hcomp_bicat_data
(B : bicat)
: hcomp_bicat_data.
Show proof.
simple refine (_ ,, _ ,, _ ,, _ ,, _ ,, _ ,, _ ,, _ ,, _ ,, _ ,, _ ,, _ ,, _ ,, _).
- exact B.
- exact (λ x y, x --> y).
- exact (λ _ _ f g, f ==> g).
- exact (λ x, id₁ _).
- exact (λ _ _ _ f g, f · g).
- exact (λ _ _ f, id2 f).
- exact (λ _ _ _ _ _ α β, α • β).
- exact (λ _ _ f, runitor f).
- exact (λ _ _ f, rinvunitor f).
- exact (λ _ _ f, lunitor f).
- exact (λ _ _ f, linvunitor f).
- exact (λ _ _ _ _ f g h, rassociator f g h).
- exact (λ _ _ _ _ f g h, lassociator f g h).
- exact (λ _ _ _ _ _ _ _ α β, β ⋆⋆ α).
- exact B.
- exact (λ x y, x --> y).
- exact (λ _ _ f g, f ==> g).
- exact (λ x, id₁ _).
- exact (λ _ _ _ f g, f · g).
- exact (λ _ _ f, id2 f).
- exact (λ _ _ _ _ _ α β, α • β).
- exact (λ _ _ f, runitor f).
- exact (λ _ _ f, rinvunitor f).
- exact (λ _ _ f, lunitor f).
- exact (λ _ _ f, linvunitor f).
- exact (λ _ _ _ _ f g h, rassociator f g h).
- exact (λ _ _ _ _ f g h, lassociator f g h).
- exact (λ _ _ _ _ _ _ _ α β, β ⋆⋆ α).
Definition bicat_to_hcomp_bicat_laws
(B : bicat)
: hcomp_bicat_laws (bicat_to_hcomp_bicat_data B).
Show proof.
repeat split ; cbn ; intros.
- apply id2_left.
- apply id2_right.
- apply vassocr.
- apply vassocl.
- apply cellset_property.
- apply hcomp_identity.
- apply interchange.
- apply hcomp_lassoc.
- apply lunitor_natural.
- apply runitor_natural.
- apply lassociator_rassociator.
- apply rassociator_lassociator.
- apply lunitor_linvunitor.
- apply linvunitor_lunitor.
- apply runitor_rinvunitor.
- apply rinvunitor_runitor.
- rewrite <- lwhisker_hcomp, <- rwhisker_hcomp.
refine (!_).
apply lassociator_lassociator.
- rewrite <- lwhisker_hcomp, <- rwhisker_hcomp.
rewrite <- lunitor_lwhisker.
rewrite !vassocr.
rewrite lassociator_rassociator.
rewrite id2_left.
apply idpath.
- apply id2_left.
- apply id2_right.
- apply vassocr.
- apply vassocl.
- apply cellset_property.
- apply hcomp_identity.
- apply interchange.
- apply hcomp_lassoc.
- apply lunitor_natural.
- apply runitor_natural.
- apply lassociator_rassociator.
- apply rassociator_lassociator.
- apply lunitor_linvunitor.
- apply linvunitor_lunitor.
- apply runitor_rinvunitor.
- apply rinvunitor_runitor.
- rewrite <- lwhisker_hcomp, <- rwhisker_hcomp.
refine (!_).
apply lassociator_lassociator.
- rewrite <- lwhisker_hcomp, <- rwhisker_hcomp.
rewrite <- lunitor_lwhisker.
rewrite !vassocr.
rewrite lassociator_rassociator.
rewrite id2_left.
apply idpath.
Definition bicat_to_hcomp_bicat
(B : bicat)
: hcomp_bicat.
Show proof.
simple refine (_ ,, _).
- exact (bicat_to_hcomp_bicat_data B).
- exact (bicat_to_hcomp_bicat_laws B).
- exact (bicat_to_hcomp_bicat_data B).
- exact (bicat_to_hcomp_bicat_laws B).
Definition hcomp_bicat_to_bicat_to_hcomp_bicat
(B : hcomp_bicat)
: bicat_to_hcomp_bicat (hcomp_bicat_to_bicat B) = B.
Show proof.
use total2_paths_f.
- do 13 (use total2_paths_f ; [ apply idpath | ] ; cbn).
use funextsec ; intro x.
use funextsec ; intro y.
use funextsec ; intro z.
use funextsec ; intro f₁.
use funextsec ; intro f₂.
use funextsec ; intro g₁.
use funextsec ; intro g₂.
use funextsec ; intro α.
use funextsec ; intro β.
cbn.
etrans.
{
refine (!_).
apply (pr12 (pr222 (pr222 B))).
}
etrans.
{
apply maponpaths.
apply (pr12 B).
}
etrans.
{
apply maponpaths_2.
apply (pr122 B).
}
apply idpath.
- apply isaprop_hcomp_prebicat_laws.
apply B.
- do 13 (use total2_paths_f ; [ apply idpath | ] ; cbn).
use funextsec ; intro x.
use funextsec ; intro y.
use funextsec ; intro z.
use funextsec ; intro f₁.
use funextsec ; intro f₂.
use funextsec ; intro g₁.
use funextsec ; intro g₂.
use funextsec ; intro α.
use funextsec ; intro β.
cbn.
etrans.
{
refine (!_).
apply (pr12 (pr222 (pr222 B))).
}
etrans.
{
apply maponpaths.
apply (pr12 B).
}
etrans.
{
apply maponpaths_2.
apply (pr122 B).
}
apply idpath.
- apply isaprop_hcomp_prebicat_laws.
apply B.
Definition bicat_to_hcomp_bicat_to_bicat
(B : bicat)
: hcomp_bicat_to_bicat (bicat_to_hcomp_bicat B) = B.
Show proof.
use subtypePath.
{
intro.
do 4 (use impred ; intro).
apply isapropisaset.
}
use total2_paths_f.
- use total2_paths_f.
+ apply idpath.
+ repeat (use pathsdirprod) ; cbn.
* apply idpath.
* apply idpath.
* apply idpath.
* apply idpath.
* apply idpath.
* apply idpath.
* apply idpath.
* apply idpath.
* repeat (use funextsec ; intro).
rewrite <- lwhisker_hcomp.
apply idpath.
* repeat (use funextsec ; intro).
rewrite <- rwhisker_hcomp.
apply idpath.
- apply isaprop_prebicat_laws.
intros.
apply cellset_property.
{
intro.
do 4 (use impred ; intro).
apply isapropisaset.
}
use total2_paths_f.
- use total2_paths_f.
+ apply idpath.
+ repeat (use pathsdirprod) ; cbn.
* apply idpath.
* apply idpath.
* apply idpath.
* apply idpath.
* apply idpath.
* apply idpath.
* apply idpath.
* apply idpath.
* repeat (use funextsec ; intro).
rewrite <- lwhisker_hcomp.
apply idpath.
* repeat (use funextsec ; intro).
rewrite <- rwhisker_hcomp.
apply idpath.
- apply isaprop_prebicat_laws.
intros.
apply cellset_property.
Definition hcomp_bicat_weq_bicat
: hcomp_bicat ≃ bicat.
Show proof.
use make_weq.
- exact hcomp_bicat_to_bicat.
- use isweq_iso.
+ exact bicat_to_hcomp_bicat.
+ exact hcomp_bicat_to_bicat_to_hcomp_bicat.
+ exact bicat_to_hcomp_bicat_to_bicat.
- exact hcomp_bicat_to_bicat.
- use isweq_iso.
+ exact bicat_to_hcomp_bicat.
+ exact hcomp_bicat_to_bicat_to_hcomp_bicat.
+ exact bicat_to_hcomp_bicat_to_bicat.
Definition weq_bicat_prebicategory : bicat ≃ prebicategory.
Show proof.