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

[Matt Oliveri <atmacen@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 3379 bytes --]

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 <javascript:>> wrote: 
> > 
> > On 17/02/2019, 01:25, "homotopyt...@googlegroups.com <javascript:> on 
> behalf of Michael Shulman" <homotopyt...@googlegroups.com <javascript:> 
> on behalf of shu...@sandiego.edu <javascript:>> 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? 
>

-- 
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@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.2: Type: text/html, Size: 4677 bytes --]