TY - RPRT TI - On the strength of proof-irrelevant type theories AU - Benjamin Werner PY - 2008 DO - 10.2168/lmcs-4(3:13)2008 UR - https://arxiv.org/abs/0808.3928 ID - 0808.3928 ER -