------------------------------------------------------------------------
-- The Agda standard library
--
-- An abstraction of various forms of recursion/induction
------------------------------------------------------------------------

-- The idea underlying Induction.* comes from Epigram 1, see Section 4
-- of "The view from the left" by McBride and McKinna.

-- Note: The types in this module can perhaps be easier to understand
-- if they are normalised. Note also that Agda can do the
-- normalisation for you.

{-# OPTIONS --cubical-compatible --safe #-}

module Induction where

open import Level
open import Relation.Unary
open import Relation.Unary.PredicateTransformer using (PT)

private
  variable
    a  ℓ₁ ℓ₂ : Level
    A : Set a
    Q : Pred A 
    Rec : PT A A ℓ₁ ℓ₂


------------------------------------------------------------------------
-- A RecStruct describes the allowed structure of recursion. The
-- examples in Data.Nat.Induction should explain what this is all
-- about.

RecStruct : Set a  (ℓ₁ ℓ₂ : Level)  Set _
RecStruct A = PT A A

-- A recursor builder constructs an instance of a recursion structure
-- for a given input.

RecursorBuilder : RecStruct A ℓ₁ ℓ₂  Set _
RecursorBuilder Rec =  P  Rec P ⊆′ P  Universal (Rec P)

-- A recursor can be used to actually compute/prove something useful.

Recursor : RecStruct A ℓ₁ ℓ₂  Set _
Recursor Rec =  P  Rec P ⊆′ P  Universal P

-- And recursors can be constructed from recursor builders.

build : RecursorBuilder Rec  Recursor Rec
build builder P f x = f x (builder P f x)

-- We can repeat the exercise above for subsets of the type we are
-- recursing over.

SubsetRecursorBuilder : Pred A   RecStruct A ℓ₁ ℓ₂  Set _
SubsetRecursorBuilder Q Rec =  P  Rec P ⊆′ P  Q ⊆′ Rec P

SubsetRecursor : Pred A   RecStruct A ℓ₁ ℓ₂  Set _
SubsetRecursor Q Rec =  P  Rec P ⊆′ P  Q ⊆′ P

subsetBuild : SubsetRecursorBuilder Q Rec  SubsetRecursor Q Rec
subsetBuild builder P f x q = f x (builder P f x q)