Merge branch 'master' into ps/rr/opposite_monoidal_categories

HoTT · Jul 4, 2024 · f02879a · f02879a
2 parents 8730d51 + d1ffba6
commit f02879a
Show file tree

Hide file tree

Showing 3 changed files with 28 additions and 2 deletions.
diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v
@@ -355,6 +355,15 @@ Proof.
   exact _.
 Defined.
 
+Global Instance is1functor_uncurry_uncurry_left {A B C D E}
+  (F : A -> B -> C) (G : C -> D -> E)
+  `{Is1Cat A, Is1Cat B, Is1Cat C, Is1Cat D, Is1Cat E,
+    !Is0Bifunctor F, !Is1Bifunctor F, !Is0Bifunctor G, !Is1Bifunctor G}
+  : Is1Functor (uncurry (uncurry (fun x y z => G (F x y) z))).
+Proof.
+  exact _.
+Defined.
+
 Global Instance is0functor_uncurry_uncurry_right {A B C D E}
   (F : A -> B -> D) (G : C -> D -> E)
   `{IsGraph A, IsGraph B, IsGraph C, IsGraph D, IsGraph E,
@@ -366,6 +375,21 @@ Proof.
   exact (fmap11 G h (fmap11 F f g)).
 Defined.
 
+Global Instance is1functor_uncurry_uncurry_right {A B C D E}
+  (F : A -> B -> D) (G : C -> D -> E)
+  `{Is1Cat A, Is1Cat B, Is1Cat C, Is1Cat D, Is1Cat E,
+    !Is0Bifunctor F, !Is1Bifunctor F, !Is0Bifunctor G, !Is1Bifunctor G}
+  : Is1Functor (uncurry (uncurry (fun x y z => G x (F y z)))).
+Proof.
+  snrapply Build_Is1Functor.
+  - intros cab cab' [[h f] g] [[h' f'] g'] [[q p] r].
+    exact (fmap22 G q (fmap22 F p r)).
+  - intros cab.
+    exact (fmap12 G _ (fmap11_id F _ _) $@ fmap11_id G _ _).
+  - intros cab cab' cab'' [[h f] g] [[h' f'] g'].
+    exact (fmap12 G _ (fmap11_comp F _ _ _ _) $@ fmap11_comp G _ _ _ _).
+Defined.  
+
 Definition fmap11_square {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
   (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
   {a00 a20 a02 a22 : A} {f10 : a00 $-> a20} {f12 : a02 $-> a22}

diff --git a/theories/WildCat/Opposite.v b/theories/WildCat/Opposite.v
@@ -127,10 +127,10 @@ Proof.
   refine (@isequiv_Htpy_path _ _ _ _ _ H0 b a f g).
 Defined.
 
-Global Instance isinitial_isterminal_op {A : Type} `{Is1Cat A} (x : A)
+Global Instance isinitial_op_isterminal {A : Type} `{Is1Cat A} (x : A)
   {t : IsTerminal x} : IsInitial (A := A^op) x
   := t.
 
-Global Instance isterminal_isinitial_op {A : Type} `{Is1Cat A} (x : A)
+Global Instance isterminal_op_isinitial {A : Type} `{Is1Cat A} (x : A)
   {i : IsInitial x} : IsTerminal (A := A^op) x
   := i.
diff --git a/theories/WildCat/Products.v b/theories/WildCat/Products.v
@@ -567,6 +567,8 @@ Proof.
   snrapply cat_binprod_corec; exact (Id _).
 Defined.
 
+(** *** Lemmas about [cat_binprod_corec] *)
+
 Definition cat_binprod_fmap01_corec {A : Type}
   `{Is1Cat A, !HasBinaryProducts A} {w x y z : A}
   (f : w $-> z) (g : x $-> y) (h : w $-> x)