src/LCCCs_ch9_7.v

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