[Agda] Prop in Agda 2.6

[Andrew Pitts]

Dear John,

> On 22 May 2019, at 18:28, Jon Sterling <jon at jonmsterling.com> wrote:
> 
> Hi Andy,
> 
> This seems consistent with an interpretation of non-cubical agda into extensional type theory,

or, to put it crudely, the set theoretic model of type theory can give a model of these axioms.

> but I just want to mention something I'd noticed before: if you wanted to add 'untrunc' to Agda, you might be tempted to have a beta rule. But this appropriate beta rule would induce equality reflection for proofs of propositions, which one probably doesn't want in the formal system.

Interesting. Can we clarify what you mean? If A : Set and e : isProp A, then for any x : A we have that untrunc e (squash x) and x are propositionally equal (using e). Conversely for any y :  ∥ A ∥ we have that squash (untrunc e y) and y are both elements of ∥ A ∥ in Prop and so are definitionally equal. Were you suggesting not making a REWRITE for untrunc e (squash x) and x? (I don’t think I need to)

Andy

> 
> Best,
> Jon
> 
> 
> 
> On Wed, May 22, 2019, at 12:47 PM, Andrew Pitts wrote:
>> I’m interested in using the built-in sort of definitionally 
>> proof-irrelevant propositions that Agda 2.6 introduced. I have 
>> readthedocs at 
>> <https://agda.readthedocs.io/en/latest/language/prop.html>.
>> 
>> For the development I have in mind (which assumes axiom K) I need Prop 
>> to be extensional
>> 
>> postulate
>>  propext :
>>    {l : Level}
>>    {P Q : Prop l}
>>    (_ : P → Q)
>>    (_ : Q → P)
>>    → ------------
>>    P ≡ Q
>> 
>> and to be able to “untruncate hprops" (in particular, to be able to 
>> untruncate identity types, in the presence of axiom K).
>> 
>> data ∥_∥ {l : Level}(A : Set l) : Prop l where
>>  squash : A → ∥ A ∥
>> 
>> isProp : {l : Level} → Set l → Set l
>> isProp A = (x y : A) → x ≡ y
>> 
>> postulate
>>  untrunc :
>>    {l : Level}
>>     {A : Set l}
>>     (_ : isProp A)
>>     → ------------
>>     ∥ A ∥ → A
>> 
>> Neither of the postulates propext or untrunc is provable in Agda 2.6, is it?
>> 
>> I think they are logically consistent axioms. But is there a better way 
>> than just postulating them?
>> 
>> Andy
>> 
>> 
>> 
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda