Small example of how to define least/greatest fixpoints in Agda

Fixpoints.agda

{-# OPTIONS --guardedness #-}

open import Agda.Builtin.Unit
open import Agda.Builtin.Size

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

data _⊎_ (A B : Set) : Set where
  left : A → A ⊎ B
  right : B → A ⊎ B

-- Containers (polynomial functors)
data Container : Set₁ where
  `var   : Container
  `const : Set → Container
  _`×_   : Container → Container → Container
  _`⊎_   : Container → Container → Container

-- We interpret containers as functors on Set
⟦_⟧ : Container → Set → Set
⟦ `var      ⟧ X  = X
⟦ `const A  ⟧ X  = A
⟦ c₁ `× c₂  ⟧ X  = ⟦ c₁ ⟧ X  × ⟦ c₂ ⟧ X
⟦ c₁ `⊎ c₂  ⟧ X  = ⟦ c₁ ⟧ X  ⊎ ⟦ c₂ ⟧ X

-- Least fixpoint of the functor defined by c
data μ (c : Container) : Set where
  inn : ⟦ c ⟧ (μ c) → μ c

-- Greatest fixpoint of the functor defined by c
record ν (c : Container) : Set where
  coinductive
  field
    force : ⟦ c ⟧ (ν c)
open ν

-- Example: lists/colists
module List/Colist (A : Set) where

  listC : Container
  listC = (`const ⊤) `⊎ (`const A `× `var)

  -- Lists are the least fixpoint of this functor
  List : Set
  List = μ listC

  [] : List
  [] = inn (left _)

  _∷_ : A → List → List
  x ∷ xs = inn (right (x , xs))

  -- Colists are the greatest fixpoint:
  Colist : Set
  Colist = ν listC

  -- Example: an infinite colist repeating the same element
  forever : A → Colist
  force (forever x) = right (x , forever x)