Some changes in response to reviewer comments

Author: Patrick Nicodemus

theories/Basics/PathGroupoids.v

@@ -96,30 +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.
-
-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.
+  (concat_p_pp p q r)^.
 
 (** The left inverse law. *)
 Definition concat_pV {A : Type} {x y : A} (p : x = y) :

theories/WildCat/Paths.v

@@ -71,8 +71,8 @@ Instance is1cat_paths {A : Type} : Is1Cat A
 Instance is1gpd_paths {A : Type} : Is1Gpd A.
 Proof.
   intros a b f; constructor.
-  - exact (@concat_pV A _ _ _).
-  - exact (@concat_Vp A _ _ _).
+  - apply concat_pV.
+  - apply concat_Vp.
 Defined.
 
 (** Any type is a 2-category with higher morphisms given by paths. *)
@@ -104,8 +104,8 @@ Proof.
     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).
+    + apply concat_pV.
+    + apply concat_Vp.
   - intros a b f; constructor.
     + exact (concat_pV _).
     + exact (concat_Vp _).

theories/WildCat/TwoOneCat.v

@@ -1,4 +1,5 @@
 Require Import Basics.Overture Basics.Tactics.
+Require Import Types.Forall.
 Require Import WildCat.Core.
 Require Import WildCat.NatTrans.
 Require Import WildCat.Prod.
@@ -10,7 +11,11 @@ Local Open Scope twocat.
 
 (** * Wild (2,1)-categories *)
 
+(** This file introduces two basic 2-dimensional structures, (2,1)-categories and bicategories. Bicategories classically have 0-cells, 1-cells and 2-cells; our presentation includes 3-cells expressing coherence relations between 2-cells, that would classically be expressed as truncated equalities. The paradigmatic example of a bicategory is the bicategory of categories, functors and natural transformations. Other common bicategories are the bicategory of sets and spans, the bicategory of rings and ring bimodules, and the bicategory of categories and profunctors. A (2,1)-category is a bicategory where all 2-cells are invertible; a (2,1)-category can also be seen as an ordinary category extended with coherence conditions on 2-cells, expressed as 3-cells. *)
+
 (** ** Wild 1-categorical structures *)
+
+(** We start by introducing the common core of the theory of 1-categories and the theory of bicategories. A wild 1-bicategory is like a wild 1-category, but without the requirement that the 2-cells are invertible in general. The theory of 1-bicategories is the fragment of the theory of bicategories containing all 0-cells, 1-cells and 2-cells, but subject to no coherence conditions between 2-cells (which would require 3-cells to express.) *)
 Class Is1Bicat (A : Type) `{!IsGraph A, !Is2Graph A, !Is01Cat A} :=
 {
   is01bicat_hom :: forall (a b : A), Is01Cat (a $-> b) ;
@@ -26,6 +31,7 @@ Class Is1Bicat (A : Type) `{!IsGraph A, !Is2Graph A, !Is01Cat A} :=
   bicat_idr_opp : forall {a b : A} (f : a $-> b), f $=> f $o Id a;
 }.
 
+(** A wild 1-category is precisely a wild 1-bicategory such that the 2-cells are invertible. *)
 Definition is1cat_is1bicat (A : Type) `{Is1Bicat A}
   (p : forall a b : A, Is0Gpd (Hom a b))
   : Is1Cat A.
@@ -37,6 +43,7 @@ Proof.
   - exact (@bicat_idr _ _ _ _ _).
 Defined.
 
+(** Conversely, forgetting the inverses of 2-cells, one recovers a 1-bicategory from a 1-category. *)
 Definition is1bicat_is1cat (A : Type) `{Is1Cat A}
   : Is1Bicat A.
 Proof.
@@ -60,8 +67,8 @@ Instance is0bifunctor_bicat_comp (A : Type) `{Is1Bicat A} (a b c : A)
 Instance Is0Functor_swap (A: Type) `{Is1Bicat A} (a b c : A)
   : Is0Functor (fun '(f,g) => cat_comp (a:=a) (b:=b) (c:=c) g f).
 Proof.
-  change (fun p => snd p $o fst p) with (fun p => (Types.Forall.flip (cat_comp (a:=a) (b:=b) (c:=c)) (fst p) (snd p))).
-  rapply (is0functor_bifunctor_uncurried (Forall.flip (cat_comp))).
+  change (fun p => snd p $o fst p) with (fun p => (flip (cat_comp (a:=a) (b:=b) (c:=c)) (fst p) (snd p))).
+  rapply (is0functor_bifunctor_uncurried (flip (cat_comp))).
   rapply is0bifunctor_flip.
 Defined.
 
@@ -87,6 +94,7 @@ Proof.
   exact ((alpha $@@ beta) $@@ gamma).
 Defined.
 
+(** The full structure of a bicategory, incorporating all appropriate coherence conditions. *)
 Class IsBicat (A : Type) `{H: Is1Bicat A} `{!Is3Graph A} :=
 {
   is1cat_hom :: forall (a b : A), Is1Cat (a $-> b) ;
@@ -116,6 +124,7 @@ Class IsBicat (A : Type) `{H: Is1Bicat A} `{!Is3Graph A} :=
       (g $@L bicat_idl f) $o (bicat_assoc f (Id b) g) $== (bicat_idr g $@R f)
 }.
 
+(** A (2,1)-category is a bicategory such that all 2-cells have a unique inverse. Here we have chosen to define (2,1)-categories as extending the theory of bicategories, but the theory of (2,1)-categories also extends the theory of 1-categories with coherence conditions on 2-cells. TODO: Give a constructor to upgrade a 1-category to a (2,1)-category by adding appropriate coherence conditions. *)
 Class Is21Cat (A : Type) `{IsBicat A} :=
 {
   is0gpd_hom :: forall (a b : A), Is0Gpd (a $-> b) ;

theories/WildCat/Universe.v

@@ -1,6 +1,6 @@
 Require Import Basics.Overture Basics.Tactics Basics.Equivalences Basics.PathGroupoids.
 Require Import Types.Equiv.
-Require Import WildCat.Core WildCat.Equiv WildCat.NatTrans WildCat.TwoOneCat WildCat.Bifunctor.
+Require Import WildCat.Core WildCat.Equiv WildCat.NatTrans WildCat.TwoOneCat WildCat.Bifunctor WildCat.Prod.
 
 (** ** The (1-)category of types *)
 
@@ -160,7 +160,7 @@ Lemma Type_associator_natural (A B C D: Type)
   (p : f == f') (q : g == g') (r : h == h') (x : A)
   : hcomp (hcomp r q) p x @ 1 = 1 @ hcomp r (hcomp q p) x.
 Proof.
-  unfold Bifunctor.fmap11, Prod.fmap_pair; simpl.
+  unfold fmap11, fmap_pair; simpl.
   refine (concat_p1 _ @ _ @ (concat_1p _)^).
   refine (whiskerR (ap_compose _ _ _) _ @ _).
   exact (concat_p_pp _ _ _ @ (whiskerR (ap_pp _ _ _)^ _)).