-- Code supplement for formalization
-- (C) 2020 Patricia Johann, Andrew Polonsky
-- This information is free; you can redistribute and/or modify it under the terms of CC BY-SA 4.0.

module Hodt where

open import Agda.Primitive
open import Agda.Builtin.Unit
open import Data.Empty
open import Data.Product
open import Data.Sum
open import Agda.Builtin.Sigma
open import Agda.Builtin.Nat
open import Data.Vec hiding ([_])
open import Data.Fin hiding (_+_)
open import Function using (id ; _∘_)

module SetsAndFunctors where

  -- Set^k, the type of k-tuples of sets.
  kSet : Nat → Set₁
  kSet k = Vec Set k

  -- Morphisms in Set^k are tuples of maps between sets, coordinatewise
  kMap : ∀ {k} → (X Y : kSet k) → Set
  kMap {zero} _ _ = ⊤  -- unit type
  kMap {suc k} (X ∷ Xs) (Y ∷ Ys) = (X → Y) × (kMap Xs Ys)

  -- the identity morphism on a tuple
  idMap : ∀ {k} → (X : kSet k) → kMap X X
  idMap {zero} _ = tt
  idMap {suc k} (X ∷ Xs) = id , idMap Xs

  -- the type of natural transformations between functors in [Set^k, Set]
  kNat : ∀ {k} → (F G : kSet k → Set) → Set₁
  kNat F G = ∀ (X : kSet _) → F X → G X

  -- the identity natural transformation
  idNat : ∀ {k} → (F : kSet k → Set) → kNat F F
  idNat F = λ X x → x

  -- isFunctor (F) asserts that the given operation F : Set^k -> Set is a functor.
  -- to construct a term of type (isFunctor F) is to give a functorial action for F
  isFunctor : ∀ {k} → (kSet k → Set) → Set₁
  isFunctor F = ∀ {X Y : kSet _} → kMap X Y → F X → F Y

  -- the type of k-ary functors on Set
  kFunctor : Nat → Set₁
  kFunctor k = Σ[ f ∈ (kSet k → Set) ] isFunctor f

  -- the functorial action of the product functor
  ×-map : ∀ {A1 A2 B1 B2 : Set} → (A1 → B1) → (A2 → B2) → A1 × A2 → B1 × B2
  ×-map f g (a1 , a2) = (f a1 , g a2)

  -- the functorial action of the sum functor
  ⊎-map : ∀ {A1 A2 B1 B2 : Set} → (A1 → B1) → (A2 → B2) → A1 ⊎ A2 → B1 ⊎ B2
  ⊎-map f g (inj₁ x) = inj₁ (f x)
  ⊎-map f g (inj₂ y) = inj₂ (g y)

  -- the functorial action of the evaluation functor
  eval-map : ∀ {k} (F G : kFunctor k) → kNat (fst F) (fst G)
                 → {X Y : kSet k} → kMap X Y → fst F X → fst G Y
  eval-map {k} (F , Fmap) (G , Gmap) α {X} {Y} f = λ x → α Y (Fmap f x)
