Added [Trunc_resp_equiv], modulo outstanding lemma [ap_equiv].