-- * Prelude

module InductionFromFold where

open import Function
open import Data.Unit
open import Data.Empty
open import Data.Sum
open import Data.Product
open import Data.Nat

open import Relation.Binary hiding (_⇒_)
open import Relation.Binary.PropositionalEquality


infixr  _⇒_
_⇒_ : {I : Set} → (I → Set) → (I → Set) → Set
A ⇒ B = {i : _} → A i → B i

-- Let's work in a sufficiently extensional type theory:

postulate 
  extensionality : {A : Set}{B : A → Set}{f g : (a : A) → B a} →
                   ((x : A) → (f x ≡ g x)) → (f ≡ g)

-- Indeed, the constructions in this paper are derived from viewing
-- least fixpoint as strong initial objects, while an intensional
-- setting only gives weak initials.

-- * W-types

-- For convenience, I'm going to work on a specific family of
-- functors: the polynomial functors, also known as
-- "containers". Their least fixpoint corresponds exactly to the
-- W-types of Martin-Lof.

-- Remark: containers are defined on any LCCC. Here, we are going to
-- work on Set, for simplicity. We could consider polynomial functors
-- between slices of Set, thus describing inductive *families*
-- (ie. indexed W-types). Or, if there is such a thing, the equivalent
-- in the homotopic framework.

-- ** Definition

-- Containers let us describe the so-called "signature functor" of our
-- datatype, ie. the set of operations and their arity.

record Cont : Set1 where
  field
    Shape : Set
    Pos : Shape → Set
open Cont

-- Its meaning is made clear through the semantics-giving extension
-- function below.

-- ** Extension of a container

-- The extension of a container computes the (strictly) positive
-- functor described by the container.

⟦_⟧ : Cont → Set → Set
⟦ φ ⟧ X = Σ[ s ∶ Shape φ ] ((p : Pos φ s) → X)

-- Hence the name polynomial functor: it's a sum indexed by Shape φ of monomials of
-- exponent P φ s.

-- Exercises: 
--   * Write the container representing Nat
--   * Write the container representing node-labelled binary trees

-- * Initial algebra semantics

-- ** External fixpoint

-- Being strictly positive, these functors admits an initial
-- algebra. Agda is very happy to notice it.

data μ (φ : Cont) : Set where
  con : (x : ⟦ φ ⟧ (μ φ)) → μ φ

-- Categorically, reading ⟦ φ ⟧ as a functor F, this is nothing but
-- that initial algebra: 
--
--     con : F (μ F) → μ F

-- Exercises:
--   * Take the fixpoint of Nat and binary trees 
--   * Check you've indeed described Nat and trees
--   * In particular, write their constructors and convince yourself
--     that they are the only constructors

-- *** Catamorphism: existence

-- Pursuing on the categorical analogy, the existence of the initial
-- algebra tells us that for any ⟦ φ ⟧-algebra (X, α : ⟦ φ ⟧ X → X),
-- there exists a (unique) morphism foldCont α from μ φ to X:

foldCont : {φ : Cont}{X : Set}
           (α : ⟦ φ ⟧ X → X) →
           μ φ → X
foldCont m (con (s , f)) = m (s , \p → foldCont m (f p))

-- Remark: in type theory, we have the existence of the morphism: we
-- build the damned thing. However, without extensionality, there is
-- no way to prove uniqueness. Our initial algebras are weak. In this
-- presentation we shall need unicity: we have therefore postulated
-- extensionality and the resulting construction is computationally
-- inert :-(

-- Exercise: 
--   * Implement addition of natural numbers using foldCont

-- *** Catamorphism: unicity

-- I'm not going to prove unicity per se (which would amount to prove
-- η for inductive elimination). Instead, I just need to prove that
-- foldCont con is equal to the identity (ie. η in the specific case
-- of the identity, in a sense).

fold∙con≡id : {φ : Cont} → (x : μ φ) → foldCont con x ≡ x
fold∙con≡id {φ} (con (sh , pos)) = cong (\p → con (sh , p)) 
                                      (extensionality (λ p → fold∙con≡id (pos p)))

-- * Induction

-- The material in this section is a mixture of Bart Jacobs' Yellow
-- Pages, Claudio Hermida's PhD thesis and, my favorite, Clément Fumex
-- PhD thesis. Clément is the one that explained these things to
-- me. Any mistake would be my original contribution.

-- I've tried to stick to the categorical terminology and notations, as
-- much as Agda would let me.

-- ** Comprehension

-- The comprehension takes a predicate P and make it a set, the
-- obvious way:

