Re: [HoTT] A small observation on cumulativity and the failure of initiality

[Thomas Streicher <stre...@mathematik.tu-darmstadt.de>]

>  A quite detailed interpretation of type theory in set theory is presented
> 
> in the paper of Peter Aczel "On Relating Type Theories and Set Theories".
> 
> On can define directly the interpretation of lambda terms (provided that abstraction is
> 
> typed), and using set theoretic coding, one can use a global application operation
> 
> (so that the interpretation is total). One can then checked by induction on derivations
> 
> that all judgements are valid for this interpretation.

Thanks, Thierry, for pointing this out. But Peter's method does not
extend to arbitrary split models of dependent type theory. What Peter
uses here intrinsically is that everything is a set since otherwise he
couldn't interpret type theoretic quantification.
My interpretation got partial on pseudoexpressions since pseudoterms
can't be understood as pseudo-type-expressions.

I don't see how Peter's method extends to interpretation of
realizability or (pre)sheaf models of dependent type theories not to
speak of arbitrary contextual cats or other split categorical models
of dependent type theories.

Thomas