I'm wondering, is there a way to make a Universe à la Tarski that models all of the types in an open type theory, where there can be user defined parameterized inductive types?
For context, I'm trying to write a syntactic model of a type theory I've got with a kind of type-case, essentially like Section 5.2 of this paper. I'm mechanizing the model in Agda, but I'm trying to abstract over the defined inductive types, so that I know my mechanization works for any set of inductive types.
The idea is that types in the source language are modeled in the target as an inductive-recursive type $Code\ \ell$, defined with an "elements-of" interpretation $El : Code \to Set$. To capture "all" the datatypes, there's a mutually-defined type $Desc$ of descriptions of inductive types, like in Diehls and Sheard or McBride:
data Desc ℓ : Set where
End : Desc ℓ
Arg : (c : Code ℓ) -> (El c -> Desc ℓ) -> Desc ℓ
Rec : Desc ℓ -> Desc ℓ
What's different than usual here is that
Arg takes a code describing a type, not a type itself, which lets us model type-case stuff.
I'm wondering, is there a way to extend this to allow for parameterized inductive types?
The usual trick with $Desc$ is to define a parameterized type as a function $(x : Params) \to Desc$. e.g. the description for $List$ is a function $DList : Set \to Desc$. But this doesn't work when
Arg takes a $Code$ instead of a type, since (as far as I can see) this requires a bunch of mutual references between $Code$ and $Desc$ that break strict positivity.
Is this similar to anything that's been done? Is there a known solution to this, or is this pushing beyond what can be modeled with a single Tarski universe?