Generalizable All Variables. (*******************************************************************************) (* Chapter 9.7: Locally Cartesian Closed Categories *) (*******************************************************************************) (* Proposition 9.20: TFAE for categories with a terminal object: it is LCCC, every slice is CCC *)