Skip to main content
1 of 2
Paul Taylor
  • 8.5k
  • 1
  • 29
  • 58

As the person who introduced the name "display map", I would like to emphasise that the whole point of doing so was to be able to do dependent type theory in categories that are NOT locally cartesian closed but "relatively" so. In an LCCC all maps are display maps.

see Chapter VIII of "Practical Foundations of Mathematics" (CUP 1999)

Paul Taylor
  • 8.5k
  • 1
  • 29
  • 58