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

[Thorsten Altenkirch]

For me the idea of inductive vs coinductive or how I called this a while ago data vs codata is an important basic intuition which comes before formal model constructions. Types are defined by constructors or by destructors, eg coproducts are defined by constructors while functions are defined by destructors, namely application. That is a function is something you can apply to arguments obtaining a result. Lambda is a derived construction, I can construct a function if I have a method to compute the result. Similarily natural numbers and lists are given by constructors, while streams are defined by destructors, to give a stream means to be able to say what its head and its tail are. And that is perfectly right Sigma types can be either given by a constructor or by destructors so in this sense they are twitters. 

There are reductions which just means that certain type formers are universal in that we can define all other from them, e.g. function types together with some inductive types are sufficient to derive a certain class of codata types. That doesn't mean that the dichotomy between data and codata isn't an important basic intuition.

On 17/02/2019, 09:19, "Michael Shulman" <shulman at sandiego.edu> wrote:

    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.
    




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.