What about infinitary (non-elementary) limits? Are there infinitary homotopy-limits? They are more common than discrete inductive types, right? So what if I considered a stream of A to be essentially an omega-fold product of A. Would that have a strict extensionality principle?

More generally, I would try and say that a coinductive type is some limit of an external diagram of elimination spines. This might address Thomas Streicher's objection, since the collection of elimination spines is countable externally.

On Sunday, February 17, 2019 at 4:19:01 AM UTC-5, Michael Shulman 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....@nottingham.ac.uk> wrote:
>
> On 17/02/2019, 01:25, "homotopyt...@googlegroups.com on behalf of Michael Shulman" <homotopyt...@googlegroups.com on behalf of shu...@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?