{-# OPTIONS --universe-polymorphism #-}
module Induction where
open import Level
open import Relation.Unary
RecStruct : ∀ {a} → Set a → Set (suc a)
RecStruct {a} A = Pred A a → Pred A a
RecursorBuilder : ∀ {a} {A : Set a} → RecStruct A → Set _
RecursorBuilder Rec = ∀ P → Rec P ⊆′ P → Universal (Rec P)
Recursor : ∀ {a} {A : Set a} → RecStruct A → Set _
Recursor Rec = ∀ P → Rec P ⊆′ P → Universal P
build : ∀ {a} {A : Set a} {Rec : RecStruct A} →
RecursorBuilder Rec →
Recursor Rec
build builder P f x = f x (builder P f x)
SubsetRecursorBuilder : ∀ {a ℓ} {A : Set a} →
Pred A ℓ → RecStruct A → Set _
SubsetRecursorBuilder Q Rec = ∀ P → Rec P ⊆′ P → Q ⊆′ Rec P
SubsetRecursor : ∀ {a ℓ} {A : Set a} →
Pred A ℓ → RecStruct A → Set _
SubsetRecursor Q Rec = ∀ P → Rec P ⊆′ P → Q ⊆′ P
subsetBuild : ∀ {a ℓ} {A : Set 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)