module Induction where
open import Relation.Unary
RecStruct : Set → Set₁
RecStruct a = Pred a → Pred a
RecursorBuilder : ∀ {a} → RecStruct a → Set₁
RecursorBuilder {a} Rec = (P : Pred a) → Rec P ⊆′ P → Universal (Rec P)
Recursor : ∀ {a} → RecStruct a → Set₁
Recursor {a} Rec = (P : Pred a) → Rec P ⊆′ P → Universal P
build : ∀ {a} {Rec : RecStruct a} →
RecursorBuilder Rec →
Recursor Rec
build builder P f x = f x (builder P f x)
SubsetRecursorBuilder : ∀ {a} → Pred a → RecStruct a → Set₁
SubsetRecursorBuilder {a} Q Rec = (P : Pred a) → Rec P ⊆′ P → Q ⊆′ Rec P
SubsetRecursor : ∀ {a} → Pred a → RecStruct a → Set₁
SubsetRecursor {a} Q Rec = (P : Pred a) → Rec P ⊆′ P → Q ⊆′ P
subsetBuild : ∀ {a} {Q : Pred a} {Rec : RecStruct a} →
SubsetRecursorBuilder Q Rec →
SubsetRecursor Q Rec
subsetBuild builder P f x q = f x (builder P f x q)