[Agda] [HoTT] Re: Why do we need judgmental equality?

[Andreas Abel]

 > CCed to the agda list. Maybe somebody can comment on the decidabilty 
status?

Ulrich Berger and Anton Setzer: Undecidability of Equality for Codata Types

     Talk given at CMCS'18 Thessaloniki, Greece, 15 April 2018

 
http://www.cs.swan.ac.uk/~csetzer/articles/CMCS2018/bergerSetzerProceedingsCMCS18.pdf


On 2019-02-17 08:56, Thorsten Altenkirch wrote:
> On 17/02/2019, 01:25, "homotopytypetheory at googlegroups.com on behalf of Michael Shulman" <homotopytypetheory at googlegroups.com on behalf of shulman at sandiego.edu> wrote:
> 
>      However, I don't find it
>      arbitrary at all: *negative* types have strict eta, while positive
>      types don't.
> 
> This is a very good point. However Streams are negative types but for example agda doesn't use eta conversion on them, I think for a good reason. Actually I am not completely sure whether this is undecidable.
> 
> E.g. the following equation cannot be proven using refl (it can be proven in cubical agda btw). The corresponding equation for Sigma types holds definitionally.
> 
> infix 5 _∷_
> 
> record Stream (A : Set) : Set where
>    constructor _∷_
>    coinductive
>    field
>      hd : A
>      tl : Stream A
> 
> open Stream
> etaStream : {A : Set}{s : Stream A} → hd s ∷ tl s ≡ s
> etaStream = {!refl!}
> 
> CCed to the agda list. Maybe somebody can comment on the decidabilty status?
> 
> 
> 
> 
> 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
>