From 9b27f2c7b66e583a886f8c7a802512dc402b3f11 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Fri, 25 Mar 2011 09:59:25 -0700 Subject: [PATCH] update imports in EquivalentCategories --- src/EquivalentCategories_ch7_8.v | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/EquivalentCategories_ch7_8.v b/src/EquivalentCategories_ch7_8.v index 7918cf3..e5bcfb2 100644 --- a/src/EquivalentCategories_ch7_8.v +++ b/src/EquivalentCategories_ch7_8.v @@ -1,14 +1,14 @@ -Generalizable All Variables. -Require Import Preamble. -Require Import General. -Require Import ch1_3_Categories. -Require Import ch1_4_Functors. -Require Import ch1_5_Isomorphisms. - (*******************************************************************************) (* Chapter 7.8: Equivalent Categories *) (*******************************************************************************) +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import Categories_ch1_3. +Require Import Functors_ch1_4. +Require Import Isomorphisms_ch1_5. + (* Definition 7.24 *) Class EquivalentCategories `(C:Category)`(D:Category){Fobj}{Gobj}(F:Functor C D Fobj)(G:Functor D C Gobj) := { ec_forward : F >>>> G ≃ functor_id C -- 1.7.10.4