canonical type with 2 terms in universe `u`

Stream: Is there code for X?

[Kevin Buzzard]

We have pempty and punit -- anyone for pbool? Otherwise I'm going to have to use ulift (fin 2) or something :-/

[Reid Barton]

there's punit ⊕ punit

[Kevin Buzzard]

You can see what I'm trying to do here and it occurs to me that being able to case on terms might be really useful, so I'm leaning towards defining pbool right now.

[Scott Morrison]

pnat! :-)

[Kevin Buzzard]

funnily enough my post-doc Maria and I were talking about that and pint the other day. She is defining valuations on Dedekind domains and their fraction fields coming from maximal ideals of the domain, and these valuations take values in with_zero (multiplicative nat) and with_zero (multiplicative int). However docs#valued has the value group in the same universe as the ring, so etc etc etc. In the end she restricted to Dedekind domains in Type. Are we evil?

[Kevin Buzzard]

Oh -- you cannot see in the API docs that Γ₀ : Type u.

[Yury G. Kudryashov]

Or you can generalize valued to valued.{v u} with Γ₀ : Type v