Switch to: References

Add citations

You must login to add citations.
  1. A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory.Peter Dybjer - 2000 - Journal of Symbolic Logic 65 (2):525-549.
    The first example of a simultaneous inductive-recursive definition in intuitionistic type theory is Martin-Löf's universe á la Tarski. A set U 0 of codes for small sets is generated inductively at the same time as a function T 0 , which maps a code to the corresponding small set, is defined by recursion on the way the elements of U 0 are generated. In this paper we argue that there is an underlying general notion of simultaneous inductive-recursive definition which is (...)
    Direct download (8 more)  
    Export citation  
    Bookmark   3 citations