finish implementation of PreMonoidalFullsubcategory
[coq-categories.git] / src / Exponentials_ch6.v
1 (*******************************************************************************)
2 (* Closed Categories                                                           *)
3
4 (*Definition ClosedCategory `(C:Category)(CI:C) :=*)