Source code on Github
{-# OPTIONS --cubical-compatible --safe #-}
module Induction where
open import Level
open import Relation.Unary
RecStruct : ∀ {a} → Set a → (ℓ₁ ℓ₂ : Level) → Set _
RecStruct A ℓ₁ ℓ₂ = Pred A ℓ₁ → Pred 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)