Library UniMath.Bicategories.WkCatEnrichment.prebicategory
**********************************************************
Mitchell Riley
June 2016
I am very grateful to Peter LeFanu Lumsdaine, whose unreleased bicategories code strongly
influenced the definitions in this file.
Require Import UniMath.Foundations.PartD.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.categories.StandardCategories. Require Import UniMath.CategoryTheory.HorizontalComposition.
Require Import UniMath.CategoryTheory.Equivalences.Core.
Local Open Scope cat.
Local Notation "C 'c×' D" := (category_binproduct C D)
(at level 75, right associativity).
Definition prebicategory_ob_hom : UU := ∑ C : UU, ∏ a b : C, category.
Coercion bicat_ob (C : prebicategory_ob_hom) : UU := pr1 C.
Definition homcat {C : prebicategory_ob_hom} (a b : C) : category := pr2 C a b.
Local Notation "a '-1->' b" := (homcat a b) (at level 50, left associativity).
Local Notation "f '-2->' g" := (@precategory_morphisms (_ -1->_) f g)
(at level 50, left associativity).
Local Notation "alpha ';v;' beta" := (@compose (_ -1-> _) _ _ _ alpha beta)
(at level 50, left associativity).
Definition prebicategory_id_comp :=
∑ C : prebicategory_ob_hom,
(∏ a : C, a -1-> a)
× (∏ a b c : C, ((a -1-> b) c× (b -1-> c)) ⟶ (a -1-> c)).
Coercion prebicategory_ob_hom_from_prebicategory_id_comp (C : prebicategory_id_comp) :
prebicategory_ob_hom := pr1 C.
Definition identity1 {C : prebicategory_id_comp} (a : C) : a -1-> a := pr1 (pr2 C) a.
Definition compose_functor {C : prebicategory_id_comp} (a b c : C)
: ((a -1-> b) c× (b -1-> c)) ⟶ (a -1-> c)
:= pr2 (pr2 C) a b c.
Definition compose1 {C : prebicategory_id_comp} {a b c : C} (f : a -1-> b) (g : b -1-> c)
:= functor_on_objects (compose_functor a b c) (make_dirprod f g).
Local Notation "f ';1;' g" := (compose1 f g)
(at level 50, left associativity).
Definition compose2h {C : prebicategory_id_comp} {a b c : C}
{f f' : a -1-> b}
{g g' : b -1-> c}
(alpha : f -2-> f')
(beta : g -2-> g')
: (f ;1; g) -2-> (f' ;1; g').
Show proof.
Local Notation "alpha ';h;' beta" := (compose2h alpha beta) (at level 50, left associativity).
Definition compose2h_iso {C : prebicategory_id_comp} {a b c : C}
{f f' : a -1-> b}
{g g' : b -1-> c}
(alpha : z_iso f f')
(beta : z_iso g g')
: z_iso (f ;1; g) (f' ;1; g').
Show proof.
Local Notation "alpha ';hi;' beta" := (compose2h_iso alpha beta) (at level 50, left associativity).
Definition associator_trans_type {C : prebicategory_id_comp} (a b c d : C) : UU
:= pair_functor (functor_identity (a -1-> b)) (compose_functor b c d) ∙
compose_functor a b d
⟹
precategory_binproduct_assoc (a -1-> b) (b -1-> c) (c -1-> d) ∙
(pair_functor (compose_functor a b c) (functor_identity (c -1-> d)) ∙
compose_functor a c d).
Definition left_unitor_trans_type {C : prebicategory_id_comp} (a b : C) : UU
:= bindelta_pair_functor
(constant_functor (a -1-> b) (a -1-> a) (identity1 a))
(functor_identity (a -1-> b)) ∙ compose_functor a a b
⟹
functor_identity (a -1-> b).
Definition right_unitor_trans_type {C : prebicategory_id_comp} (a b : C) : UU
:= bindelta_pair_functor
(functor_identity (a -1-> b))
(constant_functor (a -1-> b) (b -1-> b) (identity1 b)) ∙
compose_functor a b b
⟹
functor_identity (a -1-> b).
Definition prebicategory_data : UU :=
∑ C : prebicategory_id_comp,
(∏ a b c d : C, associator_trans_type a b c d)
× (∏ a b : C, left_unitor_trans_type a b)
× (∏ a b : C, right_unitor_trans_type a b).
Coercion prebicategory_id_comp_from_prebicategory_data (C : prebicategory_data)
: prebicategory_id_comp
:= pr1 C.
Definition associator_trans {C : prebicategory_data} (a b c d : C)
: pair_functor (functor_identity (a -1-> b))
(compose_functor b c d) ∙ compose_functor a b d
⟹
precategory_binproduct_assoc (a -1-> b) (b -1-> c) (c -1-> d) ∙
(pair_functor (compose_functor a b c) (functor_identity (c -1-> d)) ∙
compose_functor a c d)
:= pr1 (pr2 C) a b c d.
Definition associator_2mor {C : prebicategory_data} {a b c d : C}
(f : a -1-> b)
(g : b -1-> c)
(h : c -1-> d)
: (f ;1; (g ;1; h)) -2-> ((f ;1; g) ;1; h)
:= associator_trans a b c d (make_catbinprod f (make_catbinprod g h)).
Definition left_unitor_trans {C : prebicategory_data} (a b : C)
: bindelta_pair_functor
(constant_functor (a -1-> b) (a -1-> a) (identity1 a))
(functor_identity (a -1-> b)) ∙ compose_functor a a b
⟹
functor_identity (a -1-> b)
:= pr1 (pr2 (pr2 C)) a b.
Definition left_unitor_2mor {C : prebicategory_data} {a b : C}
(f : a -1-> b)
: identity1 a ;1; f -2-> f
:= left_unitor_trans a b f.
Definition right_unitor_trans {C : prebicategory_data} (a b : C)
: bindelta_pair_functor
(functor_identity (a -1-> b))
(constant_functor (a -1-> b) (b -1-> b) (identity1 b)) ∙
compose_functor a b b
⟹
functor_identity (a -1-> b)
:= pr2 (pr2 (pr2 C)) a b.
Definition right_unitor_2mor {C : prebicategory_data} {a b : C} (f : a -1-> b)
: f ;1; (identity1 b) -2-> f
:= right_unitor_trans a b f.
Definition associator_and_unitors_are_iso (C : prebicategory_data) : UU
:= (∏ (a b c d : C) (f : a -1-> b) (g : b -1-> c) (h : c -1-> d),
is_z_isomorphism (associator_2mor f g h))
× (∏ (a b : C) (f : a -1-> b), is_z_isomorphism (left_unitor_2mor f))
× (∏ (a b : C) (g : a -1-> b), is_z_isomorphism (right_unitor_2mor g)).
Definition pentagon_axiom_type {C : prebicategory_data} {a b c d e : C}
(k : a -1-> b) (h : b -1-> c) (g : c -1-> d) (f : d -1-> e)
: UU
:=
associator_2mor k h (g ;1; f) ;v; associator_2mor (k ;1; h) g f
=
(identity k ;h; associator_2mor h g f)
;v; associator_2mor k (h ;1; g) f
;v; (associator_2mor k h g ;h; identity f).
Definition triangle_axiom_type {C : prebicategory_data} {a b c : C}
(f : a -1-> b)
(g : b -1-> c)
: UU
:= identity f ;h; left_unitor_2mor g =
associator_2mor f (identity1 b) g ;v; (right_unitor_2mor f ;h; identity g).
Definition prebicategory_coherence (C : prebicategory_data) : UU
:= (∏ (a b c d e : C) (k : a -1-> b) (h : b -1-> c) (g : c -1-> d) (f : d -1-> e),
pentagon_axiom_type k h g f)
× (∏ (a b c : C) (f : a -1-> b) (g : b -1-> c), triangle_axiom_type f g).
Definition is_prebicategory (C : prebicategory_data) : UU
:= associator_and_unitors_are_iso C
× prebicategory_coherence C.
Definition prebicategory : UU := total2 is_prebicategory.
Coercion prebicategory_data_from_prebicategory (C : prebicategory) : prebicategory_data
:= pr1 C.
Definition has_homcats (C : prebicategory) : UU
:= ∏ a b : C, is_univalent (homcat a b).
Definition associator {C : prebicategory} {a b c d : C}
(f : a -1-> b) (g : b -1-> c) (h : c -1-> d)
: z_iso (f ;1; (g ;1; h)) ((f ;1; g) ;1; h).
Show proof.
Definition left_unitor {C : prebicategory} {a b : C}
(f : a -1-> b)
: z_iso ((identity1 a) ;1; f) f.
Show proof.
Definition right_unitor {C : prebicategory} {a b : C} (f : a -1-> b)
: z_iso (f ;1; (identity1 b)) f.
Show proof.
Definition pentagon_axiom {C : prebicategory} {a b c d e: C}
(k : a -1-> b) (h : b -1-> c) (g : c -1-> d) (f : d -1-> e)
: pentagon_axiom_type k h g f
:= pr1 (pr2 (pr2 C)) a b c d e k h g f.
Definition triangle_axiom {C : prebicategory} {a b c : C}
(f : a -1-> b) (g : b -1-> c)
: triangle_axiom_type f g
:= pr2 (pr2 (pr2 C)) a b c f g.
Lemma id_2mor_left {C : prebicategory} {b c : C} {g g' : b -1-> c} (β : g -2-> g')
: identity (identity1 b) ;h; β
= left_unitor g ;v; β ;v; inv_from_z_iso (left_unitor g').
Show proof.
Lemma id_2mor_right {C : prebicategory} {a b : C} {f f' : a -1-> b} (alpha : f -2-> f')
: alpha ;h; identity (identity1 b) =
right_unitor f ;v; alpha ;v; inv_from_z_iso (right_unitor f').
Show proof.
Lemma horizontal_comp_id {C : prebicategory_id_comp} {a b c : C}
{f : a -1-> b} {g : b -1-> c}
: identity f ;h; identity g = identity (f ;1; g).
Show proof.
Lemma inv_horizontal_comp {C : prebicategory_id_comp} {a b c : C}
{f f' : a -1-> b} {g g' : b -1-> c}
(alpha : z_iso f f') (beta : z_iso g g')
: (z_iso_inv_from_z_iso alpha) ;hi; (z_iso_inv_from_z_iso beta)
= z_iso_inv_from_z_iso (alpha ;hi; beta).
Show proof.
Lemma interchange {C : prebicategory} {a b c : C}
{f1 f2 f3 : a -1-> b} {g1 g2 g3 : b -1-> c}
(a1 : f1 -2-> f2) (a2 : f2 -2-> f3)
(b1 : g1 -2-> g2) (b2 : g2 -2-> g3)
: (a1 ;v; a2) ;h; (b1 ;v; b2) = (a1 ;h; b1) ;v; (a2 ;h; b2).
Show proof.
: identity (identity1 b) ;h; β
= left_unitor g ;v; β ;v; inv_from_z_iso (left_unitor g').
Show proof.
Lemma id_2mor_right {C : prebicategory} {a b : C} {f f' : a -1-> b} (alpha : f -2-> f')
: alpha ;h; identity (identity1 b) =
right_unitor f ;v; alpha ;v; inv_from_z_iso (right_unitor f').
Show proof.
Lemma horizontal_comp_id {C : prebicategory_id_comp} {a b c : C}
{f : a -1-> b} {g : b -1-> c}
: identity f ;h; identity g = identity (f ;1; g).
Show proof.
unfold compose2h.
intermediate_path (functor_on_morphisms (compose_functor a b c)
(identity (make_catbinprod f g))).
reflexivity.
apply functor_id.
intermediate_path (functor_on_morphisms (compose_functor a b c)
(identity (make_catbinprod f g))).
reflexivity.
apply functor_id.
Lemma inv_horizontal_comp {C : prebicategory_id_comp} {a b c : C}
{f f' : a -1-> b} {g g' : b -1-> c}
(alpha : z_iso f f') (beta : z_iso g g')
: (z_iso_inv_from_z_iso alpha) ;hi; (z_iso_inv_from_z_iso beta)
= z_iso_inv_from_z_iso (alpha ;hi; beta).
Show proof.
Lemma interchange {C : prebicategory} {a b c : C}
{f1 f2 f3 : a -1-> b} {g1 g2 g3 : b -1-> c}
(a1 : f1 -2-> f2) (a2 : f2 -2-> f3)
(b1 : g1 -2-> g2) (b2 : g2 -2-> g3)
: (a1 ;v; a2) ;h; (b1 ;v; b2) = (a1 ;h; b1) ;v; (a2 ;h; b2).
Show proof.
unfold compose2h.
assert (X : catbinprodmor a1 b1 · catbinprodmor a2 b2
= catbinprodmor (a1 ;v; a2) (b1 ;v; b2)) by reflexivity.
rewrite <- X.
apply functor_comp.
assert (X : catbinprodmor a1 b1 · catbinprodmor a2 b2
= catbinprodmor (a1 ;v; a2) (b1 ;v; b2)) by reflexivity.
rewrite <- X.
apply functor_comp.