Bicategory (Is1Cat compatible design)

theories/Algebra/AbSES/Core.v

@@ -287,8 +287,7 @@ Defined.
 Instance is1gpd_abses {A B : AbGroup@{u}}
   : Is1Gpd (AbSES B A).
 Proof.
-  rapply Build_Is1Gpd;
-    intros E F p e; cbn.
+  intros E F p; constructor.
   - apply eissect.
   - apply eisretr.
 Defined.

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

@@ -96,10 +96,7 @@ Definition concat_p_pp {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z =
 
 Definition concat_pp_p {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) :
   (p @ q) @ r = p @ (q @ r) :=
-  match r with idpath =>
-    match q with idpath =>
-      match p with idpath => 1
-      end end end.
+  (concat_p_pp p q r)^.
 
 (** The left inverse law. *)
 Definition concat_pV {A : Type} {x y : A} (p : x = y) :

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.
@@ -615,18 +634,20 @@ Defined.
 (** [pForall] is a 1-groupoid *)
 Instance is1gpd_pforall (A : pType) (P : pFam A) : Is1Gpd (pForall A P) | 10.
 Proof.
-  econstructor.
-  + intros ? ? p. exact (phomotopy_compose_pV p).
-  + intros ? ? p. exact (phomotopy_compose_Vp p).
+  intros ? ? p; constructor.
+  + exact (phomotopy_compose_pV p).
+  + exact (phomotopy_compose_Vp p).
 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} :=
 {
@@ -376,10 +382,13 @@ Arguments is1functor_compose {A B C}
 (** ** Wild 1-groupoids *)
 
 Class Is1Gpd (A : Type) `{Is1Cat A, !Is0Gpd A} :=
-{
-  gpd_issect : forall {a b : A} (f : a $-> b), f^$ $o f $== Id a ;
-  gpd_isretr : forall {a b : A} (f : a $-> b), f $o f^$ $== Id b ;
-}.
+  is1gpd :: forall {a b : A} (f : a $-> b), AreInverse f f^$.
+
+Definition gpd_issect {A : Type} `{Is1Gpd A} {a b : A} (f : a $-> b) :=
+  inv_issect (f:=f) (g:=f^$).
+
+Definition gpd_isretr {A : Type} `{Is1Gpd A} {a b : A} (f : a $-> b) :=
+  inv_isretr (f:=f) (g:=f^$).
 
 (** Some more convenient equalities for morphisms in a 1-groupoid. The naming scheme is similar to [PathGroupoids.v].*)
 

theories/WildCat/Equiv.v

@@ -592,7 +592,7 @@ Defined.
 Instance is1gpd_core {A : Type} `{HasEquivs A}
   : Is1Gpd (core A).
 Proof.
-  apply Build_Is1Gpd; cbn ; intros a b f;
+  intros a b f; constructor;
     refine (compose_cate_fun _ _ $@ _ $@ (id_cate_fun _)^$).
   - apply cate_issect.
   - apply cate_isretr.

theories/WildCat/Paths.v

@@ -48,33 +48,38 @@ Proof.
   exact (@ap _ _ (cat_precomp c f)).
 Defined.
 
-(** Any type is a 1-category with n-morphisms given by paths. *)
-Instance is1cat_paths {A : Type} : Is1Cat A.
+(** Any type is a 1-bicategory with n-morphisms given by paths. *)
+Instance is1bicat_paths {A : Type} : Is1Bicat A.
 Proof.
-  snapply Build_Is1Cat.
-  - exact _.
+  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
+  := is1cat_is1bicat A _.
+
 (** Any type is a 1-groupoid with morphisms given by paths. *)
 Instance is1gpd_paths {A : Type} : Is1Gpd A.
 Proof.
-  snapply Build_Is1Gpd.
-  - exact (@concat_pV A).
-  - exact (@concat_Vp A).
+  intros a b f; constructor.
+  - apply concat_pV.
+  - apply concat_Vp.
 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,33 +97,34 @@ 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.
-    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.
+  - intros a b c d.
     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.
+    + apply concat_pV.
+    + apply concat_Vp.
+  - 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).
   - intros a b c p q.
     exact (triangulator p q).
 Defined.
+
+Instance is21cat_paths {A : Type}
+  : Is21Cat A
+  := Build_Is21Cat _ _ _ _ _ _ _ _ _.