Refined Church-encoded lists predicatively

CList.agda

open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality

postulate
  funext : ∀ {a b} {A : Set a} {B : A → Set b} → {f g : (x : A) → B x}
         → ((x : A) → f x ≡ g x) → f ≡ g

  uip : ∀ {a} {A : Set a} {x y : A} → {p q : x ≡ y} → p ≡ q

-- Basic Agda stuff
-----------------------------------------------------------------j---------------
trans : ∀ {a} {A : Set a} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

cong : ∀ {a b} {A : Set a} {B : Set b} {x y : A} → (f : A → B) → x ≡ y → f x ≡ f y
cong f refl = refl

subst : ∀ {a b} {A : Set a} {B : A → Set b} {x y : A} → (p : x ≡ y) → B x → B y
subst refl x = x

Σ-eq : ∀ {a b} {A : Set a} {B : A → Set b} → {p q : Σ A B}
     → (r : fst p ≡ fst q) → subst r (snd p) ≡ snd q
     → p ≡ q
Σ-eq refl refl = refl
--------------------------------------------------------------------------------

-- Refined Church encoding in a predicative setting
--------------------------------------------------------------------------------
LAlg : Set → Set → Set
LAlg A X = Σ X (λ _ → A → X → X)

isHom : ∀ {A X Y} → LAlg A X → LAlg A Y → (X → Y) → Set
isHom {A} {X} (xnil , xcons) (ynil , ycons) f =
  Σ (f xnil ≡ ynil)
    (λ _ → ∀ (x : X) (a : A) → f (xcons a x) ≡ ycons a (f x))

CL : Set → Set₁
CL A = Σ (∀ (X : Set) → LAlg A X → X)
         (λ c → ∀ (X Y : Set) → (XAlg : LAlg A X) → (YAlg : LAlg A Y) → (f : X → Y) → isHom XAlg YAlg f
                  → f (c X XAlg) ≡ c Y YAlg)
--------------------------------------------------------------------------------

-- True lists
--------------------------------------------------------------------------------
data List (A : Set) : Set where
  nil : List A
  cons : A → List A → List A

fold : {A : Set} → List A → (X : Set) → LAlg A X → X
fold nil X (xnil , xcons) = xnil
fold (cons a as) X (xnil , xcons) = xcons a (fold as X (xnil , xcons))

fold-fusion : {A : Set} (l : List A) (X Y : Set) (XAlg : LAlg A X) (YAlg : LAlg A Y) (f : X → Y)
            → isHom XAlg YAlg f → f (fold l X XAlg) ≡ fold l Y YAlg
fold-fusion nil X Y XAlg YAlg f (nil-hom , cons-hom) =  nil-hom
fold-fusion (cons a as) X Y XAlg YAlg f h@(nil-hom , cons-hom) =
  let IH = fold-fusion as X Y XAlg YAlg f h
  in trans (cons-hom  (fold as X (fst XAlg , snd XAlg)) a) (cong (snd YAlg a) IH)

fold-isHom : {A : Set} → (X : Set) → (XAlg : LAlg A X) → isHom (nil , cons) XAlg (λ l → fold l X XAlg)
fold-isHom X XAlg = refl , (λ l a → refl)

fold-id : {A : Set} (l : List A) → fold l (List A) (nil , cons) ≡ l
fold-id nil = refl
fold-id (cons x xs) = cong (cons x) (fold-id xs)
--------------------------------------------------------------------------------


-- Refined Church encoded lists live in the higher universe Set₁ but they
-- are isomorphic to true lists.
--------------------------------------------------------------------------------
from : {A : Set} → CL A → List A
from {A} (f , _) = f (List A) (nil , cons)

to : {A : Set} → List A → CL A
to {A} l = fold l , fold-fusion l

to-from : ∀ {A : Set} (l : List A) → from (to l) ≡ l
to-from l = fold-id l

from-to : ∀ {A : Set} (c : CL A) → to (from c) ≡ c
from-to {A} (f , p) = Σ-eq c-from-to p-eq where
  c-from-to : fold (from (f , p)) ≡ f
  c-from-to = funext (λ X → funext (λ XAlg → p (List A) X (nil , cons) XAlg (λ l → fold l X XAlg) (fold-isHom X XAlg)))

  p-eq : _
  p-eq = (funext (λ x → funext (λ x₁ → funext (λ x₂ → funext (λ x₃ → funext (λ x₄ → funext (λ x₅ → uip)))))))