add inverse form of ni_commutes
[coq-categories.git] / src / Presheaves_ch9_7.v
1 Generalizable All Variables.
2
3 (*******************************************************************************)
4 (* Chapter 9.7: Presheaves                                                     *)
5 (*******************************************************************************)
6
7
8
9