Zulip Chat Archive

Stream: Is there code for X?

Topic: How to handle `Type` in this definition

Iván Renison (Oct 17 2025 at 07:56):

Hi, if I have this definition:

inductive D : Type → Type → Type 1 where
  | I (a : Type) : D a a
  | U (a b : Type) : D a b
  | S (x : ℂ) : D Unit Unit
  | C (a b c : Type) : D a b → D b c → D a c

What would be the best way to handle the Types? I think that the current one is probably not the best. I tried making D : Type u → Type v → Type (max u v + 1) but I was not able

Etienne Marion (Oct 17 2025 at 08:07):

Not sure what is your goal and not very familiar with universes, but this works:

import Mathlib

universe u

inductive D : Type → Type → Type (u + 1) where
  | I (a : Type) : D a a
  | U (a b : Type) : D a b
  | S (x : ℂ) : D Unit Unit
  | C (a b c : Type) : D a b → D b c → D a c

and I am not sure you can do better because Unit has type Type.

Etienne Marion (Oct 17 2025 at 08:08):

Replacing u + 1 by max 1 u also works.

Kevin Buzzard (Oct 17 2025 at 08:29):

How can D : Type u → Type v → ... work if you want D a a to be a possibility?

import Mathlib

universe u

inductive D : Type u → Type u → Type _ where
  | I (a : Type u) : D a a
  | U (a b : Type u) : D a b
  | S (x : ℂ) : D PUnit PUnit
  | C (a b c : Type u) : D a b → D b c → D a c

gives _ = u + 1.

Iván Renison (Oct 17 2025 at 08:34):

I thought that for the case D a a, u and v would be the same

Iván Renison (Oct 17 2025 at 08:39):

If that is not posible then probably what you send is the best, thank you

Aaron Liu (Oct 17 2025 at 10:13):

this looks evil so I would want some more details before suggesting a solution

Kevin Buzzard (Oct 17 2025 at 11:20):

Iván Renison said:

I thought that for the case D a a, u and v would be the same

Oh I think there's a misunderstanding here. D is not one function which takes universes as inputs, D is in some sense infinitely many functions parametrised by universe variables. So for example if you manage to define D : Type u -> Type v -> Type (max u v) in Lean then in particular you must have just defined D : Type 37 -> Type 42 -> Type 42 and your proposed definition of D clearly isn't going to give something of this type because of I, so it can't work. Like docs#PUnit (which I used to lift Unit to Type u) you can use docs#ULift to lift Type u to Type v as long as u <= v, but if you don't know which of the universes is the biggest then this is going to cause extra confusion.

Yury G. Kudryashov (Oct 18 2025 at 17:47):

What does this type represent?

Iván Renison (Oct 20 2025 at 12:24):

That type was a smaller version of the actual type we have, witch represents dirac notation:

inductive DiracCore : Type → Type → Type 1 where
  | zero (α β) :
      DiracCore α β
  | one (α) :
      DiracCore α α
  | scalar (c : ℂ) :
      DiracCore Unit Unit
  | delta {α : Type} [DecidableEq α] (i j : α) :
      DiracCore Unit Unit
  | ket {α} (t : α):
      DiracCore α Unit
  | bra {α} (t : α):
      DiracCore Unit α

  | add {α β} :
      DiracCore α β → DiracCore α β → DiracCore α β
  | mul {α β γ} :
      DiracCore α β → DiracCore β γ → DiracCore α γ
  | tsr {α β α' β'} :
      DiracCore α β → DiracCore α' β' → DiracCore (α × α') (β × β')
  | adj {α β} :
      DiracCore α β → DiracCore β α

  | reidx {α β α' β'} :
      α ≃ α' → β ≃ β' → DiracCore α β → DiracCore α' β'

The idea is that the α and β are the indexes the matrices corresponding to the elements. We want to define this function:

def semantic : {α : Type} → {β : Type} → [DecidableEq α] → [DecidableEq β] → DiracCore α β → Matrix α β ℂ
  | _, _, _, _, .zero _ _ => 0
  | _, _, _, _, .one _ => 1
  | _, _, _, _, DiracCore.delta i j => if i = j then 1 else 0
  ፧