What's the most pragmatic encoding for inductive-inductive types such as for a universe of types?
In pseudo Coq syntax.
Inductive U :=
| unit
| Sigma (A: U) (B: El A -> U)
with El: U -> Set:=
| tt: El unit
| pair (a: El A): El (B a) -> El (Sigma A B)
.
Your example signature is negative recursive in the second field of Sigma so it can't be encoded in total languages.
For internal universes, the usual solution is to use induction-recursion instead. In Agda:
open import Data.Product
open import Data.Unit
data U : Set
El : U → Set
data U where
unit : U
sigma : (A : U) → (El A → U) → U
El unit = ⊤
El (sigma a b) = Σ (El a) λ x → El (b x)
Induction-recursion has a reasonably concise generic scheme which can be represented in Agda.
On the other hand, inductive-inductive signatures have no known representation which is concise enough to be actually usable in Agda (for generic programming). The most concise specification is to say that signatures are type contexts in a "strictly positive" dependent type theory. Possible embeddings of this in Agda are rather difficult and tedious for practical programming purposes.
To complement András' answer, and especially if you want to stay in Coq, you can also define such an internal universe using indexed inductive types only. Basically, you replace the definitions of both U and El by a unique indexed inductive type, from which you can recover U and El after the fact.
Record Unit : Set := {}.
#[universes(polymorphic), projections(primitive)]
Record Σ {A : Type} {B : A -> Type} : Type :=
{ fst : A ; snd : B fst }.
Arguments Σ : clear implicits.
Inductive Udec : Set -> Type@{Set + 1} :=
| _unit : Udec Unit
| _sigma {ElA : Set} (A : Udec ElA) {ElB : ElA -> Set}
(B : forall a, Udec (ElB a)) : Udec (Σ ElA ElB).
Definition U@{i | Set < i } : Type@{i} := Σ@{i i} Set Udec.
Definition El (code : U) : Set := code.(fst).
Definition unit : U :=
{| fst := _ ; snd := _unit |}.
Definition sigma (A : U) (B : El A -> U) : U :=
{| fst := _; snd := _sigma A.(snd) (fun a => (B a).(snd)) |}.
Note that I have been somewhat explicit with universes, to showcase the fact that this encoding needs to bump universe levels: U cannot live at the lower level (Set) in this version, while it can in the inductive-recursive one. This is because the constructors of Udec must contain types.
