[Agda] rewriting before defining

[Thorsten Altenkirch]

On 01/03/2018, 09:30, "Agda on behalf of Andreas Abel" <agda-bounces at lists.chalmers.se on behalf of abela at chalmers.se> wrote:


>Well, the doctor could perform some surgery on Agda, take out the 
>cancerous error message and see what happens. ;-)

I was hoping that a surgeon who is better versed with the Agda source would do this for me. :-) In particular I don’t really want to use a non-standard version of Agda.

>I wash my hands in innocence.  For me, the intended use of REWRITE was 
>to add a proven propositional equality to definitional equality; if you 
>go beyond it, you have to worry about the semantics yourself.

You are right. Basically REWRITE is a limited form of equality reflection. I do prove this equality only I am proving it mutually with its use. This you can certainly do when you have full equality reflection. I shouldn’t need to introduce postulates here.

This particular instance enables me to define semisimplicial types without using a 2-level theory (the 2-level approach was described in our CSL 2016 paper http://www.cs.nott.ac.uk/~psztxa/publ/csl16.pdf). The rewrite version is both better from a pragmatic view (easier to use - I think) and from a semantic point (there are interpretations or type theory that model semisimplical types but not a (strong) 2-level theory where Nat is fibrant - at least that is what Mike Shulman told me).

In this setting we certainly do not want to have full equality reflection because it would destroy proof relevance and hence it is in this form incompatible with univalence. However, I claim that this instance of equality reflection is harmless (this is a conjecture). 

We know that REWRITE can destroy soundness - so no difference here.

Thorsten

>
>Cheers,
>Andreas
>
>On 28.02.2018 19:07, Thorsten Altenkirch wrote:
>> Hi,
>> 
>> I am mutually defining an equality and some other things. To be able to 
>> type check the other things I need the equality as a rewriting rule but 
>> agda doesn't let me.
>> 
>> That is I get the error
>> Rewrite rule from function  Skm-∘  cannot be added before the function 
>> definition
>> when checking the pragma REWRITE Skm-∘
>> when checking the attached file.
>> 
>> I know that I am cheating but I want to do it. Can I tell it that I am a 
>> doctor and I know what I am doing. Otherwise I shouldn't be allowed to 
>> use Rewrite anyway.
>> 
>> Yes, I can replace it by a postulate but that misses the point.
>> 
>> Cheers,
>> Thorsten
>> 
>> 
>> This message and any attachment are intended solely for the addressee
>> and may contain confidential information. If you have received this
>> message in error, please contact the sender and delete the email and
>> attachment.
>> 
>> Any views or opinions expressed by the author of this email do not
>> necessarily reflect the views of the University of Nottingham. Email
>> communications with the University of Nottingham may be monitored
>> where permitted by law.
>> 
>> 
>> 
>> 
>> 
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>> 
>
>
>-- 
>Andreas Abel  <><      Du bist der geliebte Mensch.
>
>Department of Computer Science and Engineering
>Chalmers and Gothenburg University, Sweden
>
>andreas.abel at gu.se
>http://www.cse.chalmers.se/~abela/
>_______________________________________________
>Agda mailing list
>Agda at lists.chalmers.se
>https://lists.chalmers.se/mailman/listinfo/agda



This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.