Bicategory (Is1Cat compatible design)

theories/Basics/Notations.v

@@ -156,6 +156,7 @@ Reserved Infix "$oE" (at level 40, left associativity).
 Reserved Infix "$==" (at level 70).
 Reserved Infix "$o@" (at level 30).
 Reserved Infix "$@" (at level 30).
+Reserved Infix "$|" (at level 30).
 Reserved Infix "$@L" (at level 30).
 Reserved Infix "$@R" (at level 30).
 Reserved Infix "$@@" (at level 30).

theories/Basics/PathGroupoids.v

@@ -101,6 +101,26 @@ Definition concat_pp_p {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z =
       match p with idpath => 1
       end end end.
 
+Theorem concat_assoc_inv {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) :
+  concat_p_pp p q r @ concat_pp_p p q r = 1.
+Proof.
+  unfold concat_pp_p, concat_p_pp.
+  refine (match r with idpath => _ end).
+  refine (match q with idpath => _ end).
+  refine (match p with idpath => _ end).
+  exact idpath.
+Defined.
+
+Theorem concat_assoc_inv' {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) :
+  concat_pp_p p q r @ concat_p_pp p q r = 1.
+Proof.
+  unfold concat_pp_p, concat_p_pp.
+  refine (match r with idpath => _ end).
+  refine (match q with idpath => _ end).
+  refine (match p with idpath => _ end).
+  exact idpath.
+Defined.
+
 (** The left inverse law. *)
 Definition concat_pV {A : Type} {x y : A} (p : x = y) :
   p @ p^ = 1

theories/Pointed/Core.v

@@ -581,6 +581,25 @@ Proof.
   - intros ? ? f; exact (pmap_precompose_idmap f).
 Defined.
 
+(** [pType] is a 1-coherent bicategory *)
+Instance is1bicat_ptype : Is1Bicat pType.
+Proof.
+  snapply Build_Is1Bicat.
+  - exact _.
+  - intros A B C h; rapply Build_Is0Functor.
+    intros f g p; cbn.
+    apply pmap_postwhisker; assumption.
+  - intros A B C h; rapply Build_Is0Functor.
+    intros f g p; cbn.
+    apply pmap_prewhisker; assumption.
+  - intros ? ? ? ? f g h; exact (pmap_compose_assoc h g f).
+  - intros ? ? ? ? f g h; exact ((pmap_compose_assoc h g f)^* ).
+  - intros ? ? f; exact (pmap_postcompose_idmap f).
+  - intros ? ? f; exact ((pmap_postcompose_idmap f)^* ).
+  - intros ? ? f; exact (pmap_precompose_idmap f).
+  - intros ? ? f; exact ((pmap_precompose_idmap f)^* ).
+Defined.
+
 (** [pType] is a pointed category *)
 Instance ispointedcat_ptype : IsPointedCat pType.
 Proof.
@@ -623,10 +642,12 @@ Defined.
 Instance is3graph_ptype : Is3Graph pType
   := fun f g => is2graph_pforall _ _.
 
-Instance is21cat_ptype : Is21Cat pType.
+Instance isbicat_ptype : IsBicat pType.
 Proof.
-  unshelve econstructor.
-  - exact _.
+  econstructor.
+  5-7: intros; constructor; [
+          apply phomotopy_compose_pV
+        | apply phomotopy_compose_Vp].
   - intros A B C f; napply Build_Is1Functor.
     + intros g h p q r.
       srapply Build_pHomotopy.
@@ -658,46 +679,38 @@ Proof.
     + intros x.
       exact (concat_Ap q _)^.
     + by pelim p f g q h k.
-  - intros A B C D f g.
-    snapply Build_Is1Natural.
-    intros r1 r2 s1.
-    srapply Build_pHomotopy.
-    1: exact (fun _ => concat_p1 _ @ (concat_1p _)^).
-    by pelim f g s1 r1 r2.
-  - intros A B C D f g.
-    snapply Build_Is1Natural.
-    intros r1 r2 s1.
-    srapply Build_pHomotopy.
-    1: exact (fun _ => concat_p1 _ @ (concat_1p _)^).
-    by pelim f s1 r1 r2 g.
-  - intros A B C D f g.
-    snapply Build_Is1Natural.
-    intros r1 r2 s1.
-    srapply Build_pHomotopy.
-    1: cbn; exact (fun _ => concat_p1 _ @ ap_compose _ _ _ @ (concat_1p _)^).
-    by pelim s1 r1 r2 f g.
-  - intros A B.
-    snapply Build_Is1Natural.
-    intros r1 r2 s1.
-    srapply Build_pHomotopy.
-    1: exact (fun _ => concat_p1 _ @ ap_idmap _ @ (concat_1p _)^).
-    by pelim s1 r1 r2.
-  - intros A B.
-    snapply Build_Is1Natural.
-    intros r1 r2 s1.
-    srapply Build_pHomotopy.
-    1: exact (fun _ => concat_p1 _ @ (concat_1p _)^).
-    simpl; by pelim s1 r1 r2.
-  - intros A B C D E f g h j.
-    srapply Build_pHomotopy.
-    1: reflexivity.
-    by pelim f g h j.
-  - intros A B C f g.
-    srapply Build_pHomotopy.
-    1: reflexivity.
-    by pelim f g.
+  - intros A B C D; snapply Build_Is1Natural.
+    (* TODO: It would be nice if this naturality proof could reuse the proof in the
+       definition of the bicategory Type. *)
+    intros [[f g] h] [[f' g'] h'] [[p q] r]; simpl in *.
+    snapply Build_pHomotopy.
+    + intro x; apply (Type_associator_natural A B C D).
+    + unfold Type_associator_natural.
+      pelim p f f' q g g' r; pelim h h'.
+      exact idpath.
+  - intros A B. snapply Build_Is1Natural.
+    intros f g p; srapply Build_pHomotopy.
+    + (* The proof is very simple, but it seems preferable to explicitly link it to the corresponding construction in Type. *)
+      exact (isnat _ (alnat:=isnatural_bicat_idl (A:=Type)) p).
+    + by pelim p f g.
+  - intros A B. snapply Build_Is1Natural.
+    intros f g p; srapply Build_pHomotopy.
+    + (* Same comment as above. *)
+      exact (isnat _ (alnat:=isnatural_bicat_idr (A:=Type)) p).
+    + simpl; unfold Type_right_unitor_natural.
+      by pelim p f g.
+  - intros A B C D E f g h k. simpl.
+    snapply Build_pHomotopy.
+    + exact (bicat_pentagon (A:=Type) f g h k).
+    + by pelim f g h k.
+  - intros A B C f g. snapply Build_pHomotopy.
+    + exact (bicat_tril (A:=Type) f g).
+    + by pelim f g.
 Defined.
 
+Instance Is21Cat_ptype : Is21Cat pType
+  := Build_Is21Cat _ _ _ _ _ _ _ _ _ .
+
 (** The forgetful map from [pType] to [Type] is a 0-functor *)
 Instance is0functor_pointed_type : Is0Functor pointed_type.
 Proof.

theories/WildCat/Core.v

@@ -171,6 +171,12 @@ Record RetractionOf {A} `{Is1Cat A} {a b : A} (f : a $-> b) :=
     is_retraction : comp_left_inverse $o f $== Id a
   }.
 
+Class AreInverse {A} `{Is1Cat A} {a b : A} (f : a $-> b) (g : b $-> a) :=
+  {
+    inv_issect : g $o f $== Id a;
+    inv_isretr : f $o g $== Id b;
+  }.
+
 (** Often, the coherences are actually equalities rather than homotopies. *)
 Class Is1Cat_Strong (A : Type)`{!IsGraph A, !Is2Graph A, !Is01Cat A} :=
 {

theories/WildCat/Paths.v

@@ -48,6 +48,21 @@ Proof.
   exact (@ap _ _ (cat_precomp c f)).
 Defined.
 
+(** Any type is a 1-bicategory with n-morphisms given by paths. *)
+Instance is1bicat_paths {A : Type} : Is1Bicat A.
+Proof.
+  snapply Build_Is1Bicat.
+  - exact _.
+  - exact _.
+  - exact _.
+  - exact (@concat_p_pp A).
+  - exact (@concat_pp_p A).
+  - exact (@concat_p1 A).
+  - intros a b f. exact ((@concat_p1 A _ _ f)^).
+  - exact (@concat_1p A).
+  - intros a b f. exact ((@concat_1p A _ _ f)^).
+Defined.
+
 (** Any type is a 1-category with n-morphisms given by paths. *)
 Instance is1cat_paths {A : Type} : Is1Cat A.
 Proof.
@@ -71,10 +86,10 @@ Proof.
 Defined.
 
 (** Any type is a 2-category with higher morphisms given by paths. *)
-Instance is21cat_paths {A : Type} : Is21Cat A.
+
+Instance isbicat_paths {A : Type} : IsBicat A.
 Proof.
-  snapply Build_Is21Cat.
-  - exact _.
+  snapply Build_IsBicat.
   - exact _.
   - intros x y z p.
     snapply Build_Is1Functor.
@@ -92,30 +107,27 @@ Proof.
       exact (whiskerL_pp p).
   - intros a b c q r s t h g.
     exact (concat_whisker q r s t h g)^.
-  - intros a b c d q r.
+  - intros a b c d.
     snapply Build_Is1Natural.
-    intros s t h.
-    apply concat_p_pp_nat_r.
-  - intros a b c d q r.
-    snapply Build_Is1Natural.
-    intros s t h.
-    apply concat_p_pp_nat_m.
-  - intros a b c d q r.
-    snapply Build_Is1Natural.
-    intros s t h.
-    apply concat_p_pp_nat_l.
+    intros [[f g] h] [[f' g'] h'] [[p q] r]; simpl in *.
+    unfold Bifunctor.fmap11, Prod.fmap_pair; simpl.
+    unfold cat_precomp; simpl in p, q, r.
+    destruct r, q, p. simpl. exact (concat_1p_p1 _ ).
+  - intros a b c d f g h; constructor.
+    + exact (concat_assoc_inv f g h).
+    + exact (concat_assoc_inv' f g h).
+  - intros a b f; constructor.
+    + exact (concat_pV _).
+    + exact (concat_Vp _).
+  - intros a b f; constructor.
+    + exact (concat_pV _).
+    + exact (concat_Vp _).
   - intros a b.
     snapply Build_Is1Natural.
-    intros p q h; cbn.
-    apply moveL_Mp.
-    lhs napply concat_p_pp.
-    exact (whiskerR_p1 h).
+    apply concat_A1p.
   - intros a b.
     snapply Build_Is1Natural.
-    intros p q h.
-    apply moveL_Mp.
-    lhs rapply concat_p_pp.
-    exact (whiskerL_1p h).
+    apply concat_A1p.
   - intros a b c d e p q r s.
     lhs napply concat_p_pp.
     exact (pentagon p q r s).