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

[Michael Shulman]

Well, I'm not really convinced that coinductive types should be
treated as basic type formers, rather than simply constructed out of
inductive types and extensional functions.  For one thing, I have no
idea how to construct coinductive types as basic type formers in
homotopical models.  I think the issue that you raise, Thorsten, could
be regarded as another argument against treating them basically, or at
least against regarding them as really "negative" in the same way that
Pis and (negative) Sigmas are.

And as for adding random extra strict equalities pertaining certain
positive types that happen to hold in some particular model, Matt, I
would say similarly that the general perspective gives yet another
reason why you shouldn't do that.  (-:

But the real point is that the general perspective I was proposing
doesn't claim to be the *only* way to do things; obviously it isn't.
It's just a non-arbitrary "baseline" that is consistent and makes
sense and matches a common core of equalities used in many type
theories, so that when you deviate from it you're aware that you're
being deviant.  (-:

On Sat, Feb 16, 2019 at 11:56 PM Thorsten Altenkirch
<Thorsten.Altenkirch at nottingham.ac.uk> 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.
>
>
>
>
> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe at googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.