From 9cd83c1c00ba30389899b7194519a3470ba4a3eb Mon Sep 17 00:00:00 2001
From: Laura Zielinski <76456473+lczielinski@users.noreply.github.com>
Date: Fri, 5 Apr 2024 15:43:19 -0500
Subject: [PATCH 1/8] Update README.md

---
 README.md | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/README.md b/README.md
index abf77e8..cf9d841 100644
--- a/README.md
+++ b/README.md
@@ -1,8 +1,10 @@
-# ViCaR
+# ViCAR
 
-Verified Categorical String Diagrams in Roq
+**Vi**sualizing **C**ategories with **A**utomated **R**ewriting in Coq
 
-## Building ViCaR
+## ACT Submission: See this tag
+
+## Building ViCAR
 
 Tested with Coq 8.14-8.18.
 

From f2e9051103ed6e700a36b0b34c62d437daed1f04 Mon Sep 17 00:00:00 2001
From: Laura Zielinski <76456473+lczielinski@users.noreply.github.com>
Date: Fri, 5 Apr 2024 16:15:35 -0500
Subject: [PATCH 2/8] Update README.md

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index cf9d841..3eea313 100644
--- a/README.md
+++ b/README.md
@@ -2,7 +2,7 @@
 
 **Vi**sualizing **C**ategories with **A**utomated **R**ewriting in Coq
 
-## ACT Submission: See this tag
+### **ACT Submission: See [this](https://github.com/inQWIRE/ViCaR/releases/tag/act-submission) tag**
 
 ## Building ViCAR
 

From 8103026474f593a23d9605dab60fe11bd6de85f6 Mon Sep 17 00:00:00 2001
From: Ben Caldwell <caldwellb@uchicago.edu>
Date: Wed, 17 Apr 2024 09:40:48 -0500
Subject: [PATCH 3/8] Small proof repair + coq-action update

---
 .github/workflows/coq-action.yml |  1 +
 ViCaR/Classes/BraidedMonoidal.v  | 14 ++++++++------
 2 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml
index 413a028..8fe9435 100644
--- a/.github/workflows/coq-action.yml
+++ b/.github/workflows/coq-action.yml
@@ -17,6 +17,7 @@ jobs:
           - '8.16'
           - '8.17'
           - '8.18'
+          - '8.19'
           - 'dev'
         ocaml_version:
           - 'default'
diff --git a/ViCaR/Classes/BraidedMonoidal.v b/ViCaR/Classes/BraidedMonoidal.v
index 347a26b..af8af03 100644
--- a/ViCaR/Classes/BraidedMonoidal.v
+++ b/ViCaR/Classes/BraidedMonoidal.v
@@ -40,8 +40,8 @@ Class BraidedMonoidalCategory {C : Type} {cC : Category C}
   
   MonoidalCategory_of_BraidedMonoidalCategory := mC;
 }.
-Arguments BraidedMonoidalCategory {_} {_}%Cat (_)%Cat.
-Arguments braiding {_} {_}%Cat {_}%Cat (_)%Cat.
+Arguments BraidedMonoidalCategory {_} {_}%_Cat (_)%_Cat.
+Arguments braiding {_} {_}%_Cat {_}%_Cat (_)%_Cat.
 Notation "'B_' x , y" := (braiding _%Cat x%Obj y%Obj) 
   (at level 20) : Brd_scope.
 
@@ -75,13 +75,15 @@ Lemma hexagon_resultant_1 {C} {cC : Category C} {mC : MonoidalCategory cC}
   id_ B ⊗ B_ M, A ∘ B_ B, (A×M) ∘ associator A M B ∘ id_ A ⊗ (B_ B, M)^-1
   ≃ associator B M A ^-1 ∘ B_ (B × M), A.
 Proof.
-  (* rewrite <- compose_iso_l. *)
   pose proof (hexagon_2 A B M) as hex2.
