Per Martin-Löf

It seems that I has grasp some insight of proof theory and constructive/intuitation logc.
Per Martin-Löf develop his initial type theory based on System F. but this theory is inconsitence due to Girard's paradox.
this pardox often arise in case that refer to a set that contain himself.
so to avoid such case, a typed mechnism is imposed into origin (untyped) lamda caculus. thus a set can never refer to himself.