5

Uniqueness is not converse to introduction. Uniqueness rules in type theory are components of isomorphisms. If a type former is specified with an isomorphism, then Constructors form one map Eliminators form the inverse map β-rules express elim ∘ con = id η-rules (uniqueness) express con ∘ elim = id For example, function types are given as Tm Γ (Π A B) ≃ Tm ...


3

We certainly do not need very many $W$-types. If we also have universes, we only need one $W$-type, namely the natural numbers. For example, the UniMath library uses just the natural numbers and no other inductive types (if we discount the fact that standard types constructors, such as products and sum, are defined inductively in Coq).


2

You asked several questions. You asked about a type indexed by a list, so you can do this. data DataType (A : Type) (F : A -> Type) : List A -> Type where empty : DataType A F [] _bla_ : forall {xs} {x} -> DataType A F xs -> F x -> DataType A F (x ∷ xs) Where F is a type family that is indexed by the elements of the list. Apart from that, ...


2

Generally, there will be one context-free grammar for both types and terms, and judgements will be used to identify those expressions which are types and which expressions are terms of a particular type. This has been written down many, many times. For a pretty typical example, you could look at Abel, Coquand and Dybjer's LICS 2007 paper, Normalization by ...


Only top voted, non community-wiki answers of a minimum length are eligible