<div dir="ltr"><div dir="ltr">On Tue, 23 Jun 2020 at 17:47, Andrew M. Pitts <<a href="mailto:amp12@cam.ac.uk" target="_blank">amp12@cam.ac.uk</a>> wrote:<br></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">I have found the proof irrelevant Prop in recent versions of Agda to be very useful indeed in the context of type theory with uniqueness of identity proofs (Axiom K) and heterogeneous Prop-valued equality, so long as one postulates the Axiom of Unique Choice (A!C), enabling one to soundly escape from Prop to Set, if you see what I mean. The attached example file contains a formulation of A!C and the definite descriptions it enables, towards the end.<br>
<br>
Andy<br></blockquote><div><br></div><div>Relatedly, I have found it useful even in settings without K (but usually with function extensionality) to postulate that the canonical map from strict Prop to hProp (the universe of homotopy propositions, defined using the standard identity type) is an equivalence (of h-preorders). It unfolds to mean that the map A → ∃ A reverses for any h-prop A. Under K, this should be equivalent to Andrew's postulate.</div><div><br></div><div>This is justified by any model with extensional equality as well as (classically) the simplicial set model. However, in constructive models of homotopy type theory, the usual exact completion problems form an obstacle to this axiom.</div><div><br></div><div>Best wishes,</div><div>Christian </div></div></div>