# Ld Nclusion - η-rules and codata

## ⇦ Previous · Index

Long time no see! This is a continuation of the cold introduction series. I'm sorry for the moronic title -- it's actually the co- version of "cold introduction", I've first fliiped "introduction" to "conclusion", and have taken away the "co-" prefix of "cold" and "conclusion", so it becomes "ld nclusion".

Why do I use such title? Well, because this time I wanna talk about codata and coinduction. So, basic knowledge on copatterns and productivity checking (guardedness) and Agda coinduction will be assumed. Links are pointed to the version v2.6.1 of the documentation.

Recall the previous post, we have introduced the composition operation. It's complicated, right? ;-)

Fortunately, this time we won't need these complicated operations. We won't need any SVG pictures either, because you've got enough of them (and should be able to draw them by yourself), and I've got enough with inkscape's shitty display on hi-dpi screens!

`module 2020-9-11-Cutt4 where`

`open import Cubical.Core.Everything`

`open import Cubical.Foundations.Prelude`

`variable A B : Set`

So, recall the proof of function extensionality:

`functionExt : (f g : A -> B) (p : ∀ a -> f a ≡ g a) -> f ≡ g`

`functionExt _ _ p i a = p a i`

Why does this proof type-check? Well, during type-checking, Agda first obtain the expression `λ i a -> p a i`

, which is of a path type, and checks the following equalities:

That the path's LHS is convertible to

`f`

To check it, we apply

`i0`

to the expression, and we get`λ a -> p a i0`

, and`p a : f a ≡ g a`

will reduce to`f a`

when applied by`i0`

due to the property of the path type, so it reduces to`λ a -> f a`

That the path's RHS is convertible to

`g`

To check it, we apply

`i1`

to the expression, and we get`λ a -> p a i1`

, which reduces to`λ a -> g a`

So, to some extent, we're checking the convertibility between `f`

and `λ a -> f a`

(and similarly for `g`

), and we accepted it by η-rule. To sum up, we can obtain some extensionality proof with path type simply by introducing new paths, and return something convertible to the LHS when applied `i0`

, and similarly for `i1`

. So, after introducing an interval pattern `i`

(the new path), we return a new lambda that satisfies the path constraints. Apart from that, we also need very minor η-rules.

So, what about other types, whose extensionality also don't hold definitionally in MLTT (we can't prove almost any extensionality in MLTT if they're not definitional)? Can we do them in CTT? Like, some coinductive types that doesn't have definitional η-rules? Like the `Stream`

type?

### Streams

`open import Cubical.Codata.Stream`

`open Stream -- click me to see definition of `Stream``

Since this post assumes background on coinductive types, I'd assume the understanding of the definition of `Stream`

as well. Question: can we do this (the `λ where`

is for introducing anonymous codata, and I prefer the postfix version of projection syntax because the scope checker works better with them than the prefix ones)?

`streamη : (a : Stream A) -> a ≡ λ where`

` .head -> a .head`

` .tail -> a .tail`

`streamη a i .head = a .head`

`streamη a i .tail = a .tail`

So, the simplest proof `λ a -> refl`

won't type-check because `streamη`

is equivalent to the absent definitional η-rule of coinductive types. So, like `funExt`

that introduces the lambda after the interval pattern, we also introduce the copattern matching after the interval pattern.

`_ = Stream-η -- similar definition in the library`

So, Agda checks that the term after the interval pattern:

When unfolded by

`.head`

, the both sides reduce to`a .head`

Which holds definitionally

When unfolded by

`.tail`

, the both sides reduce to`a .tail`

Ditto

And they hold, of course. We can obtain the extensionality of `Stream`

in a similar way:

`streamExt : {a b : Stream A}`

` (x : a .head ≡ b .head)`

` (y : a .tail ≡ b .tail) -> a ≡ b`

`streamExt x _ i .head = x i`

`streamExt _ y i .tail = y i`

By the similar technique, we can define a function taking the even-indexed elements and odd-indexed elements, and prove that merging these two streams gives you the same stream back:

`_ = mergeEvenOdd≡id`

We can finally have coinduction-proof-principle (CPP) in our type theory, proved as a theorem. The proof is here:

`_ = Equality≅Bisimulation.path≡bisim`

Also, by `isoToPath`

, we can prove `Stream A ≡ (Nat -> A)`

:

`_ = Stream≅Nat→.Stream≡Nat→`

An early note on the syntax and semantics of `Stream`

and cubical agda can be found in this PDF.

### Conaturals

Apart from `Stream`

s, we can also play with coinductive natural numbers, where you can define infinity:

`open import Cubical.Codata.Conat.Base`

`open Conat -- click to see the definition of `Conat``

`∞ : Conat`

`∞ .force = suc ∞`

The definition of `Conat`

is a bit weird because it's essentially a sum type, unlike most codata that are record types. When defining functions or proving theorems over `Conat`

, we need to do define a mutually-recursive pair of functions (or theorems), including a `Conat'`

version of it and a `Conat`

version.

We can prove the basic fact about infinity, where it's successor is equivalent to itself:

`∞+1≡∞ : succ ∞ ≡ ∞`

`∞+1≡∞ _ .force = suc ∞`

The type-checking of this definition is the same as of `streamη`

.

Then, with a proper definition of `+`

,

`_+_ : Conat -> Conat -> Conat`

`_+′_ : Conat′ -> Conat -> Conat′`

`(x + y) .force = x .force +′ y`

`zero +′ y = y .force`

`suc x +′ y = suc (x + y)`

We can prove that for any conatural number `n`

, adding it to infinity gives you infinity as well:

`n+∞≡∞ : ∀ n -> n + ∞ ≡ ∞`

`n+′∞≡∞′ : ∀ n -> n +′ ∞ ≡ suc ∞`

`n+∞≡∞ n i .force = n+′∞≡∞′ (n .force) i`

`n+′∞≡∞′ zero = refl`

`n+′∞≡∞′ (suc n) i = suc (n+∞≡∞ n i)`

This, includes infinity itself:

`∞+∞≡∞′ : ∞ + ∞ ≡ ∞`

`∞+∞≡∞′ = n+∞≡∞ ∞`

We can also prove `∞ + ∞ ≡ ∞`

by a copattern matching directly:

`∞+∞≡∞ : ∞ + ∞ ≡ ∞`

`∞+∞≡∞ i .force = suc (∞+∞≡∞ i)`

More interesting properties can be found on github, where the bisimilarity is defined, CPP is proved, and the homotopy-level of `Conat`

was proved.

##### License

*This and the **original version** of this blog are licensed under a **Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License**.*