Functional Programming, Formal Methods.
scope so we could return a P n; that’s, in simple terms, essentially the reason we can’t have induction on CoC. 3. Dependent Intersections Sadly, the implementation above requires mutual recursion, as the constructor of Nat needs access to its constructors Succ / Zero, and vice-versa. That, as far