The aim of this paper is to develop a formal theory of Mizar types. The examples are extracted from Mizar Mathematical Library (MML), some of them are simplified or presented in a bit different way. The presented theory is an approach to the structure of Mizar types as a sup-semilattice with widening (subtyping) relation as the order. It is an abstraction from the existing implementation of the Mizar verifier by Andrzej Trybulec and Czeslaw Bylinski. The theory describes the structure of types of the base fragment of Mizar language.