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