Posted by Jesper on January 22, 2026

This week I am staying at the welcoming University of Twente for the Dutch Winter School on Logic and Verification to teach a course on Agda. Since the overall theme of the school is cyclic structures and coinduction, I wanted to show off Agda’s capabilities in that area. However, it turns out that there is not a lot of introductory material on coinduction in Agda, and the Agda user manual on coinduction is also quite bare-bones (something that was already pointed out to me by the group of TU Delft bachelor students who did a project on coinduction in Agda last year). This is a big shame, since Agda’s approach to coinduction is quite unique and in my opinion much better than what other proof assistants have on offer (though I hear Isabelle’s support is quite good as well). So I want to rectify this situation by sharing an introductory tutorial series on coinduction in Agda here on my blog.

Perhaps some of you reading this are now thinking “coin-what?” Coinduction might sound like a scary thing involving lots of symbols and proofs (and it often is), but it is not my intention to go deep into the theoretical basis of coinduction, Rather I want to show how to use it in Agda with some practical examples. From this practical perspective, coinduction is just a principled way to program with infinite or cyclic structures such as streams and graphs in a total language like Agda. It’s not that Agda doesn’t allow you to define infinite lists, you just have to be honest about their inclusion when defining the type. And coinduction is precisely the way you can express that honesty.

I have three lectures at the winter school, so I’ll also divide this tutorial into three blog posts:

1. Coinductive programming (this post)
2. Coinductive proving
3. Case studies and applications

I assume you already know the basics of how to use Agda, which you can learn for example from my lecture notes on Programming and Proving in Agda. If you have any questions, corrections, or additions to this tutorial, please let me know via Zulip, the Fediverse, or good ol’ email.

Record types and copattern matching

Before I explain coinduction in Agda proper, we first need to understand the foundations that it is built upon, which are record types and copattern matching. First off, record types in Agda are just like we’d expect from other languages: a type bundling a of a number of fields into a single type. Apart from its fields, a record type can also optionally be given a constructor.

For example, we define a type of rectangles with fields for the height and the width:

record Rect : Set where
constructor rect -- optional
field
height : ℕ
width  : ℕ

To construct a value of a record type, we either use the record { ... } syntax with named fields or use the constructor directly (if we declared one):

square : ℕ → Rect
square x = record { height = x ; width = x }

square' : ℕ → Rect
square' x = rect x x

We can access the fields of a record value by using the projections Rect.height and Rect.width:

area : Rect → ℕ
area r = Rect.height r + Rect.width r

To avoid having to write the name of the record type in front of each projection, we open the record to bring projections into scope:

open Rect

perimeter : Rect → ℕ
perimeter r = 2 * height r + 2 * width r

We can also use projections in postfix notation by starting their name with a .:

rotate : Rect → Rect
rotate r = rect (r .width) (r .height)

Postfix notation is especially useful when working with nested record types since we can stack them without any parentheses. Postfix notation is also required when using the projection as a copattern in a pattern lambda (see below).

One way to think about record types is as a single-constructor data type with some syntactic sugar for the projections. However, there is a deeper and more fruitful way of looking at record types as being dual to data types. Where data types are defined by all the different ways of constructing an element, record types are defined by all the possible observations we can make of an element. To define a function that has a data type as an input, we should define it for each of the constructors of the data type (this is pattern matching). Dually, to define a function that has a record type as its output, we should define it for each of the projections of the record type. This is called copattern matching.

Concretely, to define a function by copattern matching we just define what should be the value of each of the projections applied to it. For example, below we define squash r by the values of its projections height (squash r) and width (squash r):

squash : Rect → Rect
height (squash r) = half (height r)
width  (squash r) = 2 * width r

Copattern matching can also be used together with postfix projections:

squeeze : Rect → Rect
squeeze r  .height  = 2 * (r .height)
squeeze r  .width   = half (r .width)

Finally, copattern matching can also be used in a pattern-matching lambda:

expand : Rect → Rect
expand r = λ where
.height → 2 * r .height
.width  → 2 * r .width

