Zulip Chat Archive

Stream: Is there code for X?

Topic: Predicates on predicates involving instances


view this post on Zulip Aaron Anderson (Aug 10 2020 at 07:16):

Is there a smoother way to do this:

def hereditary (P : Π (A : Type u) [group A], Prop) : Prop :=
   (A : Type u) [i : group A] (B : @subgroup A i), @P A i  P B

view this post on Zulip Aaron Anderson (Aug 10 2020 at 07:17):

Where I can define a predicate on predicates on groups, and then have functions like P and subgroup infer that A is a group, without repeatedly using @?

view this post on Zulip Aaron Anderson (Aug 10 2020 at 07:19):

(My real intention is to be able to define a Fraisse class based on my definition of first-order substructure, but I think this is a good MWE based only on mathlib https://en.wikipedia.org/wiki/Fra%C3%AFss%C3%A9_limit)

view this post on Zulip Eric Wieser (Aug 10 2020 at 07:43):

I think something like this works:

 (A : Type u) [i : group A], by exactI  (B : subgroup A), P A  P B

Last updated: May 07 2021 at 22:14 UTC