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