--eval-map {k} (F , Fmap) (G , Gmap) α {X} {Y} f = λ x → Gmap f (α X x)
  -- these two definitions are equivalent provided α is natural

  -- hoFunctor asserts that the given operation on functors
  -- is a higher-order functor, i.e., has a functorial action
  hoFunctor : ∀ {k} → (kFunctor k → kFunctor k) → Set₁
  hoFunctor {k} H = ∀ (F G : kFunctor k) → kNat (fst F) (fst G) → kNat (fst (H F)) (fst (H G))

  {- Next, we define the least fixed point operator in Agda's actual type universe.
     It has three components.
     Given a higher-order functor (H , Hmap) the first two define a k-ary functor
       (Mu H Hmap , Mu-fmap H Hmap).
     Its object part is defined as a datatype with a negative recursive occurrence,
       while the morphism part is defined by recursion over that datatype.
     The third component, Mu-hmap, asserts that the above construction is functorial in H.
     Well-foundedness and termination of these definitions are established
       meta-theoretically, by induction on the ordinal of accessibility of H.
     (Note that the functorial action of ⟦μα.h⟧ is indeed defined by transfinite
       recursion in the standard construction of initial algebras.)
     Also, due to mutual recursive dependency, the following definition is actually
       an instance of induction-recursion.
     In Agda, all componenets of a mutually recursive definition must first be
       declared with type information, before their definition is given. -}

  {-# NO_POSITIVITY_CHECK #-}
  data Mu {k} (H : kFunctor k → kFunctor k) (Hmap : hoFunctor H)
           : kSet k → Set

  {-# TERMINATING #-}
  Mu-fmap : ∀ {k} (H : kFunctor k → kFunctor k) (Hmap : hoFunctor H)
           → isFunctor (Mu H Hmap)

  -- the least fixed point, object part
  data Mu {k} H Hmap where
    sup : ∀ (X : kSet k) → fst (H (Mu H Hmap , Mu-fmap H Hmap)) X → Mu H Hmap X

  -- the least fixed point, morphism part
  Mu-fmap H Hmap {X} {Y} f (sup X x) = sup Y (snd (H (Mu H Hmap , Mu-fmap H Hmap)) f x)

  MU : ∀ {k} (H : kFunctor k → kFunctor k) (Hmap : hoFunctor H) → kFunctor k
  MU H Hmap = (Mu H Hmap , Mu-fmap H Hmap)

  -- the least fixed point, functorial action
  {-# TERMINATING #-}
  Mu-hmap : ∀ {k} (H1 : kFunctor k → kFunctor k) (H1map : hoFunctor H1)
                  (H2 : kFunctor k → kFunctor k) (H2map : hoFunctor H2)
                  (H* : ∀ (F : kFunctor k) → kNat (fst (H1 F)) (fst (H2 F)))
            → kNat (Mu H1 H1map) (Mu H2 H2map)
  Mu-hmap {k} H1 H1map H2 H2map H* X (sup X x) =
    let M1 = MU H1 H1map
        M2 = MU H2 H2map
        M12 = Mu-hmap H1 H1map H2 H2map H*
        y = H2map M1 M2 M12 X (H* M1 X x)
        z = H* M2 X (H1map M1 M2 M12 X x)
     in sup X y  -- or sup X z, which is equivalent whenever H* is natural.

  -- The unit type, polymorphic in the universe level
  data bigUnit {n : Level} : Set n where
    bigtt : bigUnit

open SetsAndFunctors

module Context where

  -- a context is a pair (n , v) where n is an integer
  -- and v is a vector of integers of length n.
  Cxt : Set
  Cxt = Σ[ n ∈ Nat ] Vec Nat n

  -- the zero vector, of the given length
  zeros : ∀ {n : Nat} → Vec Nat n
  zeros {zero} = []
  zeros {suc n} = zero ∷ zeros

  -- extending the context with k type variables
  add-zeros : ∀ (k : Nat) → (Γ : Cxt) → Cxt
  add-zeros k (n , v) = (k + n , zeros ++ v)

  -- extending the context with one k-ary functor variable
  add-one   : ∀ (k : Nat) → (Γ : Cxt) → Cxt
  add-one   k (n , v) = (suc n , k ∷ v)

  -- a context is interpreted by a tuple of functors of required arities
  ⟦_⟧C : Cxt → Set₁
  ⟦ 0 , [] ⟧C = bigUnit
  ⟦ suc n , k ∷ Γ ⟧C = kFunctor k × ⟦ n , Γ ⟧C

  -- a morphism between two instances of a context is a tuple
  -- of natural transformations between the corresponding functors (coordinatewise)
  Mor⟦_,_⟧ : ∀ {Γ} → ⟦ Γ ⟧C → ⟦ Γ ⟧C → Set₁
  Mor⟦_,_⟧ {0 , []} F G = bigUnit
  Mor⟦_,_⟧ {suc n , k ∷ Γ} ((F , Fmap) , Fs) ((G , Gmap) , Gs) = kNat F G × Mor⟦ Fs , Gs ⟧

  -- extending the interpretation with k type arguments
  add-types : ∀ {k} → kSet k → {Γ : Cxt} → ⟦ Γ ⟧C → ⟦ add-zeros k Γ ⟧C
  add-types {zero} _ {Γ} γ = γ
  add-types {suc k} (a ∷ as) {Γ} γ = let Kₐ = ((λ _ → a) , λ {X} {Y} _ → id)
                                     in (Kₐ , add-types as γ)

  -- extending the interpretation with a k-ary functor argument
  add-functor : ∀ {k} → kFunctor k → {Γ : Cxt} → ⟦ Γ ⟧C → ⟦ add-one k Γ ⟧C
  add-functor F γ = (F , γ)

  -- extending two instances of a context related by a morphism
  --   with two vectors of types related by a vector of maps
  -- yields two related instances of the extended context
  add-maps : ∀ {k} {X Y : kSet k} (f : kMap X Y) {Γ} {γ δ : ⟦ Γ ⟧C} (φ : Mor⟦ γ , δ ⟧)
             → Mor⟦ add-types X γ , add-types Y δ ⟧
  add-maps {zero} {X} {Y} f {Γ} {γ} {δ} φ = φ
  add-maps {suc k} {X ∷ Xs} {Y ∷ Ys} (f , fs) {Γ} {γ} {δ} φ = (λ _ → f) , add-maps fs φ

  -- the identity morphism on an instance of a context
  -- is the tuple of identity natural transformations on the constituent functors.
  idMor : ∀ {Γ} (γ : ⟦ Γ ⟧C) → Mor⟦ γ , γ ⟧
  idMor {.0 , []} γ = bigtt
  idMor {.(suc _) , A ∷ Γ} ((F , Fmap) , γ) = (idNat F , idMor γ)

  -- dot before a pattern means the argument has only one possible shape,
  -- and this shape has been inferred by the type-checker automatically

  -- the next function projects the interpretation of the context on the i'th coordinate
  -- that is, Proj i (F1,..,F|Γ|) = Fi
  Proj : ∀ {Γ} → ∀ (i : _) {k : Nat} {p : snd Γ [ i ]= k} → ⟦ Γ ⟧C → kFunctor k
  Proj {zero , []} i {k} {()} _
  Proj {suc n , a ∷ Γ} zero {.a} {here} (F , Fs) = F
  Proj {suc n , a ∷ Γ} (suc i) {k} {there p} (F , Fs) = Proj i {k} {p} Fs

  -- given a morphism between two instances (a tuple of natural transformations)
  -- we get a natural transformation between their i'th projectums
  Proj-map : ∀ {Γ} → ∀ (i : _) {k : Nat} {p : snd Γ [ i ]= k} → {γ δ : ⟦ Γ ⟧C}
             → Mor⟦ γ , δ ⟧ → kNat (fst (Proj i {k} {p} γ)) (fst (Proj i {k} {p} δ))
  Proj-map {.(suc _) , _} zero    {k} {here}    (φ , φs) = φ
  Proj-map {.(suc _) , _} (suc i) {k} {there p} (φ , φs) = Proj-map i φs

open Context -- using (Cxt ; ℱ)

module Grammar where

  -- The grammar of datatypes.
  data ℱ : Cxt → Set where
    Ⓐ : ∀ {Γ} (i : _) {k : Nat} {p : snd Γ [ i ]= k} → Vec (ℱ Γ) k → ℱ Γ
    Ⓚ : ∀ {n} {as} {k : Nat} → ℱ (n , as) → ℱ (suc n , k ∷ as)
    ⓪ : ∀ {Γ} → ℱ Γ
    ➀ : ∀ {Γ} → ℱ Γ
    ⨁ : ∀ {Γ} → ℱ Γ → ℱ Γ → ℱ Γ
    ⨂ : ∀ {Γ} → ℱ Γ → ℱ Γ → ℱ Γ
    μ : ∀ {Γ} (k : Nat) → ℱ (add-zeros k (add-one k Γ)) → Vec (ℱ Γ) k → ℱ Γ

  {- The interpretation of datatypes.
     There are four interpretation functions:
       * interpretation of expressions;
       * interpretation of vectors of expressions;
       * functoriality of interpretation of expressions;
       * functoriality of interpretation of vectors.
     These are all defined by mutual recursion. -}
  ⟦_⟧ :          ∀ {Γ : Cxt} (e : ℱ Γ)         → ⟦ Γ ⟧C → Set
  ⟦_⟧→ :     ∀ {k} {Γ : Cxt} (e : Vec (ℱ Γ) k) → ⟦ Γ ⟧C → kSet k
  ⟦_⟧map :       ∀ {Γ : Cxt} (e : ℱ Γ)         {γ δ : ⟦ Γ ⟧C} → Mor⟦ γ , δ ⟧ → ⟦ e ⟧ γ → ⟦ e ⟧ δ
  ⟦_⟧→map :  ∀ {k} {Γ : Cxt} (e : Vec (ℱ Γ) k) {γ δ : ⟦ Γ ⟧C} → Mor⟦ γ , δ ⟧ → kMap (⟦ e ⟧→ γ) (⟦ e ⟧→ δ)

  ⟦ Ⓐ i {k} {p} args ⟧ γ = fst (Proj i {k} {p} γ) (⟦ args ⟧→ γ)
  ⟦ Ⓚ e ⟧ (_ , γ)  = ⟦ e ⟧ γ
  ⟦ ⓪ ⟧ γ = ⊥
  ⟦ ➀ ⟧ γ = ⊤
  ⟦ ⨁ e1 e2 ⟧ γ = ⟦ e1 ⟧ γ ⊎ ⟦ e2 ⟧ γ
  ⟦ ⨂ e1 e2 ⟧ γ = ⟦ e1 ⟧ γ × ⟦ e2 ⟧ γ
  ⟦ μ k e args ⟧ γ =
    let H0 F X         = ⟦ e ⟧    (add-types     X        (add-functor F γ))
        H1 F {X} {Y} f = ⟦ e ⟧map (add-maps {_} {X} {Y} f (idMor (F , γ)))
        Hmap F G ν X   = ⟦ e ⟧map (add-maps     (idMap X) (ν , idMor γ))
     in Mu (λ F → (H0 F , H1 F)) Hmap (⟦ args ⟧→ γ)

  ⟦ [] ⟧→ γ = []
  ⟦ e ∷ exps ⟧→ γ = ⟦ e ⟧ γ ∷ ⟦ exps ⟧→ γ

  ⟦ Ⓐ i args ⟧map φ = eval-map (Proj i _) (Proj i _) (Proj-map i φ) (⟦ args ⟧→map φ)
  ⟦ Ⓚ e ⟧map (_ , φ) = ⟦ e ⟧map φ
  ⟦ ⓪ ⟧map φ = λ ω → ω
  ⟦ ➀ ⟧map φ = λ tt → tt
  ⟦ ⨁ e1 e2 ⟧map φ = ⊎-map (⟦ e1 ⟧map φ) (⟦ e2 ⟧map φ)
  ⟦ ⨂ e1 e2 ⟧map φ = ×-map (⟦ e1 ⟧map φ) (⟦ e2 ⟧map φ)
  ⟦ μ k e args ⟧map {γ} {δ} φ =
    let H0 ξ F X         = ⟦ e ⟧    (add-types     X        (add-functor F ξ))
        H1 ξ F {X} {Y} f = ⟦ e ⟧map (add-maps {_} {X} {Y} f (idMor (F , ξ)))
        Hmap ξ F G ν X   = ⟦ e ⟧map (add-maps     (idMap X) (ν , idMor ξ))
        Hγδ F X          = ⟦ e ⟧map (add-maps     (idMap X) (idNat (fst F) , φ))
        H : ∀ (ξ) → kFunctor k → kFunctor k
        H ξ F = (H0 ξ F , H1 ξ F)
        Fγ = MU (H γ) (Hmap γ)
        Fδ = MU (H δ) (Hmap δ)
        ν = Mu-hmap (H γ) (Hmap γ) (H δ) (Hmap δ) Hγδ
     in eval-map Fγ Fδ ν (⟦ args ⟧→map φ)

  ⟦ [] ⟧→map φ = tt
  ⟦ e ∷ es ⟧→map φ = (⟦ e ⟧map φ , ⟦ es ⟧→map φ)

open Grammar

module Induction where

  -- the type of predicates on type A
  Pred : Set → Set₁
  Pred A = A → Set

  -- the terminal predicate (truth)
  K₁ : ∀ {A : Set} → Pred A
  K₁ {A} = λ _ → ⊤

  -- the family of (coordinatewise) predicates on tuples of sets
  kFam : ∀ {k} → kSet k → Set₁
  kFam {zero} _ = bigUnit
  kFam (X ∷ Xs) = Pred X × kFam Xs

  -- the terminal family on a tuple
  tFam : ∀ {k} (X : kSet k) → kFam X
  tFam {zero} [] = bigtt
  tFam {suc k} (X ∷ Xs) = (K₁ , tFam Xs)

  -- (the type of) predicate component for a functor f : Set^k → Set
  -- (basically, the type of "liftings" of f from Set to Fam)
  kFunPred : ∀ {k} → (kSet k → Set) → Set₁
  kFunPred {k} f = ∀ (X : kSet k) → kFam X → Pred (f X)

  -- (the object part of) a *lifted* functor Fam^k → Fam is a pair
  -- (f : Set^k → Set , φ : ∀ X. kFam X → f X → Set), where
  --          f X : Set         gives the carrier part, and
  --    φ (X , P) : f X → Set   gives the predicate part
  kFam^ : Nat → Set₁
  kFam^ k = Σ[ f ∈ (kSet k → Set) ] kFunPred f

  {- The following code segment concerns interaction between predicate structure
  and functorial structure (maps).
  Since it is not needed for the induction rule, it is commented out. -}

  -- the following type asserts that a given tuple of maps (f1,..,fk) in kMap X Y
  -- is a tuple of predicate morphisms from (X , P) to (Y , Q).
  isFamMap : ∀ {k} {X Y : kSet k} (P : kFam X) (Q : kFam Y) → kMap X Y → Set
  isFamMap {zero} P Q tt = ⊤
  isFamMap {suc k} {X ∷ Xs} {Y ∷ Ys} (P , Ps) (Q , Qs) (f , fs) =
      (∀ (x : X) → P x → Q (f x)) × isFamMap Ps Qs fs

  -- the type of morphisms from one tuple of predicates to another.
  FamMap : ∀ {k} {X Y : kSet k} → kFam X → kFam Y → Set
  FamMap {k} {X} {Y} P Q = Σ[ f ∈ (kMap X Y) ] isFamMap P Q f

  isFamFunctor : ∀ {k} → (fφ : kFam^ k) → Set₁
  isFamFunctor {k} (f , φ) = Σ[ fmap ∈ isFunctor f ]
                             ∀ {X} {Y} (P : kFam X) (Q : kFam Y) (pq : FamMap P Q)
                             → ∀ (x : f X) → φ X P x → φ Y Q (fmap (fst pq) x)

  FamFunctor : Nat → Set₁
  FamFunctor k = Σ[ fφ ∈ (kFam^ k) ] isFamFunctor fφ

  -- cartesian product of families (the predicate part)
  ×Pred : ∀ {A B : Set} → Pred A → Pred B → Pred (A × B)
  ×Pred P Q (a , b) = P a × Q b

  -- disjoint sum of families (the predicate part)
  ⊎Pred : ∀ {A B : Set} → Pred A → Pred B → Pred (A ⊎ B)
  ⊎Pred P Q (inj₁ x) = P x
  ⊎Pred P Q (inj₂ y) = Q y

  -- evalulation of predicate functor on a predicate
  evalPred : ∀ {k} (fφ : kFam^ k) {A : kSet k} (B : kFam A)
             → fst fφ A → Set
  evalPred {k} (f , φ) {A} B = φ A B

  -- the predicate component (lifting) of a higher-order functor gives, for each
  -- lifting of the input functor, a lifting of the output functor
  hoFunPred : ∀ {k} → (kFunctor k → kFunctor k) → Set₁
  hoFunPred {k} h = ∀ {f : kFunctor k} → kFunPred (fst f) → kFunPred (fst (h f))

  -- if h is a higher order functor with a predicate lifting (= term of type hoFunPred h)
  -- then (Mu h) can be extended to a lifted functor (with a predicate component)
  {-# NO_POSITIVITY_CHECK #-}
  data Mu-pred {k} (h : kFunctor k → kFunctor k) (hmap : hoFunctor h) (hpred : hoFunPred h)
               : kFunPred (Mu h hmap) where
    sup-pred : ∀ {X : kSet k} (P : kFam X) (x : fst (h (MU h hmap)) X)
               → hpred {MU h hmap} (Mu-pred h hmap hpred) X P x
               → Mu-pred h hmap hpred X P (sup X x)

  -- a predicate on an instance is a sequence of "liftings" of each functor in the instance
  -- (i.e., a sequence of extensions of the functors with a predicate component.)
  Pred⟦_⟧ : ∀ {Γ} → ⟦ Γ ⟧C → Set₁
  Pred⟦_⟧ {zero , []} γ = bigUnit
  Pred⟦_⟧ {suc n , a ∷ as} ((F , Fmap) , Fs) = kFunPred F × Pred⟦ Fs ⟧

  -- akin to add-types and add-maps, this extends a predicate on an instance
  -- to get a predicate on an instance of the extended context .
  add-preds : ∀ {k} {As : kSet k} (Ps : kFam As) {Γ : Cxt} {γ : ⟦ Γ ⟧C}
              → Pred⟦ γ ⟧ → Pred⟦ add-types As γ ⟧
  add-preds {zero} {As} Ps {Γ} {γ} G = G
  add-preds {suc k} {A ∷ As} (P , Ps) {Γ} {γ} G = (λ _ _ → P) , add-preds Ps G

  -- projecting the predicate on an instance at a given coordinate
  ProjPred : ∀ {Γ} → ∀ (i : _) {k : Nat} {p : snd Γ [ i ]= k} → {γ : ⟦ Γ ⟧C}
             → Pred⟦ γ ⟧ → kFunPred (fst (Proj i {k} {p} γ))
  ProjPred {.(suc _) , .(k ∷ _)} zero {k} {here} {γ} (G , Gs) = G
  ProjPred {.(suc _) , .(_ ∷ _)} (suc i) {k} {there p} {γ} (G , Gs) = ProjPred i Gs

  -- predicate lifting of the interpretation:
  -- every predicate on a context instance yields a predicate on the interpretation.
  ⟦_⟧P : ∀ {Γ : Cxt} (e : ℱ Γ) {γ : ⟦ Γ ⟧C} → Pred⟦ γ ⟧ → Pred (⟦ e ⟧ γ)
  ⟦_⟧P→ : ∀ {k} {Γ : Cxt} (e : Vec (ℱ Γ) k) {γ : ⟦ Γ ⟧C} → Pred⟦ γ ⟧ → kFam (⟦ e ⟧→ γ)

  ⟦ Ⓐ i args ⟧P {γ} G = evalPred (_ , ProjPred i G) (⟦ args ⟧P→ G)
  ⟦ Ⓚ e ⟧P (_ , G) = ⟦ e ⟧P G
  ⟦ ⓪ ⟧P _ = K₁
  ⟦ ➀ ⟧P _ = K₁
  ⟦ ⨁ e₁ e₂ ⟧P {γ} G = ⊎Pred (⟦ e₁ ⟧P G) (⟦ e₂ ⟧P G)
  ⟦ ⨂ e₁ e₂ ⟧P {γ} G = ×Pred (⟦ e₁ ⟧P G) (⟦ e₂ ⟧P G)
  ⟦ μ k e args ⟧P {γ} G =
    let H₀γ F X         = ⟦ e ⟧    (add-types    X       (add-functor F γ))
        H₁γ F {X} {Y} f = ⟦ e ⟧map (add-maps {_} {X} {Y} f (idMor (F , γ)))
        Hmapγ  F G ν X  = ⟦ e ⟧map (add-maps     (idMap X) (ν , idMor γ))
        Hγ : kFunctor k → kFunctor k
        Hγ F = (H₀γ F , H₁γ F)
        Hpredγ : hoFunPred Hγ
        Hpredγ {F} Φ X ξ    = ⟦ e ⟧P   (add-preds {_} {X} ξ (Φ , G))
        Fγ = MU Hγ Hmapγ
        φ = Mu-pred Hγ Hmapγ Hpredγ
     in evalPred {k} (fst Fγ , φ) (⟦ args ⟧P→ G)

  ⟦ [] ⟧P→ {γ} G = bigtt
  ⟦ e ∷ es ⟧P→ {γ} G = (⟦ e ⟧P G) , (⟦ es ⟧P→ G)

open Induction

pattern [_] x = x ∷ []

module Lambda where
  α : Cxt
  α = (1 , [ 0 ])

  α:= : Set → ⟦ α ⟧C
  α:= A  = add-types [ A ] bigtt

  α:=⃗ : ∀ {A B : Set} → (A → B) → Mor⟦ α:= A , α:= B ⟧
  α:=⃗ {A} {B} f = (λ _ → f) , bigtt

  α:=ₚ : ∀ {A : Set} → Pred A → Pred⟦ α:= A ⟧
  α:=ₚ {A} P = (λ _ _ → P) , bigtt

  α,β : Cxt
  α,β = (2 , 0 ∷ 0 ∷ [])

  -- Lists

  alpha : ℱ α,β
  alpha = Ⓐ (suc zero) {zero} {there here} []

  beta : ℱ α,β
  beta = Ⓐ zero {zero} {here} []

  list-exp : ℱ α
  list-exp = μ 0 (⨁ ➀ (⨂ alpha beta)) []

  List : Set → Set
  List A = ⟦ list-exp ⟧ (α:= A)

  -- Lambda terms

  alpha₁ : ℱ α
  alpha₁ = Ⓐ zero {zero} {here} []

  α,φ,β : Cxt
  α,φ,β = (3 , 0 ∷ 1 ∷ 0 ∷ [])

  phi : ℱ α,φ,β → ℱ α,φ,β
  phi e = Ⓐ (suc zero) {suc zero} {there here} [ e ]

  beta₁ : ℱ α,φ,β
  beta₁ = Ⓐ zero {zero} {here} []

  lam-func : ℱ α,φ,β
  lam-func = ⨁ beta₁ (⨁ (⨂ (phi beta₁) (phi beta₁)) (phi (⨁ ➀ beta₁)))

  lam-exp : ℱ α
  lam-exp = μ 1 lam-func [ alpha₁ ]

  Lam : Set → Set
  Lam A = ⟦ lam-exp ⟧ (α:= A)

  Lam-map : ∀ {A B : Set} → (A → B) → Lam A → Lam B
  Lam-map f = ⟦ lam-exp ⟧map (α:=⃗ f)

  Lam-lift : ∀ {A : Set} → Pred A → Pred (Lam A)
  Lam-lift P = ⟦ lam-exp ⟧P (α:=ₚ P)

  -- More at Lambda.agda