Univalent polymorphism

van den Berg, B

van den Berg, B (corresponding author), Univ Amsterda, ILLC, POB 94242, NL-1090 GE Amsterdam, Netherlands.

ANNALS OF PURE AND APPLIED LOGIC, 2020; 171 (6):

Abstract

We show that Martin Hyland's effective topos can be exhibited as the homotopy category of a path category EFF. Path categories are categories of fibra......

Full Text Link