File everything.ced imports all code for the development

Found in nu/nu.ced. The generic coinductive datatype is Nu, with generator unfoldM, constructor inM, and destructor outM.

The proofs found in nu/lambek.ced point to a current gap in Cedille’s theory: one direction of Lambek’s lemma (and the codatatype reflection law) does not hold for Cedille’s currently intensional equality type, suggesting the need for an extensional equality type.

• examples/streamf.ced give the definition of the stream type as well as its destructors and generator
• examples/stream.ced show some examples of programming with streams using coiteration, corecursion, and course-of-values coiteration.

• examples/streamrelf.ced defines the type family StreamRel of generalized relations between streams
• examples/streamrelf.ced shows proofs that if the relation on elements of streams satisfies certain properties, those properties hold also for StreamRel