(using a non-Coq notation and using a newer form of coinductive types)

Inductive types are built using constructors. An example, defining two lists:

l1 = nil

l2 = cons 1 l1

Induction/recursion principles (fixpoints + pattern matching) consume them to produce some other value.

Examples:

length nil = 0

length (cons x xs) = 1 + length xs

For coinductive types it's the inverse. Coinduction/corecursion principles (cofixpoints + copattern matching) produce them. Take streams with the destructors hd : Stream A -> A and tail : Stream A -> Stream A). By defining how it's destructors work on the stream, we define a stream blink : (Bool -> Stream Nat):

hd (blink True) = 0

hd (blink False) = 1

tail (blink True) = blink False

tail (blink False) = blink True

blink True is the infinite stream 0101010101010101... To consume the stream, you call the destructors on it (and receive the defined result).

Now, just like how records are inductive types defined via destructors, the same can be done allowing coinductive types to be defined via constructors. In Coq this is called positive coinductive types and they're the original form of coinductive types introduced to Coq (and the only one until ~2019), but they're also not exactly well behaved, which is why it's now recommended to use the negative form, though e.g. this paper still uses the positive form. If you want to know more about this, I'd recommend reading the Coq documentation :-)

>Also curious how they interact with the termination checker

While infinite, negative coinductive types don't pose any termination issue because they're lazy - blink only 'describes how to deconstruct it' and does not do any computation of its own. So if you apply a finite amount of destructors to it, you only get a finite computation.

(positive coinductive types are a bit more tricky - there's a special productivity condition for them.)