projects
/
coq-hetmet.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
reorganize flattening code
[coq-hetmet.git]
/
src
/
ReificationsIsomorphicToGeneralizedArrows.v
diff --git
a/src/ReificationsIsomorphicToGeneralizedArrows.v
b/src/ReificationsIsomorphicToGeneralizedArrows.v
index
756d250
..
25febe0
100644
(file)
--- a/
src/ReificationsIsomorphicToGeneralizedArrows.v
+++ b/
src/ReificationsIsomorphicToGeneralizedArrows.v
@@
-1,7
+1,7
@@
(*********************************************************************************************************************************)
(*********************************************************************************************************************************)
-(* ReificationsEquivalentToGeneralizedArrows: *)
+(* ReificationsIsomorphicToGeneralizedArrows: *)
(* *)
(* *)
-(* The category of generalized arrows and the category of reifications are equivalent categories. *)
+(* The category of generalized arrows and the category of reifications are isomorphic categories. *)
(* *)
(*********************************************************************************************************************************)
(* *)
(*********************************************************************************************************************************)
@@
-27,7
+27,8
@@
Require Import GeneralizedArrowFromReification.
Require Import ReificationFromGeneralizedArrow.
Require Import ReificationCategory.
Require Import GeneralizedArrowCategory.
Require Import ReificationFromGeneralizedArrow.
Require Import ReificationCategory.
Require Import GeneralizedArrowCategory.
-Require Import ReificationsEquivalentToGeneralizedArrows.
+Require Import ReificationCategory.
+Require Import ReificationsAndGeneralizedArrows.
Require Import WeakFunctorCategory.
Section ReificationsIsomorphicToGeneralizedArrows.
Require Import WeakFunctorCategory.
Section ReificationsIsomorphicToGeneralizedArrows.
@@
-43,16
+44,6
@@
Section ReificationsIsomorphicToGeneralizedArrows.
(step1_functor s0 s1 r01 >>>>
InclusionFunctor (enr_v s1) (FullImage (RepresentableFunctor s1 (me_i s1)))) >>>> step1_functor s1 s2 r12
≃ step1_functor s0 s2 (compose_reifications s0 s1 s2 r01 r12).
(step1_functor s0 s1 r01 >>>>
InclusionFunctor (enr_v s1) (FullImage (RepresentableFunctor s1 (me_i s1)))) >>>> step1_functor s1 s2 r12
≃ step1_functor s0 s2 (compose_reifications s0 s1 s2 r01 r12).
- unfold IsomorphicFunctors.
- simpl.
- idtac.
- unfold compose_reifications at 0.
- eapply Build_IsomorphicFunctors.
- unfold step1_functor.
- unfold InclusionFunctor.
- simpl.
- unfold functor_comp.
- simpl.
admit.
Defined.
admit.
Defined.