    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- An abstraction of various forms of recursion/induction
    ------------------------------------------------------------------------

    -- The idea underlying Induction.* comes from Epigram 1, see Section 4
    -- of "The view from the left" by McBride and McKinna.

    -- Note: The types in this module can perhaps be easier to understand
    -- if they are normalised. Note also that Agda can do the
    -- normalisation for you.

    {-# OPTIONS --cubical-compatible --safe #-}

    module Induction where

    open import Level
    open import Relation.Unary
    open import Relation.Unary.PredicateTransformer using (PT)

    private
      variable
        a ℓ ℓ₁ ℓ₂ : Level
        A : Set a
        Q : Pred A ℓ
        Rec : PT A A ℓ₁ ℓ₂

    ------------------------------------------------------------------------
    -- A RecStruct describes the allowed structure of recursion. The
    -- examples in Data.Nat.Induction should explain what this is all
    -- about.

    RecStruct : Set a → (ℓ₁ ℓ₂ : Level) → Set _
    RecStruct A = PT A A

    -- A recursor builder constructs an instance of a recursion structure
    -- for a given input.

    RecursorBuilder : RecStruct A ℓ₁ ℓ₂ → Set _
    RecursorBuilder Rec = ∀ P → Rec P ⊆′ P → Universal (Rec P)

    -- A recursor can be used to actually compute/prove something useful.

    Recursor : RecStruct A ℓ₁ ℓ₂ → Set _
    Recursor Rec = ∀ P → Rec P ⊆′ P → Universal P

    -- And recursors can be constructed from recursor builders.

    build : RecursorBuilder Rec → Recursor Rec
    build builder P f x = f x (builder P f x)

    -- We can repeat the exercise above for subsets of the type we are
    -- recursing over.

    SubsetRecursorBuilder : Pred A ℓ → RecStruct A ℓ₁ ℓ₂ → Set _
    SubsetRecursorBuilder Q Rec = ∀ P → Rec P ⊆′ P → Q ⊆′ Rec P

    SubsetRecursor : Pred A ℓ → RecStruct A ℓ₁ ℓ₂ → Set _
    SubsetRecursor Q Rec = ∀ P → Rec P ⊆′ P → Q ⊆′ P

    subsetBuild : SubsetRecursorBuilder Q Rec → SubsetRecursor Q Rec
    subsetBuild builder P f x q = f x (builder P f x q)