Inductives via parametricity (was Re: [HoTT] universe-polymorphic assumptions)

[Jason Gross]

Does internal parametricity also give you higher inductive types via church encodings?  (I would be surprised if it did, since then it would solve the problem of computing with HITs, I presume.)

Separately, if you formulate the identity type via church encoding, and use internal parametricity to define J, what judgmental computation rules, if any, does it have?

-Jason

On Jul 8, 2015 6:52 AM, "Neelakantan Krishnaswami" <n.krish...@cs.bham.ac.uk> wrote:

On 08/07/15 08:31, Michael Shulman wrote:

On Tue, Jul 7, 2015 at 11:25 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

ind-gives-it :
    (N : U₀)
    (z : N)
    (s : N → N)
    (ind : ∀ {i} {A : N → U{i}} → A z → (∀ n → A n → A(s n)) → ∀ n → A n)
  → ∀ {i} {X : U{i}} (x : X) (f : X → X) → N → X

Whoa, really?  Agda lets you hypothesize a universe-polymorphic
argument just like any other argument?

Apparently so! I didn't realize that Agda permitted this, myself.

Do people think that's consistent?What universe does

> ind-gives-it live in?

I have been thinking about this on and off for a while, and while
I haven't worked out all the details, it seems fairly straightforward
show that universe-polymorphic definitions are consistent using a PER
model of type theory (in the style of the Nuprl semantics).

Roughly speaking, a fully universe-polymorphic definition cannot
use any construction not available at all universe levels, and so it's
safe to put it in the bottom universe. This is rather powerful,
since (as Martin implicitly observes) it means that the Church naturals
live in the bottom universe, but nevertheless can be used to produce
up large eliminations.

Best,
Neel

PS -- My interest in this arises from the fact that if you additionally
internalize reasoning about parametricity, then seemingly everything we
can do with direct inductive type definitions can also be done with
Church encodings.

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

[Neelakantan Krishnaswami]

Hi Jason,

I don't know. I've focused on parametricity with proof-irrelevant
relations, which in HoTT terms means I've looked at type theories
where all types are h-sets. I think Bob Atkey, Neil Ghani, and a few
others have been looking at models of proof-relevant relational
parametricity. I know they are interested in applications to HoTT,
but don't know the current status of that work.

I'll answer your other question in email, since it's off-topic for
the list.

Best,
Neel

On 08/07/15 21:50, Jason Gross wrote:
> Does internal parametricity also give you higher inductive types via
> church encodings? (I would be surprised if it did, since then it would
> solve the problem of computing with HITs, I presume.)
>
> Separately, if you formulate the identity type via church encoding, and
> use internal parametricity to define J, what judgmental computation
> rules, if any, does it have?
>
> -Jason
>
> On Jul 8, 2015 6:52 AM, "Neelakantan Krishnaswami"

> <mailto:HomotopyTypeTheory%2Bunsu...@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 HomotopyTypeThe...@googlegroups.com

> <mailto:HomotopyTypeThe...@googlegroups.com>.