CatDat

Implication Details

Assumptions: elementary topos

Conclusions: locally cartesian closed

Reason: See Johnstone, Cor. A2.3.4.