def pair : (A : Type 2) × A :=
  ⟨Type 1, Type 0⟩