Since the lambda function itself is anonymous, there is nothing that the projection can be syntactically applied to, so the use of postfix notation in pattern lambdas is mandatory.

If the copattern notation does not yet make sense 100%, don’t worry. There’ll be many more examples once we define some coinductive record types.

Coinductive record types

The simplest example of a coinductive type is the type of streams, i.e. infinite lists of values of a given type. Concretely, in Agda we define streams as a record type that consists of a head element of type A and a tail which is another stream. Since the type Stream occurs recursively in its own definition, we have to indicate to Agda whether we want the type to only include finite values (inductive) or also infinite values (coinductive). In this case, we want to include infinite streams, since otherwise we would end up with an empty type.

module GuardedCoinduction where

record Stream (A : Set) : Set where
coinductive
field
head  : A
tail  : Stream A
open Stream

We use the projections to define functions on streams:

firstTwo : Stream A → A × A
firstTwo s = s .head , s .tail .head

take : ℕ → Stream A → List A
take zero    s = []
take (suc n) s = s .head ∷ take n (s .tail)

drop : ℕ → Stream A → Stream A
drop zero     s  = s
drop (suc n)  s  = drop n (s .tail)

If we have an existing stream we can use it to build new streams using the record syntax:

_∷S_ : A → Stream A → Stream A
x ∷S xs = record { head = x ; tail = xs }

_++_ : List A → Stream A → Stream A
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷S (xs ++ ys)

However, if we try to define a new stream with a record constructor, Agda’s termination check fails:

