projects
/
coq-hetmet.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
organize Extraction-prefix.hs a bit
[coq-hetmet.git]
/
src
/
WeakFunctorCategory.v
diff --git
a/src/WeakFunctorCategory.v
b/src/WeakFunctorCategory.v
index
49a5189
..
85ade61
100644
(file)
--- a/
src/WeakFunctorCategory.v
+++ b/
src/WeakFunctorCategory.v
@@
-192,8
+192,8
@@
Section WeakFunctorCategoryIsomorphism.
apply q.
Defined.
apply q.
Defined.
- Theorem WeakFunctorCategoriesIsomorphic : IsomorphicCategories GA RE F1 F2.
- apply Build_IsomorphicCategories.
+ Theorem WeakFunctorCategoriesIsomorphic : IsomorphicCategories GA RE.
+ refine {| ic_f := F1 ; ic_g := F2 |}.
unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
eapply if_comp.
apply m1_m2_id.
unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
eapply if_comp.
apply m1_m2_id.