projects
/
coq-categories.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
major revision: MonoidalCat is now a subclass of PreMonoidalCat
[coq-categories.git]
/
src
/
NaturalIsomorphisms_ch7_5.v
diff --git
a/src/NaturalIsomorphisms_ch7_5.v
b/src/NaturalIsomorphisms_ch7_5.v
index
3371671
..
415d13c
100644
(file)
--- a/
src/NaturalIsomorphisms_ch7_5.v
+++ b/
src/NaturalIsomorphisms_ch7_5.v
@@
-3,7
+3,6
@@
Require Import Preamble.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
-Require Import ProductCategories_ch1_6_1.
(*******************************************************************************)
(* Chapter 7.5: Natural Isomorphisms *)
(*******************************************************************************)
(* Chapter 7.5: Natural Isomorphisms *)
@@
-224,6
+223,7
@@
Definition if_respects
Defined.
Section ni_prod_comp.
Defined.
Section ni_prod_comp.
+Require Import ProductCategories_ch1_6_1.
Context
`{C1:Category}`{C2:Category}
`{D1:Category}`{D2:Category}
Context
`{C1:Category}`{C2:Category}
`{D1:Category}`{D2:Category}
@@
-251,3
+251,4
@@
Section ni_prod_comp.
split; reflexivity.
Defined.
End ni_prod_comp.
split; reflexivity.
Defined.
End ni_prod_comp.
+