nicer equivalence relations in category

ViCaR/Classes/Category.v

@@ -8,73 +8,49 @@ Reserved Notation "A ~> B" (at level 50).
 Reserved Notation "f ≃ g" (at level 60).
 Reserved Notation "A ≅ B" (at level 60).
 
-(* 
-    Might use these to abstract out the equality relations.
-        
-    Definition relation (A : Type) := A -> A -> Prop.
-    Definition reflexive {A : Type} (R : relation A) :=
-        forall a : A, R a a.
-    Definition transitive {A: Type} (R: relation A) :=
-        forall a b c : A, (R a b) -> (R b c) -> (R a c).
-    Definition symmetric {A: Type} (R: relation A) :=
-        forall a b : A, (R a b) -> (R b a).
-    Definition equivalence {A : Type} (R : relation A) := 
-        (reflexive R) /\ (symmetric R) /\ (transitive R). 
-*)
-
 Class Category (C : Type) : Type := {
     morphism : C -> C -> Type
         where "A ~> B" := (morphism A B);
 
-    equiv {A B : C} (f g : A ~> B) : Prop 
+    (* Morphism equivalence *)
+    equiv {A B : C} : relation (A ~> B)
         where "f ≃ g" := (equiv f g) : Cat_scope;
-    equiv_symm {A B : C} {f g : A ~> B} : 
-        f ≃ g -> g ≃ f;
-    equiv_trans {A B : C} {f g h : A ~> B} :
-        f ≃ g -> g ≃ h -> f ≃ h;
-    equiv_refl {A B : C} {f : A ~> B} :
-        f ≃ f;
-
-    obj_equiv (A B : C) : Prop 
-        where "A ≅ B" := (obj_equiv A B);
-    obj_equiv_symm {A B : C} : 
-        A ≅ B -> B ≅ A;
-    obj_equiv_trans {A B M : C} :
-        A ≅ B -> B ≅ M -> A ≅ M;
-    obj_equiv_refl {A : C} :
-        A ≅ A;
+    equiv_rel {A B : C} : equivalence (A ~> B) equiv;
 
-    c_identity (A : C) : A ~> A;
+    (* Object equivalence *)
+    obj_equiv : relation C
+        where "A ≅ B" := (obj_equiv A B) : Cat_scope;
+    obj_equiv_rel : equivalence C obj_equiv;
 
     compose {A B M : C} : 
         (A ~> B) -> (B ~> M) -> (A ~> M);
     compose_compat {A B M : C} : 
         forall (f g : A ~> B), f ≃ g ->
         forall (h j : B ~> M), h ≃ j ->
         compose f h ≃ compose g j;
-
-    left_unit {A B : C} {f : A ~> B} : compose (c_identity A) f ≃ f;
-    right_unit {A B : C} {f : A ~> B} : compose f (c_identity B) ≃ f;
     assoc {A B M N : C}
         {f : A ~> B} {g : B ~> M} {h : M ~> N} : 
         compose (compose f g) h ≃ compose f (compose g h);
+
+    c_identity (A : C) : A ~> A;
+    left_unit {A B : C} {f : A ~> B} : compose (c_identity A) f ≃ f;
+    right_unit {A B : C} {f : A ~> B} : compose f (c_identity B) ≃ f;
 }.
 
+Notation "A ~> B" := (morphism A B) : Cat_scope.
+Notation "f ≃ g" := (equiv f g) : Cat_scope. (* \simeq *)
+Notation "A ≅ B" := (obj_equiv A B) : Cat_scope. (* \cong *)
+Infix "∘" := compose (at level 40, left associativity) : Cat_scope. (* \circ *)
+
 Add Parametric Relation {C : Type} {Cat : Category C} 
-    (n m : C) : (morphism n m) (equiv)
-  reflexivity proved by (@equiv_refl C Cat n m)
-  symmetry proved by (@equiv_symm C Cat n m)
-  transitivity proved by (@equiv_trans C Cat n m)
+    (A B : C) : (A ~> B) equiv
+  reflexivity proved by (equiv_refl (A ~> B) equiv equiv_rel)
+  symmetry proved by (equiv_sym (A ~> B) equiv equiv_rel)
+  transitivity proved by (equiv_trans (A ~> B) equiv equiv_rel)
   as prop_equiv_rel.
 
 Add Parametric Morphism {C : Type} {Cat : Category C} (n o m : C) : compose
-  with signature (@equiv C Cat n m) ==> (@equiv C Cat m o) ==> 
-                 equiv as compose_mor.
+  with signature (@equiv C Cat n m) ==> (@equiv C Cat m o) ==> equiv as compose_mor.
 Proof. apply compose_compat; assumption. Qed.
 
-Notation "A ~> B" := (morphism A B) : Cat_scope.
-Notation "f ≃ g" := (equiv f g) : Cat_scope. (* \simeq *)
-Notation "A ≅ B" := (obj_equiv A B) : Cat_scope. (* \cong *)
-Infix "∘" := compose (at level 40, left associativity) : Cat_scope. (* \circ *)
-
-Local Close Scope Cat.
+Local Close Scope Cat.

examples/ZXExample.v

@@ -1,29 +1,42 @@
+Require Import Setoid.
+
 From VyZX Require Import CoreData.
 From VyZX Require Import CoreRules.
 From VyZX Require Import PermutationRules.
 From ViCaR Require Export CategoryTypeclass.
 
+Lemma proportional_equiv {n m : nat} : equivalence (ZX n m) proportional.
+Proof.
+    constructor.
+    unfold reflexive; apply proportional_refl.
+    unfold transitive; apply proportional_trans.
+    unfold symmetric; apply proportional_symm.
+Qed.
+
+Lemma equality_equiv : equivalence nat eq.
+Proof. 
+    constructor. 
+    unfold reflexive; easy.
+    unfold transitive; apply eq_trans.
+    unfold symmetric; apply eq_sym.
+Qed.
+
 #[export] Instance ZXCategory : Category nat := {
     morphism := ZX;
 
     equiv := @proportional;
-    equiv_symm := @proportional_symm;
-    equiv_trans := @proportional_trans;
-    equiv_refl := @proportional_refl;
+    equiv_rel := @proportional_equiv;
 
     obj_equiv := eq;
-    obj_equiv_symm := @eq_sym nat;
-    obj_equiv_trans := @eq_trans nat;
-    obj_equiv_refl := @eq_refl nat;
-
-    c_identity n := n_wire n;
+    obj_equiv_rel := equality_equiv;
 
     compose := @Compose;
     compose_compat := @Proportional.compose_compat;
+    assoc := @ComposeRules.compose_assoc;
 
+    c_identity n := n_wire n;
     left_unit _ _ := nwire_removal_l;
     right_unit _ _ := nwire_removal_r;
-    assoc := @ComposeRules.compose_assoc;
 }.
 
 Definition zx_associator {n m o} :=
@@ -266,7 +279,7 @@ Proof.
     apply functional_extensionality; intros.
     bdestruct_all; simpl in *; try lia.
     all: solve_simple_mod_eqns.
-Admitted.
+Qed.
 
 Lemma hexagon_lemma_1 : forall {n m o}, 
     (zx_braiding ↕ n_wire o) ⟷ zx_associator ⟷ (n_wire m ↕ zx_braiding)