# Tag Info

### When to use coinductive types?

First a note: you are using the syntax for so-called "positive" coinductive types, which makes them look like inductive types, defined by "constructors". This has various problems:...
• 3,040
Accepted

### What is the state of coinductive types and reasoning in Coq?

Intuition of the problem A good rule of thumb is to consider that in intensional type theory, coinductive types and function types share a lot of properties. In particular, equality over streams is ...
• 2,266
Accepted

### Is it possible to define fib coinductive stream w/o sized types?

I recommend the state machine definition that we'd use for looping over Fibonacci numbers: ...
• 2,067
Accepted

### Is induction over mutually inductive coinductive types possible?

It makes sense to want something like this, but Agda's termination/productivity checker does not actually validate this interpretation of the types. The reasoning behind your induction principle is ...
• 942

### Comparison between proof assistants for coinductive structures and proofs

Here's my quick and dirty overview. I don't know Lean, so anyone who does is free to edit the answer to add it, but my impression is that co-induction isn't natively supported there yet. Coq: ...
Accepted

### Defining and using bisimilarity for negatively-defined conatural numbers

You must recognize that you really have two mutually defined types here: conat and option conat. (In general, you should think ...
• 533

### How to prove that addition is commutative for conatural numbers in Coq

You just have to be a bit smarter about the definition of coadd so that it consumes both arguments. ...
• 8,969

### Why do coinductive types require bisimilarity relations?

Semantically, bisimulation just is the correct notion of equality for coinductive types. A nice intuition for it comes from parametricity. The Church encoding of a coinductive stream type \$\nu a.\,(\...
• 2,013
Accepted

### What are the differences and similarities between records, coinductive records, and codatatypes?

By reading your question, I believe that you are not looking for a very technical answer, but general ideas instead. If you would like to dig deeper, you can search with the keyword 'polarity' and '...
• 6,124

### What is a non-canonical term?

Your claim that Agda has element which Idris doesn't have is not true. Here's an Idris-equivalent I came up with: ...
• 6,124
Accepted

### Why do coinductive types require bisimilarity relations?

Coinductive types "require bisimilarity instead of =" for the same reason function types "require ...
• 533
Accepted

### How to reason about and extract code for inductive types with negative occurrences in Coq?

Building on Cody's suggestion, the following might work for you. I will consider a simpler type that still captures the essence of the problem. Define a structure which, given a type ...
• 8,969

### Comparison between proof assistants for coinductive structures and proofs

I do not know much about other proof assistants, but as for Coq I can say that there are quite some resources around that you might benefit from. Here is a starting point. However, the current ...

### Is existence of Stream as final co-algebra for the suitable functor enough to write functions into equality of streams by co-induction in ExtMLTT?

The universal property of final coalgebras can be formalized as unique-ana : ∀ (f : A → B × A) (g : A → Stream B) → unfold ∘ g ≡ map₂ g ∘ f → g ≡ ana f where <...
• 1,727
Accepted

### Is there a formalism of "coinductive" data types with negative occurrences?

I found my answer in Guarded Domain Theory and its implementation in Guarded Cubical Agda (implementing Ticked Cubical Type Theory). The following program type-checks ...

### How to prove that addition is commutative for conatural numbers in Coq

Andrej Bauer has introduced a smarter definition of coadd and has proven that it is commutative. However, I would like to show that we can prove commutativity ...
• 101

### How to prove that addition is commutative for conatural numbers in Coq

You could try to use the techniques described in Nils Anders Danielsson's Beating the Productivity Checker Using Embedded Languages. I've used them in the Agda standard library and successfully ...
• 1,126

### Stream of all finite prefixes of a stream

If you do not care about algorithmic efficiency, the simplest way to do this is to thread an accumulator in your cofixpoint: ...
• 2,266
1 vote

### Defining and using bisimilarity for negatively-defined conatural numbers

This is not really an answer, but in case you decide not to use coinductive types at all, you can have a look at how the Brown-Pradic result is formalized in Martín Escardó's ...
• 8,969
1 vote

### Co-induction principle

It it a plausible thing to do? I could just be lacking imagination, but this doesn't seem like a plausible thing to do. This seems to be a misguided attempt at understanding coinduction by duality ...
• 1,727
1 vote

### Is there a formalism of "coinductive" data types with negative occurrences?

Your datatype is a variant of the domain equation for the untyped lambda calculus. Verifying that an arbitrary untyped lambda term is normalizing is an undecidable problem, but there are undecidable ...
• 304
1 vote

### Two-step induction of inductive predicate on Streams

Do you mean the induction principle generated by the following definition ? ...
1 vote

### What is a non-canonical term?

The notion of a canonical term is an additional structure on type theory which must be specified. Informally speaking, it means something like "special nice form that we like very much". ...
• 8,969

Only top scored, non community-wiki answers of a minimum length are eligible