List of generic types

Stream: new members

[Chase Norman]

I have created a type for a weighted directed graph on vertex type V:
def Graph (V: Type) := V → V → Nat
I would like to create a List, set, or other collection of Graphs with varying vertex types. However, because Graph is formally of type Type → Type, this cannot be done directly. Is there an idiomatic way to perform this kind of genericism?
Thanks.

[Patrick Johnson]

You can use docs4#Sigma:

def Graph (V : Type) : Type := V → V → Nat

def graph₁ : Graph Nat := λ _ _ => 0
def graph₂ : Graph Int := λ _ _ => 0

def myList : List (Σ V, Graph V) := [⟨_, graph₁⟩, ⟨_, graph₂⟩]

[Eric Wieser]

Note this only works if the types live in the same universe; if you'd used Type u instead of Type then you couldn't put a Graph Nat and a Graph (ulift.{37} Nat) in the same sigma type