Define quiver as inductive type.

Stream: new members

[Rémi Bottinelli]

Hey, trying to define a quiver as an inductive type, I'm getting the error invalid inductive datatype, resultant type is not a sort which I can't really make sense of. I tried fiddling with universes, but it doesn't seem to help. Is there a way to make this snippet work?

import category_theory.category.basic
import category_theory.functor.basic
import combinatorics.quiver.basic

open set classical function
local attribute [instance] prop_decidable


universes u v u' v' u'' v''


section push_quiver


variables {V : Type u} [quiver.{v+1} V] {V' : Type u'} (σ : V → V')

def push {V : Type u} [quiver.{v+1} V] {V' : Type u'} (σ : V → V')  := V'
def push_quiver : quiver (push σ) := ⟨λ X' Y', Σ (X: {X // σ X = X'}) (Y : {Y // σ Y = Y'}), X.val ⟶ Y.val⟩

-- would be better but get universe troubles
inductive push_quiver_arrows {V : Type u} [quiver.{v+1} V] {V' : Type u'} (σ : V → V') : quiver V'
| mk {X Y : V} (f : X ⟶ Y) : push_quiver_arrows (σ X) (σ Y)

end push_quiver

[Yaël Dillies]

An inductive with a single non-recursive constructor is a structure. So why not just use structure?

[Yaël Dillies]

I can't really make sense of what you wrote, because the return type of push_quiver_arrows is quiver V', not V' → V' → Sort*.

[Yaël Dillies]

Note that quiver V is not definitionally equal to V → V → Sort*. So you should wrap a V → V → Sort* explicitly rather than letting Lean figure out that you think quiver V is the same as V → V → Sort*.

[Rémi Bottinelli]

I wanted to make this using an inductive type after Joel Rioux proposal to make the following into an inductive def.

[Rémi Bottinelli]

Now I'm dumbly trying to make as much as possible into inductive types, and figured it would also work here.

[Rémi Bottinelli]

But I guess the difference was that in that case, the hom_rel type is defeq to … -> Prop, is that it?

[Yaël Dillies]

I mean, yes, it will work, but you need the return type to be V' → V' → Sort*, not quiver V'

[Yaël Dillies]

Here it makes sense to make it an inductive because push_quiver_arrows (σ X) (σ Y) doesn't match all push_quiver_arrows X Y.

[Yaël Dillies]

The fact that's it an inductive doesn't have anything to do with the error. It's like doing

def foo : quiver V := λ x y, empty -- fails

instead of

def bar : quiver V := ⟨λ x y, empty⟩

[Rémi Bottinelli]

Right, that makes sense. It's just that quiver is a struct and hom_rel was a definition.

[Rémi Bottinelli]

Thanks for taking the time to help me figure out this basic stuff, @Yaël Dillies !