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