Let be a Archimedean ordered integral domain with a dense linear order?, and let be the semiring? of positive terms in . A -premetric space is a type with a family of types
called the -premetric, and a family of dependent terms
representing that the -premetric for , , is a proposition.