⟨_⟩ : {X : Set} → (P : X → Set) → Set
⟨_⟩ P = Σ[ x ∶ _ ] P x

-- ** Canonical lifting

-- The canonical lifting takes a functor on Set, here presented as a
-- container φ, and "lift" it as a functor on predicates,
-- ie. functions X → Set:

infix  _^_
_^_ : (φ : Cont){X : Set}(P : X → Set) → ⟦ φ ⟧ X → Set
(φ ^ P) (sh , pos) = (p : Pos φ sh) → P (pos p) 

-- Intuitively, for a predicate P, the lifting asks that all
-- sub-branches of the tree-like structure ⟦ φ ⟧ X satisfy the
-- predicate P. This is computing the good ol' induction hypothesis!

-- Exercises: 
--   * Compute the lifting for Nat and binary trees
--   * Verify that these are indeed the induction hypothesis

-- ** Induction, implemented by a fold

-- You might have seen it coming by now: we are going to obtain
-- induction by using the initial φ-algebras. To do so, from the
-- induction step α : φ^ P ⇒ P ∘ con, we define a φ-algebra:
-- 
--    ( ⟨ P ⟩, α^ : ⟦ φ ⟧ ⟨ P ⟩ → ⟨ P ⟩ )
--
-- As follow:

ind : {φ : Cont}
      (P : μ φ → Set)
      (α : φ ^ P ⇒ P ∘ con) →
      (x : μ φ) → ⟨ P ⟩
ind {φ} P α = foldCont {X = ⟨ P ⟩} α^
  where α^ : ⟦ φ ⟧ ⟨ P ⟩ → ⟨ P ⟩
        α^ (sh , pos) = (con (sh , proj₁ ∘ pos)) , α {sh , proj₁ ∘ pos} (proj₂ ∘ pos)

-- Recall that ⟨ P ⟩ is a pair of an X and a P-witness for that X: our
-- algebra thus computes the identity for the first element of that
-- pair, while unfolding the inductive step on the proof side. Doing
-- so, we *know* (because we defined it so) that the result ⟨ P ⟩ is a
-- proof of P for the x we started with.

-- Remark: I've used a slightly obscure syntax to denote the inductive
-- step α : φ ^ P ⇒ P ∘ con. Put explicitly, here is the beast:
--
--     α : {xs : ⟦ φ ⟧ (μ φ)} → φ^ P xs → P (con xs)
--
-- Intuitively, this functions is nothing but the traditional
-- inductive step: for an (here, implicit) object xs : ⟦ φ ⟧ (μ φ), we
-- are given φ^ P xs -- the induction hypothesis -- and we are asked
-- to prove P (con xs).

-- Exercise: 
--   * Unfold α on Nat and binary trees
--   * Check that these are indeed the good ol' inductive steps

-- ** Proof: the result of ind is a proof on the initial x:

-- To prove this, we proceed in two steps. First, we prove that the
-- first element of the computed pair is equal to the folding the
-- initial algebra:

proj₁∘ind≡fold∙con : {φ : Cont}
                     (P : μ φ → Set)
                     (α : φ ^ P ⇒ P ∘ con)
                     (x : μ φ) →  proj₁ (ind P α x) ≡ foldCont con x
proj₁∘ind≡fold∙con {φ} P α (con (sh , pos)) = 
      cong (\x → con (sh , x))
           (extensionality help)
  where help : (x : Pos φ sh) → 
               ((proj₁ (ind P α (pos x))) ≡ foldCont con (pos x))
        help x =  proj₁∘ind≡fold∙con P α (pos x)

-- The second step is then to prove by transitivity the desired
-- result: the first element of the pair is actually the one we start
-- with:

proj₁∘ind≡id : {φ : Cont}
               (P : μ φ → Set)
               (α : φ ^ P ⇒ P ∘ con)
               (x : μ φ) → proj₁ (ind P α x) ≡ x
proj₁∘ind≡id {φ} P α x = trans (proj₁∘ind≡fold∙con P α x) 
                               (fold∙con≡id x)

-- * Induction

-- So, what is induction? It's simply the second projection of ind!

inductionCont : {φ : Cont}
                (P : μ φ → Set)
                (α : φ ^ P ⇒ P ∘ con)
                (x : μ φ) → P x
inductionCont P α x = subst P 
                            (proj₁∘ind≡id P α x) 
                            (proj₂ (ind P α x))

-- Remark: to fix the type, we have to substitute by our
-- proofs. Sadly, our proofs are non canonical: they rely on the
-- extensionality axiom. Consequently, this definition is
-- computationally inert. That's why doing category theory in type
-- theory is rarely a good idea ;-)