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

[Michael Shulman <shulman@sandiego.edu>]

On Sun, Feb 17, 2019 at 4:08 AM Matt Oliveri <atmacen@gmail.com> wrote:
> 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?

Yes, that might work.  I think that the last time I thought about
coinductive types in homotopy models I was trying to give them some
kind of dependent coinduction principle.  But if we take seriously the
positive/negative perspective that I advanced before, we would expect
coinductive types to have simply a destructor, a non-dependent
corecursor, a beta-rule for destructing the corecursor, and an
eta-principle saying something like that the endomorphism defined from
the destructor and the corecursor is the identity.  And that would
probably be modeled by the omega-fold product of a type with itself.

More generally, if F is a functor that preserves fibrations, fibrant
objects, and sequential limits (like F(X) = A x X for streams), then
the infinite limit

... -> F(F(F(1))) -> F(F(1)) -> F(1) -> 1

might be a model for the corresponding coinductive type with such an
eta-principle.

So maybe there's nothing wrong with coinductive types as such, and the
point is just that computational considerations like decidability
don't always match up with the principled category-theoretic
explanations.  (-:

> 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?
>
> --
> 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.

-- 
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.