From 15f6147aab33c49aeb870892bed2e22c2ba139de Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Thu, 4 Jul 2024 14:51:29 +0200
Subject: [PATCH 1/3] add comment to Products.v

Signed-off-by: Ali Caglayan <alizter@gmail.com>

<!-- ps-id: 7d047c94-9393-4dce-88fc-04fb36a74098 -->
---
 theories/WildCat/Products.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/WildCat/Products.v b/theories/WildCat/Products.v
index da9236bbb3b..12d186c22ba 100644
--- 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)

From f723a45ccba4102cd88d9dcad46522729ceeb6a6 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Thu, 4 Jul 2024 14:54:43 +0200
Subject: [PATCH 2/3] composed bifunctor instances

Signed-off-by: Ali Caglayan <alizter@gmail.com>

<!-- ps-id: e0996497-9e64-4954-9dff-984a6faa0776 -->
---
 theories/WildCat/Bifunctor.v | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v
index 865f8ceb6b6..f6625ba4560 100644
--- 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}

From e28fbfaa9786a5cdcda15891d616f66c5f4c3850 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Thu, 4 Jul 2024 14:55:17 +0200
Subject: [PATCH 3/3] rename opposite initial/terminal instances

Signed-off-by: Ali Caglayan <alizter@gmail.com>

<!-- ps-id: 55a4d338-836f-4570-b7da-31bc9702dde5 -->
---
 theories/WildCat/Opposite.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/WildCat/Opposite.v b/theories/WildCat/Opposite.v
index 1c515862c38..8d26289d5bf 100644
--- 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.