(*******************************************************************************) (* Closed Categories *) (*Definition ClosedCategory `(C:Category)(CI:C) :=*)