Significantly improved category automation. Fenceposting has been imp…

…lemented in Ltac, and appears to be correct in some limited tests. More testing should be done. Performance is also poor at the moment: there are some fixes that should be possible immediately, but other issues (particularly with to_Cat) may require a tradeoff of speed and efficacy (which can be shifted onto the user with multiple tactics). Also, Universe Polymorphism has been enabled in all category files, so that Categories whose morphisms have specific universes (really, 'whose morphisms are in Set') play nicely. We now have 'ZXCategory.(morphism) = ZX', which previously failed due to universe constraints, and in doing so significantly hampered automation (which requires conversion of the local context to category names so it can match on them).

ViCaR/Classes/BraidedMonoidal.v

@@ -2,6 +2,8 @@ Require Import Category.
 Require Import Monoidal.
 Require Import Setoid.
 
+#[local] Set Universe Polymorphism.
+
 Local Open Scope Cat.
 
 Notation CommuteBifunctor' F := ({|

ViCaR/Classes/CastCategory.v

@@ -1,8 +1,10 @@
 Require Import Setoid.
 
 Require Export CategoryTypeclass.
+Require Logic.Eqdep_dec. (* only for UIP_dec *)
+Require PeanoNat. (* only for eq_dep on nat *)
 
-Require Import ExamplesAutomation.
+#[local] Set Universe Polymorphism.
 
 Local Open Scope Cat.
 
@@ -605,7 +607,7 @@ Definition CastCategory_of_DecEq_Category {C : Type} (cC: Category C)
     match HA in (_ = a) return (a ~> B' -> A ~> B) with (* Tell coq that A = A' *)
     | eq_refl =>
       fun f => 
-      match HB in (_ = a) return (A ~> a -> A ~> B) with 
+      match HB in (_ = b) return (A ~> b -> A ~> B) with 
       | eq_refl => fun f' => f'
       end f
     end;
@@ -616,7 +618,17 @@ Definition CastCategory_of_DecEq_Category {C : Type} (cC: Category C)
 |}.
 
 Definition CastCategory_of_NatCategory (cC: Category nat) :
-  @CastCategory nat cC.
-apply CastCategory_of_DecEq_Category.
-apply PeanoNat.Nat.eq_dec.
-Defined.
+  @CastCategory nat cC := {|
+  cast := fun A B A' B' HA HB =>
+    match HA in (_ = a) return (a ~> B' -> A ~> B) with (* Tell coq that A = A' *)
+    | eq_refl =>
+      fun f => 
+      match HB in (_ = b) return (A ~> b -> A ~> B) with 
+      | eq_refl => fun f' => f'
+      end f
+    end;
+  cast_refl := ltac:(intros A B HA HB; 
+    rewrite (Eqdep_dec.UIP_refl_nat _ HA);
+    rewrite (Eqdep_dec.UIP_refl_nat _ HB);
+    reflexivity);
+|}.

ViCaR/Classes/Category.v

@@ -4,6 +4,8 @@ Declare Scope Cat_scope.
 Delimit Scope Cat_scope with Cat.
 Local Open Scope Cat.
 
+#[local] Set Universe Polymorphism.
+
 Reserved Notation "A ~> B" (at level 55).
 Reserved Notation "f ≃ g" (at level 60).
 Reserved Notation "A ≅ B" (at level 60).
@@ -354,8 +356,6 @@ Qed.
 Definition ContravariantFunctor {C D : Type} (cC: Category C) (cD : Category D) : Type :=
   Functor (cC^op) cD.
 
-Require Import ExamplesAutomation.
-
 Definition ContravariantFunctor_of_ContraFunctor {C D : Type} 
   `{cC : Category C} `{cD : Category D} (F : ContraFunctor cC cD) : 
   ContravariantFunctor cC cD := {|

ViCaR/Classes/CompactClosed.v

@@ -3,6 +3,8 @@ Require Import Monoidal.
 Require Import BraidedMonoidal.
 Require Import SymmetricMonoidal.
 
+#[local] Set Universe Polymorphism.
+
 Local Open Scope Cat.
 
 Reserved Notation "A ★" (at level 0).

ViCaR/Classes/Dagger.v

@@ -1,6 +1,8 @@
 Require Import Setoid.
 Require Import Category.
 
+#[local] Set Universe Polymorphism.
+
 Local Open Scope Cat.
 
 Reserved Notation "f †" (at level 0).