From ac32299199705b8824231454a21af4ca70eedd7f Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sat, 26 Mar 2011 02:13:02 -0700 Subject: [PATCH] fix {Reification,GeneralizedArrow}Category --- src/GeneralizedArrowCategory.v | 2 +- src/ReificationCategory.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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 -- 1.7.10.4