Properly universal type space

The notation and definitions mostly follow [HBIR]. We remind some of them to make the note self-contained. For the sake of clarity, we restrict the discussion to the case of two players only. Everything extends to more players. 1.1 Type spaces Let Ω be a compact Polish space. A type space T over Ω is a tuple (Ti, µi)i=1,2, where Ti are measurable spaces and µi: Ti → ∆ (Ω × T−i) is a measurable mapping. If Ti can be given a topology under which Ti are Polish spaces and µi are Borel measurable, then we refer to T as a Polish type space. A belief-preserving type mapping between type spaces T, T ′ over Ω is a profile φ = (φi)i=1,2 of measurable mappings φi: Ti → T ′i such that for any player i, any type ti ∈ Ti, any measurable subset S0 ⊆ Ω, S ′ ⊆ T ′−i, µ ′ (S0 × S′|φi (ti)) =