Questions tagged [coinductive-type]

Use with coinductive types.

3 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
21 votes
0 answers

Categorical semantics of Agda

I would like to know the state of the art regarding the categorical semantics of the type theory implemented by Agda — or at least some approximation of that type theory that is amenable to ...
Mike Shulman's user avatar
  • 3,040
12 votes
0 answers

Rules for mutual inductive/coinductive types

Some proof assistants, like Agda and maybe Coq, allow families of mutually defined types, or nested definitions of types, in which some are inductive and others are coinductive. I have no idea what ...
Mike Shulman's user avatar
  • 3,040
1 vote
0 answers

Can you help me lay out the different variations of CoC and their generalizations?

I am learning the typed lambda-calculus and looking into the Calculus of Constructions. It was going well until I was slapped in the face with variations, and now I'm confused about the layout of all ...
Alex Byard's user avatar