```{-

<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∞
```