module Induction where
open import Relation.Unary
RecStruct : Set → Set1
RecStruct a = Pred a → Pred a
RecursorBuilder : ∀ {a} → RecStruct a → Set1
RecursorBuilder {a} Rec = (P : Pred a) → Rec P ⊆ P → Universal (Rec P)
Recursor : ∀ {a} → RecStruct a → Set1
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 → Set1
SubsetRecursorBuilder {a} Q Rec = (P : Pred a) → Rec P ⊆ P → Q ⊆ Rec P
SubsetRecursor : ∀ {a} → Pred a → RecStruct a → Set1
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)