From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Sat, 26 Mar 2011 09:13:02 +0000 (-0700)
Subject: fix {Reification,GeneralizedArrow}Category
X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=ac32299199705b8824231454a21af4ca70eedd7f

fix {Reification,GeneralizedArrow}Category
---

diff --git a/src/GeneralizedArrowCategory.v b/src/GeneralizedArrowCategory.v
index d98f85a..974fdc3 100644
--- a/src/GeneralizedArrowCategory.v
+++ b/src/GeneralizedArrowCategory.v
@@ -24,6 +24,6 @@ Require Import Enrichment_ch2_8.
 Require Import RepresentableStructure_ch7_2.
 Require Import GeneralizedArrow.
 
-Instance CategoryOfGeneralizedArrows : Category SMME GeneralizedArrow.
+Definition CategoryOfGeneralizedArrows : Category SMME (fun x y => @GeneralizedArrow x _ y).
   admit.
   Qed.
diff --git a/src/ReificationCategory.v b/src/ReificationCategory.v
index eb6b5fd..d271c02 100644
--- a/src/ReificationCategory.v
+++ b/src/ReificationCategory.v
@@ -24,6 +24,6 @@ Require Import Enrichment_ch2_8.
 Require Import RepresentableStructure_ch7_2.
 Require Import Reification.
 
-Instance CategoryOfReifications : Category SMME Reification.
+Definition CategoryOfReifications : Category SMME (fun x y:SMME => Reification (smme_e x) (smme_e y) (mon_i (smme_mon y))).
   admit.
   Qed.
\ No newline at end of file