InitialAlgebra.agda

{-# OPTIONS --without-K --safe #-}
module InitialAlgebra where

open import Level hiding (zero) renaming (suc to ℓ-suc)

open import Relation.Binary.PropositionalEquality.Core

open import Data.Nat.Base using (ℕ; zero; suc; _+_)
open import Data.List.Base using (List; []; _∷_)

open import Categories.Category
open import Categories.Functor
open import Categories.Functor.Algebra
open import Categories.Category.Construction.F-Algebras

open import Categories.Object.Initial

open import Categories.Category.Instance.Sets

-- First, let us fix a category 𝒞.
module Inductives {o ℓ e} (𝒞 : Category o ℓ e) where
  open Category 𝒞

  -- We can give semantics to an inductive type as initial
  -- algebras for some endofunctor.
  record Inductive : Set (o ⊔ ℓ ⊔ e) where
    field
      F : Endofunctor 𝒞
      τ : F-Algebra F
      initial : IsInitial (F-Algebras F) τ

    open Functor F public
    -- Let's rename some things to be a little more descriptive.
    -- We use 'roll' here to indicate that the 
    -- F-Algebra τ witnesses the fact that we can "roll up" a layer
    -- of recursion.
    open F-Algebra τ renaming (A to Carrier; α to roll) public
    -- Furthermore, we use 'fold' here to emphasize that the map between
    -- F-Algebra carriers witnessed by 'initial' is indeed the fold we are looking for!
    -- We have to do some silly things with modules here because of some annoying implicits.
    open IsInitial initial public
    module Fold α = F-Algebra-Morphism (IsInitial.! initial {α}) renaming (f to fold; commutes to fold-commutes)
    open Fold public

  open Inductive public

  -- Now, for the heart of the matter! We are looking for a universal property
  -- that says that some map out of an inductive "is a fold". Really, something
  -- "is a fold" if it's an F-Algebra morphism out of the inductive type into
  -- /some/ other F-Algebra.
  -- By the uniqueness of the initial map, this means that our map 'f' is equal
  -- to 'fold'.
  record IsFold (T : Inductive) {A : Obj} (f : T .Carrier ⇒ A) : Set (ℓ ⊔ e) where
    field
      -- This morphism, combined with 'A', forms an F-Algebra.
      alg      : T .F₀ A ⇒ A
      -- This condition is just restating the commuting condition from 'F-Algebra-Morphism'.
      commutes : f ∘ T .roll ≈ alg ∘ T .F₁ f

    -- The F-Algebra in question.
    Alg : F-Algebra (T .F)
    Alg = record { A = A ; α = alg }

    -- Bundle up the commuting condition along with the morphism on carriers to form an
    -- F-Algebra morphism.
    mor : F-Algebra-Morphism (T .τ) Alg
    mor =  record { f = f ; commutes = commutes }
    
    -- Show that 'f' is indeed equal to a fold for some algebra.
    is-fold : T .fold Alg ≈ f
    is-fold = T .!-unique mor

-- As an example, let's consider a concrete example: Lists.
private module Example where
  -- Let's work over the Category of Sets.
  open Category (Sets 0ℓ)
  open Inductives (Sets 0ℓ)

  -- First, let's define smash products.
  data Smash (A B : Set) : Set where
    nada : Smash A B
    smash : A → B → Smash A B

  -- Next, let's witness the fact that 'Smash' is functorial
  -- in it's second argument.
  smash-map : ∀ {A B C} → (B → C) → Smash A B → Smash A C
  smash-map f nada        = nada
  smash-map f (smash a b) = smash a (f b)

  SMASH : Set → Endofunctor (Sets 0ℓ)
  Functor.F₀ (SMASH A) = Smash A
  Functor.F₁ (SMASH A) = smash-map
  Functor.identity (SMASH A) {x = nada} = refl
  Functor.identity (SMASH A) {x = smash _ _} = refl
  Functor.homomorphism (SMASH A) {x = nada} = refl
  Functor.homomorphism (SMASH A) {x = smash _ _} = refl
  Functor.F-resp-≈ (SMASH A) eq {x = nada} = refl
  Functor.F-resp-≈ (SMASH A) eq {x = smash a _} = cong (smash a) eq

  -- We can construct a Smash-Algebra whose carrier is List.
  ListAlg : (A : Set) → F-Algebra (SMASH A)
  F-Algebra.A (ListAlg A) = List A
  F-Algebra.α (ListAlg A) nada = []
  F-Algebra.α (ListAlg A) (smash x xs) = x ∷ xs

  open F-Algebra renaming (A to Carrier; α to ⟦_⟧)
  open F-Algebra-Morphism renaming (f to mor)

  -- Furthermore, given a Smash-Algebra, we can construct a map out of List
  -- into it's carrier
  list-fold : ∀ {A} → (α : F-Algebra (SMASH A)) → List A → α .Carrier
  list-fold α [] = ⟦ α ⟧ nada
  list-fold α (x ∷ xs) = ⟦ α ⟧ (smash x (list-fold α xs))

  -- Furthermore, list-fold commutes with it's associated algebra.
  list-fold-commutes : ∀ {A} → (α : F-Algebra (SMASH A)) → list-fold α ∘ ⟦ ListAlg A ⟧ ≈ ⟦ α ⟧ ∘ smash-map (list-fold α)
  list-fold-commutes α {nada} = refl
  list-fold-commutes α {smash x xs} = refl

  -- This means that list-fold is an F-Algebra Morphism.
  list-fold-mor : ∀ {A} → (α : F-Algebra (SMASH A)) → F-Algebra-Morphism (ListAlg A) α
  mor (list-fold-mor α) = list-fold α
  commutes (list-fold-mor α) = list-fold-commutes α

  -- To make matters more interesting, 'list-fold-mor' witnesses initiality of 'ListAlg'.
  list-fold-unique : ∀ {A} {α : F-Algebra (SMASH A)} → (f : F-Algebra-Morphism (ListAlg A) α) → F-Algebras (SMASH A) [ list-fold-mor α ≈ f ]
  list-fold-unique f {[]} = sym (f .commutes {x = nada})
  list-fold-unique f {x ∷ xs} rewrite list-fold-unique f {xs} = sym (f .commutes {x = smash x xs})

  ListAlgInitial : ∀ A → IsInitial (F-Algebras (SMASH A)) (ListAlg A)
  IsInitial.! (ListAlgInitial A) {α} = list-fold-mor α
  IsInitial.!-unique (ListAlgInitial A) = list-fold-unique

  -- All of this means that 'List' is an inductive type.
  LIST : Set → Inductive
  Inductives.Inductive.F (LIST A) = SMASH A
  Inductives.Inductive.τ (LIST A) = ListAlg A
  Inductives.Inductive.initial (LIST A) = ListAlgInitial A

  -- With all of that categorical boilerplate out of the way, let's show that
  -- 'length is a fold.
  length : ∀ {A : Set} → List A → ℕ
  length [] = 0
  length (_ ∷ xs) = suc (length xs)

  -- First, we define the associated F-Algebra.
  length-alg : ∀ {A} → Smash A ℕ → ℕ
  length-alg nada = 0
  length-alg (smash _ n) = suc n

  -- Next, we prove the commuting condition.
  length-commutes : ∀ {A} → length ∘ (LIST A) .roll ≈ (length-alg ∘ smash-map length)
  length-commutes {x = nada} = refl
  length-commutes {x = smash _ _} = refl

  -- Then that's it!
  length-is-fold : ∀ {A} → IsFold (LIST A) length
  Inductives.IsFold.alg length-is-fold = length-alg
  Inductives.IsFold.commutes length-is-fold = length-commutes