Pi.group for Prop

Stream: Is there code for X?

[Sky Wilshaw]

Do we have docs4#Pi.group where I : Prop?

{I : Prop} {f : I → Type v} [(i : I) → Group (f i)] : Group ((i : I) → f i)

[Eric Wieser]

No, but @Yaël Dillies has asked for this before

[Yaël Dillies]

(in the same context of Con(NF), actually)

[Eric Wieser]

I think the problem is that we can't have one instance for both because it would live in a universe that's not sufficiently obviously in Type

[Eric Wieser]

And it has to live in Type because we decided that only types are allowed to be groups

[Sky Wilshaw]

Is there a problem with supplying both instances, or is it just undesirable?

[Yaël Dillies]

It's not just a matter of supplying both instances, but also maintaining an entire parallel API.

[Sky Wilshaw]

That makes sense. The cost sounds pretty high given how few people will use such a feature.

[Eric Rodriguez]

Is there any harm with using the existing instance with PLift? Also I'm curious, what's the intended use?

[Sky Wilshaw]

The use case is that I want the group structure on ∀ x : α, [Foo x] → G x. More precisely, Foo encodes the x that have been "calculated so far" in a very large induction.

[Yaël Dillies]

To be quite fair, you could just make Foo Type-valued and everything should still work.

[Sky Wilshaw]

That's true, but there are some very good reasons this particular Foo should be in Prop!