Sort u →
  {G : Type u_1} →
    {X : Type u_2} →
      [inst : Group G] →
        [inst_1 : MulAction G X] →
          DiscreteTiling.Prototile G X →
            {G' : Type u_1} →
              {X' : Type u_2} →
                [inst' : Group G'] → [inst'_1 : MulAction G' X'] → DiscreteTiling.Prototile G' X' → Sort u