{-

<www.cl.cam.ac.uk/users/amp12/agda/initial-T-algebras/code.zip>

Construction of the initial algebra for a strictly positive
endofunctor on Set using uniqueness of identity proofs, function
extensionality, quotients types and sized types.

Andrew Pitts 2019-11-07
-}

module InitialTAlgebra where

-- some standard definitions
open import Prelude

-- quotient types and function extensionality via private declaration
-- and PrimTrustMe
open import QuotientViaPrimTrustme+Private

{-
Quotient types and function extensionality via postulates + REWRITE
and POLARITY pragmas

open import QuotientViaPostulate+Rewrite+Polarity

is insufficient for the defintion of Success.M to be accepted by Agda
-}

----------------------------------------------------------------------
-- Strictly positive endofunctor
----------------------------------------------------------------------
postulate
  T : Set → Set
  T' : {X Y : Set} → (X → Y) → T X → T Y
  Tid :
    {X : Set}
    (x : T X)
    → ---------
    x ≡ T' id x
  T∘ :
    {X Y Z : Set}
    (g : Y → Z)
    (f : X → Y)
    (x : T X)
    → --------------------------
    T' g (T' f x) ≡ T' (g ∘ f) x

{-# POLARITY T ++ #-} -- this tells Agda that T is strictly positive

----------------------------------------------------------------------
-- T-Algebra structure
----------------------------------------------------------------------
record isTAlg (A : Set) : Set₁ where
  constructor mkalg
  field
    sup : T A → A

open isTAlg ⦃ ... ⦄ public

----------------------------------------------------------------------
-- The property of being an T-algebra morphism
----------------------------------------------------------------------
isTAlgMor :
  {A B : Set}
  {{α : isTAlg A}}
  {{β : isTAlg B}}
  (h : A → B)
  → --------------
  Set
isTAlgMor h = ∀ e → h (sup e) ≡ sup (T' h e)

----------------------------------------------------------------------
-- Definition of initial T-algebra
----------------------------------------------------------------------
record isInitialTAlg (A : Set){{_ : isTAlg A}} : Set₁ where
  field
    fun : (B : Set){{_ : isTAlg B}} → A → B
    mor : (B : Set){{_ : isTAlg B}} → isTAlgMor (fun B)
    unq :
      (B : Set)
      {{_ : isTAlg B}}
      (f : A → B)
      (_ : isTAlgMor f)
      → ---------------
      fun B ≡ f

open isInitialTAlg{{...}} public

{-
The aim is to construct a T-algebra (M : Set, isTAlgM : isTalg M) for
which one can find a proof of isInitialTAlg M.
-}

----------------------------------------------------------------------
-- Non-terminating construction of intial T-algebra
----------------------------------------------------------------------
module NonTerminating where
  -- Agda accepts the following because of the POLARITY pragma for T
  data M : Set where
    mu : T M → M

  -- M is a T-algebra by construction
  instance
    isTAlgM : isTAlg M
    sup{{isTAlgM}} = mu
{-
But can one prove that M is the initial T-algebra? I don’t think so,
because both the existence and the uniqueness part of the initiality
property involve recursions that Agda cannot see are terminating.
-}
  module _
    (X : Set)
    {{ξ : isTAlg X}}
    where
    {-# TERMINATING #-} -- termination checking fails for rec
    rec : M → X
    rec (mu t) = sup (T' rec t)

    isTAlgMorrec : isTAlgMor rec
    isTAlgMorrec _ = refl

    module _
      (f : M → X)
      (isTAlgMorf : isTAlgMor f)
      where
      {-# TERMINATING #-} -- termination checking fails for uniq
      uniq : rec ≡ f
      uniq = funext λ{(mu t) →
        proof
          sup (T' rec t)
        =[ ap (λ f → sup (T' f t)) uniq ]
          sup (T' f t)
        =[ symm (isTAlgMorf _) ]
          f (mu t)
        qed}

  initialTAlg : isInitialTAlg M
  fun {{initialTAlg}} = rec
  mor {{initialTAlg}} = isTAlgMorrec
  unq {{initialTAlg}} = uniq

----------------------------------------------------------------------
-- Unsuccessful construction of initial T-algebra using sized types
----------------------------------------------------------------------
module Unsuccessful where
{-
To get around the problem in Nonterminating, it's natural to consider
using sizes to "help the termination checker by tracking the depth of
data structures across definition boundaries” (as it says in the Agda
documantation).  The first sized version of Nonterminating.M one might
consider is the indexed datatype

  data M : Size → Set where
    mu : (i : Size) → T (M i) → M (↑ i)

but this does not work very well for trying to prove the uniqueness
part of intiality, compared with the following parameterized datatype.
-}
  data M (i : Size) : Set where
    mu : (j : Size< i) → T(M j) → M i

  M∞ : Set  -- we hope this is the underlying type of
  M∞ = M ∞  -- an initial T-algebra

  φ : -- comparison function between M j and M i for j ≤ i
    (i : Size)
    (j : Size≤ i) -- Size≤ i is an abbreviation for Size< (↑ i)
    → -----------
    M j → M i
  φ _ _ (mu k x) = mu k x -- a version of the identity function

  φid :
    (i : Size)
    (x : M i)
    → ---------
    φ i i x ≡ x
  φid _ (mu _ _) = refl

  {-
  It seems that the following proposition is needed to prove the
  uniqueness property, but there is no obvious reason why it is
  provable. We can make it so by suitably quotienting M, as in module
  Successful, below.
  -}
  postulate
    muφ :
      (i : Size)
      (j : Size< i)
      (k : Size< j)
      (t : T(M k))
      → --------------------------
      mu j (T' (φ j k) t) ≡ mu k t

  -- M∞ is a T-algebra
  instance
    isTAlgM∞ : isTAlg M∞
    sup{{isTAlgM∞}} = mu ∞

  module _
    (X : Set)
    {{ξ : isTAlg X}}
    where
    -- the existence part of initiality
    rec : (i : Size) → M i → X
    rec i (mu j t) = sup (T' (rec j) t)

    rec∞ : M∞ → X
    rec∞ = rec ∞

    isTAlgMorrec∞ : isTAlgMor rec∞
    isTAlgMorrec∞ _ = refl

    module _
      (f : M∞ → X)
      (isTAlgMorf : isTAlgMor f)
      where
      -- the uniqueness part of intiality
      uniq :
        (i : Size)
        (x : M i)
        → -------------------
        rec i x ≡ f (φ ∞ i x)
      uniq i (mu j t) =
        proof
          sup (T' (rec j) t)
        =[ ap (λ f → sup (T' f t)) (funext (uniq j)) ]
          sup (T' (f ∘ φ ∞ j) t)
        =[ ap sup (symm (T∘ _ _ _)) ]
          sup (T' f (T' (φ ∞ j) t))
        =[ symm (isTAlgMorf _) ]
          f (mu ∞ (T' (φ ∞ j) t))
        =[ ap f (muφ ∞ ∞ j t) ] -- the postulated muφ is used here
          f (mu j t)
        qed

      uniq∞ : rec∞ ≡ f
      uniq∞ = funext λ x →
        proof
          rec ∞ x
        =[ uniq ∞ _ ]
          f (φ ∞ ∞ x)
        =[ ap f (φid ∞ _) ]
          f x
        qed

  initialTAlg : isInitialTAlg M∞
  fun {{initialTAlg}} = rec∞
  mor {{initialTAlg}} = isTAlgMorrec∞
  unq {{initialTAlg}} = uniq∞

----------------------------------------------------------------------
-- Successful construction of initial T-algebra using sized types
-- and quotients
----------------------------------------------------------------------
module Successful where
  -- we make a mutually inductive definition of a (size-indexed)
  -- type M i and a relation R i by which it is quotiented
  mutual
    data M (i : Size) : Set where
      mu : (j : Size< i) → T (Q j) → M i
      -- the use in mu of the quotient Q j rather than M j seems
      -- necessary in order to show that Q ∞ is a T-algebra

    data R (i : Size) : M i → M i → Set where
      muψ :
        (j : Size< i)
        (k : Size< j)
        (t : T (Q k))
        → --------------------------------
        R i (mu j (T' (ψ j k) t)) (mu k t)

    Q : Size → Set
    Q i = M i / R i

    φ : (i : Size)(j : Size≤ i) → M j → M i
    φ _ _ (mu k x) = mu k x

    φresp :
      (i : Size)
      (j : Size≤ i)
      {x y : M j}
      (_ : R j x y)
      → ------------
      R i (φ i j x) (φ i j y)
    φresp _ _ (muψ k l t) = muψ k l t

    ψ : (i : Size)(j : Size≤ i) → Q j → Q i
    ψ i j =
      quot.lift (quot.mk (R i) ∘ φ i j) (quot.eq (R i) ∘ φresp i j)
    -- end mutual

  φid :
    (i : Size)
    (x : M i)
    → ---------
    φ i i x ≡ x
  φid _ (mu _ _) = refl

  ψid :
    (i : Size)
    (x : Q i)
    → ---------
    ψ i i x ≡ x
  ψid i =
    quot.elim (R i)
      (λ x → ψ i i x ≡ x)
      (λ{(mu _ _) → refl})
      (λ r → uip' (quot.eq (R i) r))

  Q∞ : Set
  Q∞ = Q ∞

  qu : (i : Size) → T (Q i) → Q∞
  qu i = quot.mk (R ∞) ∘ mu i

  quψ :
    (i : Size)
    (j : Size< i)
    (t : T(Q j))
    → --------------------------
    qu i (T' (ψ i j) t) ≡ qu j t
  quψ i j = quot.eq (R ∞) ∘ muψ i j

  instance
    isTAlgQ∞ : isTAlg Q∞
    sup{{isTAlgQ∞}} = qu ∞

  module _
    (X : Set)
    {{ξ : isTAlg X}}
    where
    mutual
      rec : (i : Size) → Q i → X
      rec i = quot.lift (rec' i) (receq i)

      rec' : (i : Size) → M i → X
      rec' _ (mu j t) = sup (T' (rec j) t)

      receq :
        (i : Size)
        {x y : M i}
        (_ : R i x y)
        → ------------------
        rec' i x ≡≡ rec' i y
      receq _ (muψ j k t) =
        proof
          sup (T' (rec j) (T' (ψ j k) t))
        =[ ap sup (T∘ (rec j) (ψ j k) t) ]
          sup (T' (rec j ∘ ψ j k) t)
        =[ ap (λ g → sup (T' g t)) (recψ j k) ]
          sup (T' (rec k) t)
        qed

      rec'φ :
        (i : Size)
        (j : Size< i)
        (x : M j)
        → -------------------------
        rec' i (φ i j x) ≡ rec' j x
      rec'φ _ _ (mu _ x) = refl

      recψ :
        (i : Size)
        (j : Size< i)
        → -------------------
        rec i ∘ ψ i j ≡ rec j
      recψ i j  =
        funext (quot.elim (R j)
          (λ x → rec i (ψ i j x) ≡ rec j x)
          (rec'φ i j)
          (λ r → uip' (ap (rec j) (quot.eq (R j) r))))
    --end mutual

    rec∞ : Q∞ → X
    rec∞ = rec ∞

    isTAlgMorrec∞ : isTAlgMor rec∞
    isTAlgMorrec∞ _ = refl

    module _
      (f : Q∞ → X)
      (isTAlgMorf : isTAlgMor f)
      where
      uniq :
        (i : Size)
        (x : Q i)
        → -------------------
        rec i x ≡ f (ψ ∞ i x)
      uniq i =
        quot.elim (R i)
          (λ x → rec i x ≡ f (ψ ∞ i x))
          (λ{(mu j t) → symm (g j t)})
          (λ e → uip (ap (rec i) (quot.eq (R i) e)))
        where
        g :
          (j : Size< i)
          (t : T (Q j))
          → -----------------------------
          f (qu j t) ≡ sup (T' (rec j) t)
        g j t =
          proof
            f (qu j t)
          =[ ap f (symm (quψ ∞ _ _)) ]
            f (sup (T' (ψ ∞ j) t))
          =[ isTAlgMorf _ ]
            sup (T' f (T' (ψ ∞ j) t))
          =[ ap sup (T∘ _ _ _) ]
            sup (T' (f ∘ ψ ∞ j) t)
          =[ ap (λ f → sup (T' f t)) (symm (funext (uniq j))) ]
            sup (T' (rec j) t)
          qed

      uniq∞ : rec∞ ≡ f
      uniq∞ = funext λ x →
        proof
          rec∞ x
        =[ uniq ∞ _ ]
          f (ψ ∞ ∞ x)
        =[ ap f (ψid ∞ _) ]
          f x
        qed

  initialTAlg : isInitialTAlg Q∞ --success!
  fun {{initialTAlg}} = rec∞
  mor {{initialTAlg}} = isTAlgMorrec∞
  unq {{initialTAlg}} = uniq∞