Monoidal coherence

theories/Basics/PathGroupoids.v

@@ -832,6 +832,16 @@ Proof.
   apply concat_1p.
 Defined.
 
+(** We can see [concat_A1p] and [concat_pA1] as saying that for [e] a left or right unit of some multiplication [*], the unitor [e * x = x] is natural. [concat_Ap_assoc] proves that for an associative multiplication, the associator is natural. *)
+Definition concat_Ap_assoc {A: Type} (op : A -> A -> A)
+  (assoc : forall x y z, op x (op y z) = op (op x y) z)
+  (x x' y y' z z' : A) (f : x = x') (g : y = y') (h : z = z')
+  : (ap011 op f (ap011 op g h)) @ assoc x' y' z' = assoc x y z @ ap011 op (ap011 op f g) h.
+Proof.
+  destruct f, g, h.
+  exact (concat_1p_p1 _).
+Defined.
+
 (** It would be nice to have a consistent way to name the different ways in which this can be dependent.  The following are a sort of half-hearted attempt. *)
 
 Definition ap011D {A B C} (f : forall (a:A), B a -> C)

theories/Spaces/List/Theory.v

@@ -72,6 +72,27 @@ Proof.
     napply (ap_compose (fun l => l ++ z)).
 Defined.
 
+(** The triangle condition for a monoidal category, complementing [list_pentagon]. *)
+Definition list_triangle {A: Type} (x y : list A)
+  : idpath (a :=  x ++ y) = app_assoc x nil y @ ap011 app (app_nil x) 1.
+Proof.
+  revert y.
+  induction x as [| x0 x IHx]. 
+  - reflexivity.
+  - intro y.
+    change (app_nil (x0 :: x)) with (ap (cons x0) (app_nil x)); simpl.
+    rewrite ap011_is_ap, concat_p1.
+    rewrite <- ap_compose.
+    change (fun x1 : list A => (x0 :: x1) ++ y) with
+      (fun x1 : list A => (cons x0 (x1 ++ y))).
+    rewrite (ap_compose (fun x1 => x1 ++ y)).
+    rewrite <- ap_pp.
+    rewrite <- IHx.
+    apply ap_1.
+Defined.
+
+
+
 (** The length of a concatenated list is the sum of the lengths of the two lists. *)
 Definition length_app {A : Type} (l l' : list A)
   : length (l ++ l') = length l + length l'.

theories/WildCat/Equiv.v

@@ -719,3 +719,30 @@ Proof.
   - intros g r s.
     exact (Build_Cat_IsBiInv g r g s).
 Defined.
+
+(** ** Equivalences in groupoids *)
+
+(** All morphisms in 1-groupoids are equivalences. This is not an instance so that it can be used only when needed. *)
+Definition hasequivs_1gpd (A : Type) `{Is1Gpd A} : HasEquivs A.
+Proof.
+  snapply Build_HasEquivs.
+  - intros x y.
+    exact (x $== y).
+  - exact (fun _ _ _ => Unit).
+  - intros x y.
+    exact idmap.
+  - intros x y f.
+    exact tt.
+  - intros x y f _.
+    exact f.
+  - simpl; intros x y f _.
+    exact (Id _).
+  - intros x y f.
+    exact f^$.
+  - intros x y f.
+    exact (gpd_issect f).
+  - intros x y f.
+    exact (gpd_isretr f).
+  - intros x y f g p q.
+    exact tt.
+Defined.