CoeSort + Actual Sort

Stream: Is there code for X?

[Robert Maxton]

What's the easiest way to spell "something that is either a Sort u, or at least has a CoeSort instance?"

More specifically, I want to be able to accept functions of the type α → α → Sort* , but I also need to be able to write EquivLike _ a b for (a b : α), so α needs to be coercible to a Sort. I don't want to actually restrict to Sort* → Sort _ → Sort*, though, because then not only my own function but the function passed can't make use of any properties of α beyond those of Sort*. I considered just using a direct sum, but to be honest that sounds like it's likely to be quite inconvenient both for me and any users of the tactic I'm writing, as we'd end up constantly having to do case splits. If that's what I have to do then that's what I have to do, but I thought I'd at least check first.

I'd like to just require a CoeSort instance, but unfortunately, it seems that Sorts themselves are not coercible to Sort (or at least #synth CoeSort (Type u) (Type u) finds nothing.)

[Robert Maxton]

... I guess I can just write an inductive typeclass and make an instance for Sort and an instance that turns CoeSort into my typeclass, but then I basically run into right into Chesterton's Fence: why doesn't CoeSort already have instances for Sorts? It seems like whatever the answer to that is, it will probably apply to my custom typeclass as well.

[Eric Wieser]

This sounds like an #xy problem; can you describe in a little more detail what you're actually trying to do?

[Robert Maxton]

Essentially, I want to be able to write something like

  def TFAEType {α : Type*} (eqv : α → α → Sort*) (l : List α) :=
    ∀ x ∈ l, ∀ y ∈ l, EquivLike (EqvGen' eqv x y) x y

(where EqvGen' is EqvGen but for (α → α → Sort*)). Basically, I wantTFAEType to be defined in such a way that the actual underlying isomorphisms are defined and can be composed, so that I can automatically generate the correct isos as part of a related tactic later. But unless I resort to importing BundledHoms or something (which I believe ends up adding a dependency onto a large chunk of the category theory libraries), that means that x and y need to be coercible to Sort.

[Robert Maxton]

My current approach is

@[aesop safe unfold]
def TFAEType {α : Type*} (eqv : α → α → Sort*) {β : α → Sort _}
    [∀ (a b : α), (EquivLike (EqvGen' eqv a b) on β) a b] (l : List α) :=
  ∀ x ∈ l, ∀ y ∈ l, EqvGen' eqv x y

which... might work for me? But it depends on how well Lean can e.g. infer that β is just identity if α is already a Sort u; I haven't had the chance to really test the user-friendliness of this def yet

[Eric Wieser]

Can you make that a mwe by including EqvGen'?

[Robert Maxton]

Not really, because EqvGen' itself is something I'm working on that only sort of "works." (In particular Lean is insisting that it be either always-Prop or never-Prop and this is putting a big hole in my use case.)

import Mathlib.Data.FunLike.Equiv
import Mathlib.Tactic.Common

  variable {α : Sort u} (r: α → α → Sort v)


  /--`EqvGen' r` is the equivalence relation generated by the relation `r`.

  This is basically just `EqvGen`, but generalized to `Sort u`.-/
  inductive EqvGen' : α → α → Type (max u v)
   | rel   : ∀ a b, r a b → EqvGen' a b
   | refl  : ∀ a, EqvGen' a a
   | symm  : ∀ a b, EqvGen' a b → EqvGen' b a
   | trans : ∀ a b c, EqvGen' a b → EqvGen' b c → EqvGen' a c

-- @[aesop safe unfold]
def TFAEType {α : Type*} (eqv : α → α → Sort*) {β : α → Sort _}
    [∀ (a b : α), (EquivLike (EqvGen' eqv a b) on β) a b] (l : List α) :=
  ∀ x ∈ l, ∀ y ∈ l, EqvGen' eqv x y

This compiles, at least...

[Robert Maxton]

Bleck. Part of the issue, of course, is figuring out what EqvGen' should even be. The above is just copypasta from EqvGen; it sort of works (in that it compiles and kind of represents the thing I want), but since it doesn't actually specify a function for refl, symm, trans, it's not really suited for purpose I don't think