An alternative implementation of https://doisinkidney.com/posts/2018-10-16-total-combinations.html

bins.agda

module bins where

open import Size
open import Codata.Stream
open import Codata.Thunk
open import Data.List.Base as List using (List; _∷_; [])
open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_; [_])
open import Function
open import Relation.Unary

_<<>_ : ∀ {a b i} {A : Set a} {B : Set b} →
        List⁺ (A → B) → Stream A i → Stream B i
fs <<> xs = concat (map (λ a → List⁺.map (_$ a) fs) xs)

data Bin : Set where O I : Bin

allLetters : List⁺ Bin
allLetters = O ∷ I ∷ []

cofix : ∀ (A : Size → Set) → ∀[ Thunk A ⇒ A ] → ∀[ A ]
cofix A f = f (λ where .force → cofix A f)

bins : Stream (List⁺ Bin) _
bins = [ O ] ∷ λ where
  .force → cofix (Stream (List⁺ Bin)) $ λ bins → [ I ] ∷ λ where
    .force → List⁺.map List⁺._∷⁺_ allLetters <<> bins .force

open import Agda.Builtin.Equality
import Data.Vec as Vec
open import Data.Nat
open import Data.Char
open import Data.String as String

showBin : Bin → Char
showBin O = 'O'
showBin I = 'I'

lookAt : ℕ → List String
lookAt k = List.map (String.fromList⁺ ∘′ List⁺.map showBin)
         $ Vec.toList $′ take k bins

_ : lookAt 20 ≡ "O" ∷ "I"
              ∷ "OI" ∷ "II" ∷ "OOI" ∷ "IOI" ∷ "OII" ∷ "III"
              ∷ "OOOI" ∷ "IOOI" ∷ "OIOI" ∷ "IIOI" ∷ "OOII" ∷ "IOII" ∷ "OIII" ∷ "IIII"
              ∷ "OOOOI" ∷ "IOOOI" ∷ "OIOOI" ∷ "IIOOI" ∷ []
_ = refl