hedbergs_theorem.ipl

IPL's pedigree includes intuitionistic type theory: some theorems in type theory can be directly implemented in IPL. One prominent example is Hedberg's theorem.
View file at Google Code.


View file at Google Code.