About the choice of Set Level in Syntax

[DKXXXL]

Dear Kovacs and Kaposi, Hello! I wonder how you guys usually choose the set level when QIIT the syntax?

postulate
  Con   : ∀ i → Set (suc i)
  Ty    : ∀ {j}(Γ : Con j) i → Set (suc i ⊔ j)
  ∙     : Con zero
  _▶_   : ∀ {i}(Γ : Con i){j}(A : Ty Γ j) → Con (i ⊔ j)
  Sub   : ∀ {i}(Γ : Con i){j}(Δ : Con j) → Set (i ⊔ j)
  Tm    : ∀ {i}(Γ : Con i){j}(A : Ty Γ j) → Set (i ⊔ j)
  _[_]T : ∀ {i}{Δ : Con i}{j}(A : Ty Δ j){k}{Γ : Con k}(σ : Sub Γ Δ) → Ty Γ j

I guess it directly comes from standard model, (i.e. first construct standard model for the syntax and then postulate the syntax from the standard model) but then why not choose other models (maybe other standard models? I am not sure if it is unique) instead?

Is it possible that some specific choices of set level will disrupt the construction of the canonicity/normalization models in the future?

Or there is some pattern in this postulation I didn't see?

Thanks for any enlightening comments! Ende Jin

[akaposi]

The syntax should be in the lowest universe. If you have the syntax as a QIIT in cubical Agda, then that's where it lives, and also that's how you should postulate the syntax. If you use the shallow embedding trick to obtain a strict model and you treat it as if it was the syntax, then the model enforces some universe level and that's what you you have to use. Maybe it would be more honest to use type-in-type when defining the shallow embedded "syntax" and make it live in the lowest universe.

On the other hand, the canonicity displayed model works for the standard model viewed as the standard model (and not as syntax), and then it is just a way to select the canonical elements from that particular model.

[DKXXXL]

The syntax should be in the lowest universe

I think I am more of asking what is the pattern of the universe polymorphism used here.

If the lowest suffice, then why not let all of them live in Set0?

Con and Ty have to succ the level, in my opinion, because in standard model Con is interpreted as Set i and Ty is interpreted as a function type.
But according to your comment, if the set level is directly from syntax, do you mean that I cannot construct a cubical syntactic model for Con : Set0, Ty : (G : Con) -> Set0 ?

Also the other question is, why _[_]T is returning Ty of level j, instead of their union like all the other constructors above?

[AndrasKovacs]

Tbh I don't think that the universe polymorphism in Syntax here is necessary, maybe it was copied from somewhere where we needed a universe-polymorphic notion of model. A postulated syntax should just be in Set0.

[DKXXXL]

Tbh I don't think that the universe polymorphism in Syntax here is necessary, maybe it was copied from somewhere where we needed a universe-polymorphic notion if model. A postulated syntax should just be in Set0.

Thanks! Is it because, in standard model, U i will need to be mapped to Set i and if I make the former i : Nat then it requires an Agda non-admitted function Nat -> Level. Thus U, as a syntax piece, has to have type U : (i : Level) -> Set (succ i)? And this makes the postulate syntax universe polymorphic?

[AndrasKovacs]

Nat -> Level functions are possible in Agda. The most pedantic way to specify syntax and models would be:

• In the notion of model, we have Nat as levels, and we can pick i,j,k,l sizes for Con, Ty, Sub and Tm freely.
• The syntax has 0 for all i,j,k,l as a model.
• The standard model uses Nat -> Level conversion in the definition. IIRC this implies that the standard model is omega-sized for all i,j,k,l. So finite levels in an object theory necessitates transfinite levels in the metatheory (for the std model).

A less pedantic and more convenient version is to say that the notion of model has Level levels already ("shallowly embedded"). This is nicer than Nat, because there's a level solver for Level in Agda. But formally this is a bit imprecise.

I think you're correct about the choice of level bumps in the syntax in this repo; indeed it looks like the level polymorphism is set up so that the standard model is definable with the same type signature for the components. The syntax postulation was probably copied from a level-polymorphic std model definition.