Well Founded

定礎性とかいうんですけどね。超限帰納法は、不等号関係列に必ず起点があれば使えるってやつ

　　<-TransFinite : {ψ : HOD → Set n}
　　　　 → WellFounded _<_
　　　　 → ({x : HOD} → ({y : HOD} → y < x → ψ y) → ψ x ) → (x : HOD) → ψ x
　　<-TransFinite {ψ} wfa ind x = induction x (wfa x) where
　　　　 induction : (x : HOD) → Acc _<_ x → ψ x
　　　　 induction x (acc rs) = ind {x} (λ {y} y<x → induction y (rs y y<x) )

という風に使うんだが、肝心の WellFounded _<_ の作り方がわからない

　　ordWF : WellFounded _o<_
　　ordWF = ?

とか作っていくんだが。調査中

元は 1984 の論文か...


Constructing Recursion Operators in Intuitionistic Type Theory" by Lawrence C Paulson.