-  rewrite <- (compose_tensor_iso_r' _ (IdentityIsomorphism _)).
+  replace (id_ A) with (IdentityIsomorphism A ^-1) by easy.
+  rewrite <- (compose_tensor_iso_r' (associator B M A ^-1 ∘ B_ B × M, A) (IdentityIsomorphism A) (B_ B, M)).
   simpl.
   rewrite 2!compose_iso_r.
   rewrite !assoc.
   rewrite <- compose_iso_l.
+  Check compose_tensor_iso_r.
+  replace (id_ B) with (forward (IdentityIsomorphism B)) by easy.
   rewrite (compose_tensor_iso_r _ (IdentityIsomorphism _)).
   rewrite assoc, compose_iso_l'.
   symmetry in hex2.
@@ -93,6 +95,7 @@ Proof.
   apply compose_cancel_r.
   pose proof (hexagon_1 B A M) as hex1.
   rewrite <- compose_iso_l'.
+  replace (id_ M) with (IdentityIsomorphism M ^-1) by easy.
   rewrite <- (compose_tensor_iso_l' _ (IdentityIsomorphism _)).
   simpl.
   rewrite <- 3!assoc.
@@ -101,5 +104,4 @@ Proof.
   easy.
 Qed.
 
-
-Local Close Scope Cat.
\ No newline at end of file
+Local Close Scope Cat.

From 3ef69c0f485b35ca1ad49043260ffc94b5b13226 Mon Sep 17 00:00:00 2001
From: Ben Caldwell <caldwellb@uchicago.edu>
Date: Wed, 17 Apr 2024 09:44:15 -0500
Subject: [PATCH 4/8] Undid change from %Cat to %_Cat, is a breaking change

---
 ViCaR/Classes/BraidedMonoidal.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/ViCaR/Classes/BraidedMonoidal.v b/ViCaR/Classes/BraidedMonoidal.v
index af8af03..cabbf7b 100644
--- a/ViCaR/Classes/BraidedMonoidal.v
+++ b/ViCaR/Classes/BraidedMonoidal.v
@@ -40,8 +40,8 @@ Class BraidedMonoidalCategory {C : Type} {cC : Category C}
   
   MonoidalCategory_of_BraidedMonoidalCategory := mC;
 }.
-Arguments BraidedMonoidalCategory {_} {_}%_Cat (_)%_Cat.
-Arguments braiding {_} {_}%_Cat {_}%_Cat (_)%_Cat.
+Arguments BraidedMonoidalCategory {_} {_}%Cat (_)%Cat.
+Arguments braiding {_} {_}%Cat {_}%Cat (_)%Cat.
 Notation "'B_' x , y" := (braiding _%Cat x%Obj y%Obj) 
   (at level 20) : Brd_scope.
 

From 195647c7d011b5073a00b936b7ee46b30fc34291 Mon Sep 17 00:00:00 2001
From: Ben Caldwell <caldwellb@uchicago.edu>
Date: Wed, 17 Apr 2024 09:49:59 -0500
Subject: [PATCH 5/8] Updated README.md, coq-vicar.opam version, dune-project
 version, and coq-action version.

---
 .github/workflows/coq-action.yml | 2 --
 README.md                        | 4 ++--
 coq-vicar.opam                   | 4 ++--
 dune-project                     | 2 +-
 4 files changed, 5 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml
index 8fe9435..49704c4 100644
--- a/.github/workflows/coq-action.yml
+++ b/.github/workflows/coq-action.yml
@@ -12,8 +12,6 @@ jobs:
     strategy:
       matrix:
         coq_version:
-          - '8.14'
-          - '8.15'
           - '8.16'
           - '8.17'
           - '8.18'
diff --git a/README.md b/README.md
index 3eea313..4998320 100644
--- a/README.md
+++ b/README.md
@@ -6,9 +6,9 @@
 
 ## Building ViCAR
 
-Tested with Coq 8.14-8.18.
+Currently supports Coq 8.16-8.19.
 
-To build ViCaR, run `make vicar`
+To build ViCaR, run `make vicar`.
 
 
 ## Examples
diff --git a/coq-vicar.opam b/coq-vicar.opam
index b630cfb..41644b4 100644
--- a/coq-vicar.opam
+++ b/coq-vicar.opam
@@ -1,6 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "0.1.0"
+version: "0.1.1"
 synopsis: "Coq library reasoning about categorical string diagrams"
 description: """
 inQWIRE's ViCaR is a library for reasoning about
@@ -13,7 +13,7 @@ homepage: "https://github.com/inQWIRE/ViCaR"
 bug-reports: "https://github.com/inQWIRE/ViCaR/issues"
 depends: [
   "dune" {>= "2.8"}
-  "coq" {>= "8.12"}
+  "coq" {>= "8.16"}
   "odoc" {with-doc}
 ]
 build: [
diff --git a/dune-project b/dune-project
index a57ea96..c9f0a92 100644
--- a/dune-project
+++ b/dune-project
@@ -18,4 +18,4 @@
  )
 
  (depends
-   (coq (>= 8.12))))
+   (coq (>= 8.16))))

From bd6ae287051a0c6f96743e95224a280d28a8aa89 Mon Sep 17 00:00:00 2001
From: Ben Caldwell <caldwellb@uchicago.edu>
Date: Wed, 17 Apr 2024 10:02:47 -0500
Subject: [PATCH 6/8] Updated README with basic instructions for visualization.

---
 README.md      | 8 ++++++++
 coq-vicar.opam | 8 ++++----
 2 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/README.md b/README.md
index 4998320..a70642e 100644
--- a/README.md
+++ b/README.md
@@ -10,6 +10,14 @@ Currently supports Coq 8.16-8.19.
 
 To build ViCaR, run `make vicar`.
 
+## Installing ViCAR through opam
+
+To install ViCAR through opam, run 
+```bash
+opam pin -y coq-vicar https://github.com/inQWIRE/ViCAR.git
+```
+
+To use the visualizer, first have [coq-lsp](https://github.com/ejgallego/coq-lsp) installed, then install the VSCode extension found at [https://marketplace.visualstudio.com/items?itemName=inQWIRE.vizcar]. After instantiating the appropriate typeclass you would like to visualize you can run the vizcar command in vscode to activate visualizing. The vizcar plugin only visualizes terms using the ViCAR grammar. To automatically take a term to the ViCAR grammar, use the `categorify` tactic.
 
 ## Examples
 
diff --git a/coq-vicar.opam b/coq-vicar.opam
index 41644b4..72db620 100644
--- a/coq-vicar.opam
+++ b/coq-vicar.opam
@@ -3,14 +3,14 @@ opam-version: "2.0"
 version: "0.1.1"
 synopsis: "Coq library reasoning about categorical string diagrams"
 description: """
-inQWIRE's ViCaR is a library for reasoning about
+inQWIRE's ViCAR is a library for reasoning about
  categorical string diagrams
 """
 maintainer: ["inQWIRE Developers"]
 authors: ["inQWIRE"]
 license: "MIT"
-homepage: "https://github.com/inQWIRE/ViCaR"
-bug-reports: "https://github.com/inQWIRE/ViCaR/issues"
+homepage: "https://github.com/inQWIRE/ViCAR"
+bug-reports: "https://github.com/inQWIRE/ViCAR/issues"
 depends: [
   "dune" {>= "2.8"}
   "coq" {>= "8.16"}
@@ -30,4 +30,4 @@ build: [
     "@doc" {with-doc}
   ]
 ]
-dev-repo: "git+https://github.com/inQWIRE/ViCaR.git"
+dev-repo: "git+https://github.com/inQWIRE/ViCAR.git"

From 0bc61ab66bac82c7bfc9fc429fffc606ad62469e Mon Sep 17 00:00:00 2001
From: Ben Caldwell <caldwellb@uchicago.edu>
Date: Wed, 17 Apr 2024 10:14:35 -0500
Subject: [PATCH 7/8] Updated README visualization instructions

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index a70642e..8d418ea 100644
--- a/README.md
+++ b/README.md
@@ -17,7 +17,7 @@ To install ViCAR through opam, run
 opam pin -y coq-vicar https://github.com/inQWIRE/ViCAR.git
 ```
 
-To use the visualizer, first have [coq-lsp](https://github.com/ejgallego/coq-lsp) installed, then install the VSCode extension found at [https://marketplace.visualstudio.com/items?itemName=inQWIRE.vizcar]. After instantiating the appropriate typeclass you would like to visualize you can run the vizcar command in vscode to activate visualizing. The vizcar plugin only visualizes terms using the ViCAR grammar. To automatically take a term to the ViCAR grammar, use the `categorify` tactic.
+To use the visualizer, first have [coq-lsp](https://github.com/ejgallego/coq-lsp) installed, then install the VSCode extension found at [https://marketplace.visualstudio.com/items?itemName=inQWIRE.vizcar]. After instantiating the appropriate typeclass you would like to visualize you can run the vizcar command in vscode to activate visualizing. The vizcar plugin only visualizes terms using the ViCAR grammar. To automatically take a term with an instantiated typeclass to the ViCAR grammar, use the `to_Cat` tactic.
 
 ## Examples
 

From 46b12b34ecb8e538efc2aefcc82c01561a6ea896 Mon Sep 17 00:00:00 2001
From: Ben Caldwell <caldwellb@uchicago.edu>
Date: Wed, 17 Apr 2024 12:36:16 -0500
Subject: [PATCH 8/8] Fixed compilation issues

---
 ViCaR/Classes/BraidedMonoidal.v | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/ViCaR/Classes/BraidedMonoidal.v b/ViCaR/Classes/BraidedMonoidal.v
index 375f79d..392d155 100644
--- a/ViCaR/Classes/BraidedMonoidal.v
+++ b/ViCaR/Classes/BraidedMonoidal.v
@@ -69,7 +69,7 @@ Lemma hexagon_resultant_1 (A B M : C) :
 Proof.
   pose proof (hexagon_2 A B M) as hex2.
   replace (id_ A) with (IdentityIsomorphism A ^-1) by easy.
-  rewrite <- (compose_tensor_iso_r' (associator B M A ^-1 ∘ B_ B × M, A) (IdentityIsomorphism A) (B_ B, M)).
+  rewrite <- (compose_tensor_iso_r' (associator B M A ^-1 ∘ β_ B × M, A) (IdentityIsomorphism A) (β_ B, M)).
   simpl.
   rewrite 2!compose_iso_r.
   rewrite !(assoc).
@@ -86,7 +86,7 @@ Proof.
   rewrite <- !(assoc).
   apply compose_cancel_r.
   pose proof (hexagon_1 B A M) as hex1.
-  rewrite <- compose_iso_l'.
+  rewrite assoc, <- compose_iso_l'.
   replace (id_ M) with (IdentityIsomorphism M ^-1) by easy.
   rewrite <- (compose_tensor_iso_l' _ (IdentityIsomorphism _)).
   simpl.
@@ -96,4 +96,6 @@ Proof.
   easy.
 Qed.
 
-Local Close Scope Cat.
\ No newline at end of file
+End BraidedCoherenceRewrites.
+
+Local Close Scope Cat.