Added Relations example (over types), with individual structures for …

…product (through CompactClosed & DaggerSymmetricMonoidal) and sum (through SymmetricMonoidal & DaggerSymmetricMonoidal), as well as showing the latter cannot be a CompactClosedCategory.
inQWIRE · Mar 8, 2024 · b9b3c46 · b9b3c46
1 parent 2b2d006
commit b9b3c46
Show file tree

Hide file tree

Showing 3 changed files with 530 additions and 2 deletions.
diff --git a/ViCaR/Classes/ExamplesAutomation.v b/ViCaR/Classes/ExamplesAutomation.v
@@ -2,9 +2,9 @@ From VyZX Require Import PermutationAutomation.
 Require Import String.
 
 Ltac print_state :=
-  try (match goal with | H : ?p |- _ => idtac H ":" p; fail end);
+  try (match reverse goal with | H : ?p |- _ => idtac H ":" p; fail end);
   idtac "---------------------------------------------------------";
-  match goal with |- ?P => idtac P; idtac "" 
+  match reverse goal with |- ?P => idtac P; idtac "" 
 end.
 
 Ltac is_C0 x := assert (x = C0) by (cbv; lca).

diff --git a/examples/NatRelationsExample.v b/examples/NatRelationsExample.v
@@ -1,4 +1,5 @@
 Require Import Setoid.
+From ViCaR Require Export CategoryTypeclass.
 
 Require Import Psatz.