[Agda] Defining equality in Prop

[Christian Sattler]

On Tue, 23 Jun 2020 at 17:47, Andrew M. Pitts <amp12 at cam.ac.uk> wrote:

> 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.
>
> Andy
>

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.

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.

Best wishes,
Christian
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200623/1efd20c6/attachment.html>