module BadZeroes where
{-# NON_TERMINATING #-}
zeroes : Stream ℕ
zeroes = record { head = 0 ; tail = zeroes }

There is actually a good reason why Agda rejects this definition: with it, normalizing the expression zeroes will go into an infinite loop. Since Agda needs to reduce terms during type checking, this would mean that Agda’s type checker could loop forever as well, which we’d like to avoid.

To define a new stream, we have to use copatterns instead:

zeroes : Stream ℕ
zeroes .head = 0
zeroes .tail = zeroes

The expression zeroes only reduces when projections are applied to it, thus there is no infinite loops created by this definition. The key point is that to compute each consecutive value in the stream zeroes, we need an additional application of tail. Hence Agda will only compute the stream for as far as we have asked for.

We generalize the definition of zeroes to repeat a given value:

repeat : A → Stream A
repeat x .head = x
repeat x .tail = repeat x

Exercise. Define the lookup function on streams and prove that looking up any value in repeat x returns x:

lookup : Stream A → ℕ → A
lookup-repeat : (x : A) (n : ℕ) → lookup (repeat x) n ≡ x

Solution.

lookup xs zero    = xs .head
lookup xs (suc n) = lookup (xs .tail) n

lookup-repeat x zero    = refl
lookup-repeat x (suc n) = lookup-repeat x n

Just using copatterns is not sufficient to define a sensible stream, however. For example, computing the second element of the stream ones defined below loops forever:

module BadOnes where
{-# NON_TERMINATING #-}
ones : Stream ℕ
ones .head = 1
ones .tail = ones .tail

To avoid bad definitions such as this one, Agda requires that coinductive values should be productive: applying any (finite) number of projections to them should terminate. This is enforced by the guardedness criterion: every (co)recursive call needs to appear

• in a clause with a copattern, and
• either at the top level or as the argument to one or more constructors.

(Side note: the Agda user manual does not have a proper specification of the guardedness criterion, so I am not sure if this description is 100% correct. Let me know if you have a better description.)

To use the guardedness criterion for productivity, we need to enable it explicitly by using the --guardedness flag (e.g. by putting {-# OPTIONS --guardedness #-} at the top of the file). The reason we have to enable it explicitly is because Agda also provides an alternative way to check productivity, namely sized types, that we’ll discuss below.

As another example, we define a map function on streams:

map : (A → B) → Stream A → Stream B
map f xs .head  = f (xs .head)
map f xs .tail  = map f (xs .tail)

A counterexample to the guardedness criterion is the following definition of the stream of natural numbers:

module FailingNats where
{-# TERMINATING #-}
nats : Stream ℕ
nats .head = 0
nats .tail = map suc nats

The recursive call to nats appears in an argument to the function map which is not a constructor, so it fails the guardedness check. The problem with this definition is that the guardedness checker does not look at the definition of map so for all it knows it might not produce a value “in time” for the nats definition to be productive. For example, if we used the following definition of map, then nats would cease to be productive.

map' : (A → B) → Stream A → Stream B
map' f xs .head = f (xs .tail .head)
map' f xs .tail = map f (xs .tail .tail)

We can assist the productivity checker by first defining the more general natsFrom stream:

natsFrom : ℕ → Stream ℕ
natsFrom n .head = n
natsFrom n .tail = natsFrom (suc n)

nats : Stream ℕ
nats = natsFrom 0

Alternatively, we can use sized types to provide Agda with more information about map (see later in this post).

Exercise. Prove that the lookup function commutes with map:

lookup-map : (i : ℕ) → lookup (map f s) i ≡ f (lookup s i)

Solution.

lookup-map zero    = refl
lookup-map (suc i) = lookup-map i

Exercise. When defining the stream of Fibonacci numbers, we run into a similar problem as with defining nats:

zipWith : (f : A → B → C)
→ Stream A → Stream B → Stream C
zipWith f xs ys .head = f (xs .head) (ys .head)
zipWith f xs ys .tail = zipWith f (xs .tail) (ys .tail)

module FailingFibonacci where
{-# TERMINATING #-}
fibonacci : Stream ℕ
fibonacci .head = 0
fibonacci .tail .head = 1
fibonacci .tail .tail =
zipWith _+_ fibonacci (fibonacci .tail)

A more general way to work around the limitations of syntactic guardedness is to use the tabulate function, which is the inverse to lookup. Implement tabulate and use it to define fibonacci.

tabulate : (ℕ → A) → Stream A
fibonacci : Stream ℕ

Solution.

tabulate f .head = f 0
tabulate f .tail = tabulate (f ∘ suc)

fibonacci = tabulate fib
where
fib : ℕ → ℕ
fib zero = 1
fib (suc zero) = 1
fib (suc (suc x)) = fib x + fib (suc x)

Exercise. A stream can contain elements of any type, including the type of streams itself. We can think of a stream of streams as a two-dimensional matrix that is infinite in both directions. It is a fun exercise to implement a transpose function for infinite matrices and prove its defining property. You probably need the lookup-map property you used before. It might also be useful to use the equational reasoning syntax from the module ≡-Reasoning which is defined in Relation.Binary.PropositionalEquality.Properties in the standard library.

transpose : Stream (Stream A) → Stream (Stream A)
transpose-flips-lookup
: (xss : Stream (Stream A)) (i j : ℕ)
→ lookup (lookup (transpose xss) i) j
≡ lookup (lookup xss j) i

Solution.

transpose xss .head = map head xss
transpose xss .tail = transpose (map tail xss)

transpose-flips-lookup xss zero j = lookup-map j
transpose-flips-lookup xss (suc i) j =
begin
lookup (lookup (transpose xss) (suc i)) j
≡⟨⟩
lookup (lookup (transpose xss .tail) i) j
≡⟨ transpose-flips-lookup (map tail xss) i j ⟩
lookup (lookup (map (λ r → tail r) xss) j) i
≡⟨ cong (λ yss → lookup yss i) (lookup-map j) ⟩
lookup (tail (lookup xss j)) i
≡⟨⟩
lookup (lookup xss j) (suc i)
∎
where open ≡-Reasoning

Mixing induction and coinduction

Streams are a nice first example of a coinductive type, but they are also a bit boring because they all have exactly the same structure, the only difference is in the values. To define more interesting types with potentially infinite values, we can mix induction and coinduction by mutually defining a data type and a coinductive record type. For example, we define a type of potentially infinite lists or colists:

mutual
data Colist (A : Set) : Set where
[]   : Colist A
_∷_  : A → Colist' A → Colist A

record Colist' (A : Set) : Set where
coinductive
field
force : Colist A
open Colist' public

This pattern of defining a datatype together with a coinductive record with a single field called force is quite common when defining coinductive types in Agda.

We convert a list to a (finite) colist:

fromList : List A → Colist A
fromList []       = []
fromList (x ∷ xs) = x ∷ record { force = fromList xs }

Despite the fact that fromList produces a colist, the reason why it passes the Agda termination checker is because it is structurally recursive on the input list. In other words, this function is defined by induction, not coinduction.

In contrast, converting a stream to an (infinite) colist needs to use a copattern to make it pass the guardedness check:

fromStream : Stream A → Colist A
fromStream {A} xs = xs .head ∷ rest
where
rest : Colist' A
rest .force = fromStream (xs .tail)

To make the definition a bit less verbose, we inline the definition of rest by using a (co)pattern lambda:

fromStream' : Stream A → Colist A
fromStream' {A} xs = xs .head ∷
(λ where .force → fromStream' (xs .tail))

Unfortunately, the syntactic noise of λ where .force → is not avoidable because the guardedness criterion requires a copattern to appear syntactically in the definition.

Another example of a mixed induction/coinduction is the type of co-natural numbers, which is the type of regular Peano numbers plus infinity ∞:

mutual
data Coℕ : Set where
zero  : Coℕ
suc   : Coℕ' → Coℕ

record Coℕ' : Set where
coinductive
field force : Coℕ
open Coℕ' public

∞ : Coℕ
∞ = suc λ where .force → ∞

Exercise. Define the following functions:

fromℕ : ℕ → Coℕ
colength : Colist A → Coℕ

Solution.

fromℕ zero = zero
fromℕ (suc n) = suc λ where .force → fromℕ n

colength [] = zero
colength (x ∷ xs) = suc λ where
.force → colength (xs .force)

A more substantial example of mixing induction and coinduction is the type of streams of bits Zero and One that have infinitely many zeroes:

data ZeroOne : Set
record ZeroOne' : Set

data ZeroOne where
Zero_ : ZeroOne' → ZeroOne
One_  : ZeroOne  → ZeroOne

record ZeroOne' where
coinductive
field force : ZeroOne
open ZeroOne' public

Since the recursive argument of the One constructor has type ZeroOne rather than ZeroOne', the constructor is considered to be inductive and hence it can only be applied a finite number of times before we get another Zero constructor.

Coinduction with sized types

The guardedness criterion has the advantage of being fairly simple and easy to check, but we have also seen that it can be annoying and rule out natural definitions of coinductive values. Sized types are an alternative to the syntactic guardedness checker that annotates the size of expressions in their types. They are enabled by putting {-# OPTIONS --sized-types #-} at the top of our file (using --guardedness and --sized-types together is inconsistent, see issue #1209 on the Agda bug tracker).

To use sized types, we should import the builtin module Size (or Agda.Builtin.Size if you are not using the standard library):

module SizedCoinduction where
open import Size using (Size; Size<_; ∞)
variable i : Size

The module Size provides:

• The type Size : Set
• The family of types Size< i : Set for every i : Size
• The size ∞ : Size
• Some more operations on sizes that are not relevant here.

We can think of sizes as natural numbers extended with ∞, but pattern matching on sizes is not allowed. The type Size< i is similar to the Fin n type of natural numbers less than n. A special property of these types is that we have subtyping Size< i <: Size and Size< i <: Size< j when i ≤ j.

To make use of sizes, we should parametrize our coinductive types by a size representing the number of observations we can safely make, i.e. the “depth” until where the coinductive value has been defined. For example, we parametrize a stream by its size:

record Stream (A : Set) (i : Size) : Set where
coinductive
field
head : A
tail : {j : Size< i} → Stream A j
open Stream

When taking the tail of a stream of size i, we should pick any size j that is strictly smaller than i and we get a stream of that size.

When writing a function that takes a stream as input we usually assume that the stream is already fully defined, which means we use size ∞:

take : ℕ → Stream A ∞ → List A
take zero    s = []
take (suc n) s = s .head ∷ take n (s .tail)

drop : ℕ → Stream A ∞ → Stream A ∞
drop zero    s = s
drop (suc n) s = drop n (s .tail)

On the other hand, when defining a new stream we should define it at an arbitrary size i:

zeroes : Stream ℕ i
zeroes .head  = 0
zeroes .tail  = zeroes

We can understand this definition better by making all the implicit sizes explicit:

zeroes' : {i : Size} → Stream ℕ i
zeroes' {i} .head      = 0
zeroes' {i} .tail {j}  = zeroes {j}

In the definition of zeroes' {i} .tail, we have to give a function of type {j : Size< i} → Stream ℕ j. Since j < i, the recursive call zeroes {j} is made at a size strictly smaller than i, which is why it is accepted by Agda’s productivity checker for sized types.

Using sizes, we now give a more precise type to map that makes it clear that it preserves the depth for which the stream is defined:

map : (A → B) → Stream A i → Stream B i
map f s .head = f (s .head)
map f s .tail = map f (s .tail)

This allows us to give a direct definition of nats using map, showing that sized types allow more definitions than the guardedness criterion:

nats : Stream ℕ i
nats .head  = 0
nats .tail  = map suc nats

Exercise. Define zipWith for sized streams with the proper size annotations and use it to define fibonacci without using tabulate.

fibonacci : Stream ℕ i

Solution.

zipWith : (A → B → C)
→ Stream A i → Stream B i → Stream C i
zipWith f xs ys .head = f (xs .head) (ys .head)
zipWith f xs ys .tail = zipWith f (xs .tail) (ys .tail)

fibonacci .head = 1
fibonacci .tail .head = 1
fibonacci .tail .tail =
zipWith _+_ fibonacci (fibonacci .tail)

This was just a basic introduction to sized types, we will see more examples using them in parts 2 and 3 of this series.

Unfortunately, despite their appeal there is a whole list of issues with sized types, or at least with their current implementation in Agda.

Long list of currently open issues with sized types in Agda

First, as we have seen it takes additional work to annotate types and functions with sizes, and the resulting definitions are not compatible with Agda code that does not uses sized types because of the additional arguments.

Second, Agda has a heuristic for assigning default values to implicit sizes if there are no constraints on them, but the current implementation of this heuristic is too eager, forcing us to give explicit values to sizes that should be inferrable (see issues #992, #2439, #2551, and #2930).

Third, the fact that sized types make use of subtyping (which is not used in other parts of Agda aside from the rarely-used --cumulativity flag) also causes a number of spurious errors (see issues #1579, #2409, #2440, and #3039.

Third, there are several other cases where the termination/productivity checker for sized types is more restrictive than it should be, though there is not a clear pattern as far as I can tell (see issues #300, #1515, #1869, #1894, #2041, #2098, #2331, #2651, and #2903).

Fourth, there are some examples that make Agda’s type checker loop in the presence of sized types (see issues #1417, #1428, #1523, #3144, and #4376).

Finally and most worryingly, there are several known inconsistencies in the current implementation of sized types, most (but not all) follow from the fact that Agda considers ∞ to be strictly smaller than itself (see issues #1201, #1946, #2820, #3026, #6002, and #7178). It has been prophesized that one day we will get a new implementation of sized types that avoids these issues (or at least the most severe ones). Great honor will be bestowed on the one implementing this. We also pay our respect to the heroes who have fallen on their quest for this holy grail.

While it is unlikely that you run into these issues when using sized types in the “indended” way, this state of affairs is not ideal and has naturally hindered the adoption of sized types.

In the mean time, Isaac Elliott has a great blog post on Sized types and coinduction in Safe Agda where he shows a way to “fake” sized types without using the --sized-types flag. While you lose some convenience such as subtyping and heuristics for inferring sizes, it could be a good alternative if you want to use a kind of sized types in the --safe fragment of Agda.

That’s all for this post! Thank you for reading it, and look forward to the second part of this series where I’ll write about how to state and prove properties of coinductive structures.