For every type and subtype , let be a function from the subtype to . Given any subtype , the inverse image by definition is a subtype of and thus a subtype of . One could restrict the domain of to and the codomain of to , and find the inverse image of under , or the 2-fold iterated inverse image of under :
One could repeat this definition indefinitely, which could be formalised by the dependent types representing the -fold iterated inverse image of under .